Re: [tlaplus] TLAPS: ENABLEDrules depends on assumptions of level

On Tuesday, November 28, 2023 at 1:48:14 PM UTC-5 Stephan Merz wrote:

You are exploring mostly uncharted territory here, and I encourage you to file this as an issue on GitHub so that it won't get lost.

Logically, your proof should only rely on a state-level assumption, i.e. you should be able to prove

ASSUME terminate = TRUE
PROVE (ENABLED <<NextDown>>_cvars => ENABLED <<CNext>>_cvars)

which implies your actual proposition. But I see why you find it unwieldy that the proof fails with temporal-level hypotheses.

Stephan

On 28 Nov 2023, at 18:05, Ramon Snir <ramo...@xxxxxxxxx> wrote:

I am using TLAPS from branch "updated_enabled_cdot".

If there is any temporal assumption in the context, ENABLEDrules fails. This is true even if that assumption is irrelevant to the current step (but was needed for previous steps). I have not found a way to hide an unnamed assumption from a step. I've attached various attempts I've made below.

What I am trying to prove is: ASSUME [](terminate = TRUE) PROVE (ENABLED <<NextDown>>_cvars => ENABLED <<CNext>>_cvars)

which requires me to have a temporal assumption in context, because the statement is not true if the assumption is not true. I am not sure how to prove this lemma given this limitation.

I don't believe there is a way for me to restructure this without any assumptions, even by moving the lemma into the theorem, but even if I could it would be very unreadable.

Various attempts:

Q == terminate' = FALSE
P == terminate' = terminate

\* Example 1 - works */

LEMMA ENABLED Q => ENABLED P
PROOF
<1>. Q => P
  OMITTED
<1>. QED
  BY ENABLEDrules

\* Example 2 - works */

LEMMA ASSUME TRUE PROVE ENABLED Q => ENABLED P
PROOF
<1>. Q => P
  OMITTED
<1>. QED
  BY ENABLEDrules

\* Example 3 - doesn't work */

LEMMA ASSUME []TRUE PROVE ENABLED Q => ENABLED P
PROOF
<1>. Q => P
  OMITTED
<1>. QED
  BY ENABLEDrules
\*ENABLEDrules depends on assumptions of level > 1
\*
\*
\*Obligation:
\*
\*ASSUME NEW VARIABLE x,
\*     NEW VARIABLE terminate,
\*     []TRUE ,
\*     Q => P ,
\*     TRUE
\*PROVE  ENABLED Q => ENABLED P

\* Example 4 - doesn't work */

LEMMA ASSUME Q => P
  PROVE ENABLED Q => ENABLED P
PROOF BY ENABLEDrules
\*ENABLEDrules depends on assumptions of level > 1
\*
\*
\*Obligation:
\*
\*ASSUME NEW VARIABLE x,
\*     NEW VARIABLE terminate,
\*     Q => P ,
\*     TRUE
\*PROVE  ENABLED Q => ENABLED P

\* Example 5 - doesn't work */

LEMMA ASSUME ((terminate = TRUE) => (terminate' = FALSE))
  PROVE (ENABLED (terminate = TRUE) => ENABLED (terminate' = FALSE))
PROOF
<1>. QED
  BY ENABLEDrules
\*ENABLEDrules depends on assumptions of level > 1
\*
\*
\*Obligation:
\*
\*ASSUME NEW VARIABLE x,
\*     NEW VARIABLE terminate,
\*     terminate = TRUE => terminate' = FALSE ,
\*     TRUE
\*PROVE  ENABLED (terminate = TRUE) => ENABLED (terminate' = FALSE)

\* Example 6 - doesn't work */

PROPOSITION ASSUME [](terminate = TRUE)
  PROVE (ENABLED (terminate' = TRUE) => ENABLED (UNCHANGED terminate))
PROOF
<1>. (terminate = TRUE) /\ (terminate = TRUE)'
  BY PTL
<1>. (terminate' = TRUE) => (UNCHANGED terminate)
  OBVIOUS
<1>. QED \* fails, see status below
  BY ENABLEDrules
\*ENABLEDrules depends on assumptions of level > 1
\*
\*
\*Obligation:
\*
\*ASSUME NEW VARIABLE x,
\*     NEW VARIABLE terminate,
\*     [](terminate = TRUE) ,
\*     terminate = TRUE /\ (terminate = TRUE)' ,
\*     terminate' = TRUE => UNCHANGED terminate ,
\*     TRUE
\*PROVE  ENABLED (terminate' = TRUE) => ENABLED UNCHANGED terminate

--
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/0cda95d7-7d8a-4ce3-b8b4-b4f761e363fdn%40googlegroups.com.

Re: [tlaplus] TLAPS: ENABLEDrules depends on assumptions of level > 1