Does LATTICE rule work with the branch updated_enabled_cdot?

[Andreas Recke]

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

[Andreas Recke]

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

[Stephan Merz]

Hello Andreas,

apologies for the late reply.

In response to your original question, TLAPS is not built for checking proofs that apply temporal proof rules such as LATTICE. This was a deliberate design decision: in the original TLA papers, a temporal sequent A |- B is interpreted as "if A is valid in all interpretations of interest, then so is B". Equivalently, it can be identified with |- []A => B.

In non-temporal reasoning, TLAPS adopts the standard interpretation of predicate logic where A |- B (in actual syntax, "ASSUME A PROVE B") is equivalent with |- A => B.

In order to soundly extend TLAPS to temporal proof rules, we would have had to introduce a second kind of sequents, which could perhaps be written "[]ASSUME A []PROVE B". We decided that at least for the time being, we would like to avoid introducing this complication and solely rely on PTL to carry out proofs in temporal logic. The translation to propositional temporal logic recognizes if all hypotheses of the current proof context are "boxed", in which case all used facts A can be promoted to []A.

In short, it is impossible in first approximation to use temporal proof rules in a proof. We believe that despite this restriction, you should still be able to verify properties of specifications, but we may reconsider this design decision when we'll have better experience with carrying out proofs in temporal logic.

In particular, for your example [1]

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

you will see that you get a warning 

       System => j = d ~> j = d - 1 (* non-[] *),

in the proof obligations pane. This indicates that the corresponding hypothesis is not "boxed", and therefore the fact "e = d-1" will not be promoted to [](e = d-1), which would be necessary to conclude [2].

The following variant of your problem is accepted by TLAPS:

THEOREM SmallTest == ASSUME
   NEW VARIABLE j,
   NEW CONSTANT S,

   NEW CONSTANT d \in S,
   NEW CONSTANT e \in S,
   e = d-1,

   j=d ~> j=d-1
PROVE
   j=d ~> j=e
<1>. j=d-1 <=> j=e
  OBVIOUS
<1>. QED
  BY PTL

In particular, the formula "j=d ~> j=d-1" stands for "[](j=d => <> j=d-1)", and therefore all hypotheses are "boxed". This is representative of the reasoning that we expect to occur in a verification problem. Note that the auxiliary step is required because PTL does not handle equational reasoning and will therefore not replace "d-1" by "e". Since all hypotheses are "boxed", the assertion will be promoted to [](j=d-1 <=> j=e) when PTL is invoked.

–––

The explanation for your problems in the second message is similar. In particular, for

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 

the proof of the SUFFICES step succeeds because its assertion coincides with the standard interpretation of sequents. However, the QED step still doesn't succeed because of the presence of non-boxed hypotheses.

Hope this helps you to understand how to set up the proof for your original problem,

Stephan

[1] I presume that S is a constant that is declared or defined in your module, and I added the hypothesis "NEW CONSTANT S" for the sequent to be accepted.

[2] TLAPS could be a little more clever here by detecting that the hypothesis is a constant-level formula and promote it to the boxed formula anyway, but it doesn't do this.

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/37114691-5b42-42ce-a506-73ed0f5a4ea4n%40googlegroups.com.