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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Tue, 2 Jan 2018 11:57:17 +0100*References*: <c5a4ba61-9440-4983-b8e1-766491a5ad65@googlegroups.com>

Hi Roy, first of all, welcome to the group and congratulations for getting so far in your proof! Your proof of the corollary fails because in lemma BoxImpl, ASSUME NEW P, NEW Q .... stands for ASSUME NEW CONSTANT P, NEW CONSTANT Q ... but you try to apply the lemma to the state predicates TypeOK and BalanceGeqZero. If you try to reprove the variant of BoxImpl with ASSUME NEW STATE P, NEW STATE Q .... the proof will (should) fail. The reason is that in the sequent ASSUME A PROVE B, the formula A is assumed only for the initial state. Thus the rephrased lemma assumes the implication P => Q only for the first state, which is not enough to prove the conclusion []Q. The way to prove your corollary is as follows: COROLLARY BGZInvariant == Spec => []BalanceGeqZero <1>1. TypeOK => BalanceGeqZero <1>. QED BY TypeOKInvariant, <1>1, PTL Since step <1>1 is proved in an empty context (more generally, in a context all of whose assumptions are boxed), it gets promoted to the theorem "[](TypeOK => BalanceGeqZero)" for the call to the PTL decision procedure. In your proof of the corollary, this is not possible because the step appears within the context with non-boxed assumption Spec. As a general rule, it is not useful to state proof rules of propositional temporal logic as lemmas because they are anyway superseded by the PTL decision procedure. Hope this helps, Stephan > On 2 Jan 2018, at 11:33, Roy Overbeek <r.over...@xxxxxxxxx> wrote: > > Hi, > > I am studying TLA+ and have written a specification Spec of a toy bank account. TypeOK asserts (among others) that balance \in Nat. I have already proven: > > THEOREM TypeOKInvariant == Spec => []TypeOK > > I would now like to prove the corollary > > COROLLARY BGZInvariant == Spec => []BalanceGeqZero > > where > > BalanceGeqZero == balance >= 0. > > To this end, I have first successfully proven a general lemma: > > LEMMA BoxImpl == ASSUME NEW P, > NEW Q, > P => Q, > []P > PROVE []Q > > My current proof for BGZInvariant is then: > > COROLLARY BGZInvariant == Spec => []BalanceGeqZero > <1> SUFFICES ASSUME Spec \* Proof succeeds. > PROVE []BalanceGeqZero > OBVIOUS > <1>1 TypeOK => BalanceGeqZero \* Proof succeeds. > BY DEFS TypeOK, BalanceGeqZero > <1>2 []TypeOK \* Proof succeeds. > BY TypeOKInvariant > <1> QED \* Proof fails. Why? > BY BoxImpl, <1>1, <1>2 > > I do not understand why the QED step fails. I have tried a similar setup with a lemma not involving [], and that worked, so it seems to be that P and Q should be instantiatable with respectively TypeOK and BalanceGeqZero. Adding PTL does not help, and I have so far not been able to find a solution in the literature. > > Any help would be much appreciated. > > Roy > > -- > 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+u...@xxxxxxxxxxxxxxxx. > To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. > Visit this group at https://groups.google.com/group/tlaplus. > For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:**Re: [tlaplus] How can this lemma (involving []) be applied?***From:*Roy Overbeek

**References**:**How can this lemma (involving []) be applied?***From:*Roy Overbeek

- Prev by Date:
**How can this lemma (involving []) be applied?** - Next by Date:
**Re: [tlaplus] How can this lemma (involving []) be applied?** - Previous by thread:
**How can this lemma (involving []) be applied?** - Next by thread:
**Re: [tlaplus] How can this lemma (involving []) be applied?** - Index(es):