SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.

[Andrew Helwer]

I ran into this error when writing theorems like:

THEOREM Spec => []Invariant

PROOF

  <1> HAVE Spec

  <1> ...

  <1> QED

If I replace it with this then SANY stops complaining:

THEOREM Spec => []Invariant

PROOF

  <1> SUFFICES ASSUME Spec PROVE []Invariant OBVIOUS

  <1> ...

  <1> QED

Why is the second one okay but the first one is not? I thought the first one was just shorthand for the second.

Andrew

[Stephan Merz]

The error message says:

Non-constant TAKE, WITNESS, or HAVE for temporal goal

so this restriction was an explicit design decision. (Not sure if it is documented anywhere ...)

Even with the explicit SUFFICES construct, your proof is likely to be doomed: at some point you'll have to apply temporal logic reasoning (the PTL method), and as a rule of thumb, in all temporal steps the context should only contain "boxed" assumptions, i.e., all assumptions A should be equivalent to []A. This is true for constant formulas A, formulas []A, <>[]A, WF_v(A) etc., but not for Spec, which will contain an initial state predicate.

If you continue your proof attempt, you'll find that PTL warns about "non-[] assumption" and fails. Invariant proofs should be written in the form

THEOREM Spec => []Invariant

<1>1. Init => Invariant

<1>2. Invariant /\ [][Next]_v => Invariant'

<1>. QED  BY <1>1, <1>2, PTL DEF Spec

In particular, the context of the QED step is empty, so all its assumptions are "boxed".

Stephan

--
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/CABj%3DxUW4ayrmf%2BsVxViXOmpj0QSGb%3DvRCpUwmqn%3D1QVygirEOQ%40mail.gmail.com.

[Andrew Helwer]

Thanks, Stephan! I was stuck with tlapm not proving the final QED step, removing the SUFFICES step fixed it.

Andrew

[Andrew Helwer]

Actually this introduces another issue: I've found that theorems like Spec => []TypeOK are very valuable when proving theorems like Spec => []InductiveInvariant, because you can always introduce the fact TypeOK to restrict the value of variables. However, you can only do that if you're assuming Spec is true; now that I'm not including Spec as an assumption with SUFFICES, how can I introduce TypeOK into a different proof?

Thanks,

Andrew

[Leslie Lamport]

THEOREM Spec => F

<1>1. Spec => []G

<1>2. SUFFICES ASSUME []G

               PROVE  F

<1>3. F

<1>4. QED

  BY <1>1, <1>2, <1>3, PTL

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9003123c-4c17-4c5a-9338-42f79676fd4cn%40googlegroups.com.

[Leslie Lamport]

I forgot to insert the proof of <1>2, which is “BY <1>1”

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/LV2PR21MB322990DB15E64D0CBB258465B8899%40LV2PR21MB3229.namprd21.prod.outlook.com.

[Stephan Merz]

Like so:

THEOREM TypeCorrect == Spec => []TypeOK

THEOREM Invariance == Spec => []Invariant

<1>1. Init => Invariant. \* you may add TypeOK on the left-hand side but it’s probably useless 

<1>2. TypeOK /\ Invariant /\ [Next]_v => Invariant’

<1>. QED  BY <1>1, <1>2, TypeCorrect, PTL DEF Spec

Appealing to the previously proved theorem TypeCorrect in the QED proof justifies the use of TypeOK in step <1>2.

Stephan

On 29 Mar 2023, at 19:27, Andrew Helwer <andrew...@gmail.com> wrote:



To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9003123c-4c17-4c5a-9338-42f79676fd4cn%40googlegroups.com.