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

*From*: Roy Overbeek <r.over...@xxxxxxxxx>*Date*: Tue, 2 Jan 2018 02:33:27 -0800 (PST)

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

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

- Prev by Date:
**Re: [tlaplus] TLA+ Toolbox 1.5.4 release** - Next by Date:
**Re: [tlaplus] How can this lemma (involving []) be applied?** - Previous by thread:
**Re: How to model database tables?** - Next by thread:
**Re: [tlaplus] How can this lemma (involving []) be applied?** - Index(es):