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

[Ramon Snir <ramonsnir@xxxxxxxxx>]

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0cda95d7-7d8a-4ce3-b8b4-b4f761e363fdn%40googlegroups.com.