| 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]
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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2CBA9C6F-EDA4-46BC-BECA-49B237D074B0%40gmail.com. |