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

*From*: Ramon Snir <ramonsnir@xxxxxxxxx>*Date*: Tue, 28 Nov 2023 12:49:53 -0800 (PST)*References*: <0cda95d7-7d8a-4ce3-b8b4-b4f761e363fdn@googlegroups.com> <FC9E59E1-949E-48AE-9E8D-09947BD07A98@gmail.com>

I'll open a GitHub issue :)

Unfortunately, my proof really does require [](terminate = TRUE) and not (terminate = TRUE) due to the properties of the actions. Since this is a lemma and not a proposition I need to prove for its own sake, I may just have to work harder to reorganize things to change the lemma to a different lemma that doesn't require [](terminate = TRUE), but it's unfortunate. I might also keep that single step as proof omitted and keep the rest of the lemma as in.

It's just a shame because I felt close to wrapping up the whole proof and then this tiny lemma, which seemed obvious so I omitted its proof until the end, failed due to this quirk.

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 proveASSUME terminate = TRUEPROVE (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.StephanOn 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 isnottrue 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' = FALSEP == terminate' = terminate\* Example 1 - works */LEMMAENABLEDQ =>ENABLEDPPROOF<1>. Q => POMITTED<1>.QEDBYENABLEDrules\* Example 2 - works */LEMMAASSUMETRUEPROVEENABLEDQ =>ENABLEDPPROOF<1>. Q => POMITTED<1>.QEDBYENABLEDrules\* Example 3 - doesn't work */LEMMAASSUME[]TRUEPROVEENABLEDQ =>ENABLEDPPROOF<1>. Q => POMITTED<1>.QEDBYENABLEDrules\*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 */LEMMAASSUMEQ => PPROVEENABLEDQ =>ENABLEDPPROOFBYENABLEDrules\*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 */LEMMAASSUME((terminate = TRUE) => (terminate' = FALSE))PROVE(ENABLED(terminate = TRUE) =>ENABLED(terminate' = FALSE))PROOF<1>.QEDBYENABLEDrules\*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 */PROPOSITIONASSUME[](terminate = TRUE)PROVE(ENABLED(terminate' = TRUE) =>ENABLED(UNCHANGEDterminate))PROOF<1>. (terminate = TRUE) /\ (terminate = TRUE)'BYPTL<1>. (terminate' = TRUE) => (UNCHANGEDterminate)OBVIOUS<1>.QED\* fails, see status belowBYENABLEDrules\*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.

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/82528086-fa6f-4c55-9143-e9e82a7e4dd2n%40googlegroups.com.

**References**:**[tlaplus] TLAPS: ENABLEDrules depends on assumptions of level > 1***From:*Ramon Snir

**Re: [tlaplus] TLAPS: ENABLEDrules depends on assumptions of level > 1***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TLAPS: ENABLEDrules depends on assumptions of level > 1** - Next by Date:
**[tlaplus] How to fix "TLC cannot handle the temporal formula"?** - Previous by thread:
**Re: [tlaplus] TLAPS: ENABLEDrules depends on assumptions of level > 1** - Next by thread:
**[tlaplus] How to fix "TLC cannot handle the temporal formula"?** - Index(es):