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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 29 Jul 2019 08:52:53 +0200*References*: <61020587-764f-43bf-859f-24001b37baa4@googlegroups.com>

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 state LEMMA BoxImplies == ASSUME NEW TEMPORAL F, NEW TEMPORAL G, []F, [](F => G) PROVE []G and 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
--
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/50ACB5BD-FAE7-4BD1-B471-BE58CE03D7AE%40gmail.com. |

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

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

- Prev by Date:
**[tlaplus] Re: Specifying Garbage Collection** - Next by Date:
**Re: [tlaplus] Proving INV1** - Previous by thread:
**[tlaplus] Meta-theorem (induction lemma) in TLA+** - Next by thread:
**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+** - Index(es):