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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 26 Jul 2021 10:13:57 +0200*References*: <ee395ae0-b749-4f4e-9da0-611f91564424n@googlegroups.com>

Hello, that example is not an easy one for learning how to use the TLAPS proof assistant. I haven't tried to finish the proof, but I'll give you some hints on how to proceed. The level-2 proof starts with <2> SUFFICES ASSUME Inv, Lbl_1 \/ Lbl_2 \* Next PROVE Inv' This indicates that the case distinction should be as follows: <3>1. CASE Lbl_1 <3>2. CASE Lbl_2 Note that the actions such as Lbl_1 give you stronger hypotheses than just assuming, say, pc = "Lbl_1", which is but one conjunct of the definition of Lbl_1. Indeed, we can then finish the proof by <3>. QED BY <3>1,<3>2 Of course, the real work is in proving steps <3>1 and <3>2. I would not expect these proofs to work by brute force (BY expanding definitions and invoking utility lemmas), but probably you want to decompose them along the definitions of the actions. For Lbl_1, this suggests writing <4>1. CASE i < N <4>2. CASE ~(i < N) <4>. QED BY <4>1, <4>2 For step <4>1, we can now gather information on the effect of the action: <5>1. /\ pc = "Lbl_1" /\ j' = i+1 /\ pc' = "Lbl_2" /\ UNCHANGED << A, A0, i >> BY <3>1, <4>1 DEF Lbl_1 In particular, this tells us that we only need to worry about the conjunct of RealInv' that talks about what is expected when pc = Lbl_2. And now think about why the predicate holds true and guide the prover towards proving it. (As you observed, just adding all available facts and expanding all relevant definitions rarely works when proofs become a bit more complicated.) Steps <4>2 and <3>2 will be handled similarly. When the proof is done, you may be able to shorten it by compressing some proof steps into larger leaf proofs, but this is just cosmetics: I usually find that decomposing the proof helps me discover what is actually needed. Note in particular that I used the case assumptions <3>1 and <4>1 in the proof of step <5>1: as a user you may find this unnecessary but TLAPS requires all necessary facts to be invoked explicitly. Hope this helps (and if you finish the proof we'd love to add it to the collection of examples), Stephan
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/F4365BD0-F29D-4F1D-A526-2365B7621EF2%40gmail.com. |

**Follow-Ups**:

**References**:

- Prev by Date:
**[tlaplus] How to prove RealInv' in the example "BubbleSort" ?** - Next by Date:
**[tlaplus] How to obtain the value in a function** - Previous by thread:
**[tlaplus] How to prove RealInv' in the example "BubbleSort" ?** - Next by thread:
**Re: [tlaplus] How to prove RealInv' in the example "BubbleSort" ?** - Index(es):