[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: shinsa82 <shinsa82@xxxxxxxxx>*Date*: Tue, 6 Aug 2019 02:49:54 -0700 (PDT)*References*: <61020587-764f-43bf-859f-24001b37baa4@googlegroups.com> <50ACB5BD-FAE7-4BD1-B471-BE58CE03D7AE@gmail.com> <d3afd887-ba2f-4b58-b001-b5484a6f5da1@googlegroups.com> <32628BBC-D4E2-4D10-8361-A15125D09CB7@gmail.com>

Got it. Thank you!

2019年7月31日水曜日 15時43分01秒 UTC+9 Stephan Merz:

-- 2019年7月31日水曜日 15時43分01秒 UTC+9 Stephan Merz:

By the way, is there any way to declare a formula including variables by "NEW <something> Invariant"?For introducing new identifiers in assumptions you can writeNEW [ CONSTANT | STATE | VARIABLE | ACTION | TEMPORAL ] <id>and if you don't specify a level, it defaults to CONSTANT. For a state-level formula such as an invariant, you want to writeNEW STATE InvRegards,Stephan

2019年7月29日月曜日 15時52分56秒 UTC+9 Stephan Merz:Hello,for a lemma involving temporal operators to be useful, its hypotheses should be "boxed", i.e. occur in the scope of an always operator. For example, you could stateLEMMA BoxImplies ==ASSUME NEW TEMPORAL F, NEW TEMPORAL G,[]F, [](F => G)PROVE []Gand then use this lemma somewhere in a proof about temporal properties. For details, please see section 8.3 of [1]. In practice, we never state lemmas of (propositional) temporal logic because the PTL decision procedure proves them automatically.Also note that your proof only goes through only because "NEW Invariant" implicitly means "NEW CONSTANT Invariant", hence the formula Invariant' in steps <1>2 and <1>3 gets rewritten to Invariant, and these steps are therefore tautologies. It is certainly not what you had in mind.Regards,Stephan[1] http://lamport.azurewebsites.net/tla/tla2- guide.pdf I want to prove a meta-theorem (or induction lemma, tactic) for a specification and reuse it in other proofs, like Coq.I wonder if its possible or not.Consider the following spec:----vars == <state variables>Act1 == ...Act2 == ...Next == Act1 \/ Act2Spec == Init /\ [][Next]_vars----Then we expect the following lemma holdfor any non-temporal formula "Invariant", and we want to use it to prove, say, its type invariance.(I know its too simple. Actually I want to consider more complicated cases)I was able to prove the lemma, but I could not "apply" the lemma to the type invariant theorem.Is there anything wrong?----LEMMASpecInduction ==ASSUMENEWInvariant,ASSUMEInitPROVEInvariant,ASSUMEInvariant, Act1PROVEInvariant',ASSUMEInvariant, Act2PROVEInvariant',PROVESpec => []InvariantPROOF<1>1. Init => InvariantOBVIOUS<1>2. Invariant /\ Next => Invariant'OBVIOUS<1>3. Invariant /\UNCHANGEDvars => Invariant'OBVIOUS<1>QEDBYPTL, <1>1, <1>2, <1>3DEFSpec------

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/61020587- .764f-43bf-859f-24001b37baa4% 40googlegroups.com --

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com .

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d3afd887- .ba2f-4b58-b001-b5484a6f5da1% 40googlegroups.com

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/129e09cf-45c2-44c8-b129-bb7b96e41bc5%40googlegroups.com.

**References**:**[tlaplus] Meta-theorem (induction lemma) in TLA+***From:*shinsa82

**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+***From:*Stephan Merz

**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+***From:*shinsa82

**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Debugging endless model checking** - Next by Date:
**[tlaplus] About ordinary assignment** - Previous by thread:
**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+** - Next by thread:
**[tlaplus] Fingerprint Collision** - Index(es):