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

[Andreas Recke <Andreas.Recke@xxxxxxx>]

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?

Thank you again in advance!

Andreas

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4a6834b7-b851-4b82-9a7b-4759e173a434n%40googlegroups.com.