[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Wed, 29 Mar 2023 10:27:21 -0700 (PDT)*References*: <CABj=xUW4ayrmf+sVxViXOmpj0QSGb=vRCpUwmqn=1QVygirEOQ@mail.gmail.com> <30EB506E-5FC5-4B2C-B21D-EB577C63BEA6@gmail.com> <470f9eae-3d0a-4271-afb9-7e23539444a3n@googlegroups.com>

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.AndrewOn 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 goalso 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 formTHEOREM Spec => []Invariant<1>1. Init => Invariant<1>2. Invariant /\ [][Next]_v => Invariant'<1>. QED BY <1>1, <1>2, PTL DEF SpecIn particular, the context of the QED step is empty, so all its assumptions are "boxed".StephanOn 29 Mar 2023, at 18:16, Andrew Helwer <andrew...@xxxxxxxxx> wrote:I ran into this error when writing theorems like:THEOREM Spec => []InvariantPROOF<1> HAVE Spec<1> ...<1> QEDIf I replace it with this then SANY stops complaining:THEOREM Spec => []InvariantPROOF<1> SUFFICES ASSUME Spec PROVE []Invariant OBVIOUS<1> ...<1> QEDWhy 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.

**Follow-Ups**:**Re: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.***From:*Stephan Merz

**RE: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.***From:*'Leslie Lamport' via tlaplus

**References**:**[tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.***From:*Andrew Helwer

**Re: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.***From:*Stephan Merz

**Re: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.** - Next by Date:
**RE: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.** - Previous by thread:
**Re: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.** - Next by thread:
**RE: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.** - Index(es):