[tlaplus] Re: Does LATTICE rule work with the branch updated_enabled_cdot?

Some additional weird stuff: when decomposing the proof into
THEOREM SmallTest == ASSUME
NEW TEMPORAL System,
NEW VARIABLE j,
NEW CONSTANT d \in S,
NEW CONSTANT e \in S,
e = d-1,
System => j=d ~> j=d-1
PROVE
System => j=d ~> j=e
<1>1. SUFFICES ASSUME System
PROVE  j=d ~> j=e
OBVIOUS
<1>2. QED BY <1>1

TLAPS proves the SUFFICES construct <1>1 successfully!! But the outer proof failed. I can even prove that

j=d-1 <=> j=e OBVIOUS

but it does not help. Playing the the proof tactics, e.g. putting PTL into the BY clause or not did not change the situation.

Moreover, writing the proof like
THEOREM SmallTest == ASSUME
NEW TEMPORAL System,
NEW VARIABLE j,
NEW CONSTANT d \in S,
NEW CONSTANT e \in S,
e = d-1,
System => j=d ~> j=d-1,
System
PROVE
j=d ~> j=e
OBVIOUS

Fails, although this is the same as the SUFFICES proof above.

Seems like a bug.

Kind regards
Andreas

Andreas Recke schrieb am Donnerstag, 15. September 2022 um 21:37:36 UTC+2:
Hi,
I am trying to set up a liveness proof.
I was able to use the WF1 rule successfully, but going farther did not work.

I have just a simple "count down from N to 0 then stop" spec.
I know there is an example that uses NatInduction, but I want to specifically
use the LATTICE rule because I would like to set up a framework for a more
complicated spec.

But now I am stuck at this:
ASSUME d \in S /\ d > 0
[]TypeOk /\ [][Next]_vars /\ WF_vars(Next) => (G(d) ~> G(d-1))

But reformulating this to
[]TypeOk /\ [][Next]_vars /\ WF_vars(Next) => (G(d) ~> \E e \in S: e < d /\ G(e))

does not work.

Moreover, another toy example with somehow similar also failed
THEOREM SmallTest == ASSUME
NEW TEMPORAL System,
NEW VARIABLE j,
NEW CONSTANT d \in S,
NEW CONSTANT e \in S,
e = d-1,
System => j=d ~> j=d-1
PROVE
System => j=d ~> j=e
BY
PTL

As if there is a bug. Or am I making a strange mistake?

Anyway: does LATTICE work with this new branch?