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

# How can this lemma (involving []) be applied?

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