RE: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.

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

From: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> On Behalf Of Andrew Helwer
Sent: Wednesday, March 29, 2023 10:27
To: tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Subject: Re: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.

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

On Wednesday, March 29, 2023 at 1:23:23 PM UTC-4 Andrew Helwer wrote:

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

Andrew

On Wednesday, March 29, 2023 at 12:49:26 PM UTC-4 Stephan Merz wrote:

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

On 29 Mar 2023, at 18:16, Andrew Helwer <andrew...@xxxxxxxxx> wrote:

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

--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUW4ayrmf%2BsVxViXOmpj0QSGb%3DvRCpUwmqn%3D1QVygirEOQ%40mail.gmail.com.

--
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/9003123c-4c17-4c5a-9338-42f79676fd4cn%40googlegroups.com.