Re: [tlaplus] How can this lemma (involving []) be applied?

[Stephan Merz <stepha...@xxxxxxxxx>]

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.