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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 10 Apr 2020 12:21:05 +0200*References*: <b24fe285-fbfe-4117-8560-7836646f51b2@googlegroups.com> <63676597-8A03-44C4-A3A0-DD7801FBD695@gmail.com> <9bb91b56-ba80-43fd-8805-b47e49071291@googlegroups.com>

Hello,
yes, success of that step shows you that your decomposition into cases is adequate for proving the enclosing goal.
Understanding why a proof fails is hard. It could be that the assertion is wrong or it could be that the automatic backends are not strong enough to understand why the assertion holds. In order to better understand what is going on, you will have to look at the proof obligation that the PM displays, and the smaller the obligation is, the easier it will be for you to understand it. It is therefore not helpful to just expand all definitions and use all available facts – also, that risks making the provers confused. It is better to introduce lemmas and outline the proof as a sequence of small steps (you may later collapse them into a larger step once you've understood how the proof really works). Doing so in the concrete example reveals that quite a bit of scaffolding is necessary, such as showing that infinity / minus infinity is different from integers or reasoning about how the minimum of a set evolves when an element is added etc. I also strengthened the invariant to include the fact that the set y is always finite, since this is needed for the lemmas about setMin / setMax. I have not completed the proof, but I hope that the outline in the attached module will help you better understand how to successfully write proofs. It may be the case that some facts proved in sub-cases of <3>10 / <3>11 will again be needed in the proof of <3>12. In that case you may want to refactor the proof to introduce them as level-3 steps and use them wherever needed. (That's why I left some "space" before <3>10.) Regards, Stephan P.S.: Instead of copying and pasting parts of proofs, please attach TLA+ modules that can be directly loaded into the Toolbox. 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/D5755256-A183-480F-B208-9AEAF3612D54%40gmail.com. |

**Attachment:
MinMax1.tla**

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/D5755256-A183-480F-B208-9AEAF3612D54%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] MinMax Refinement Proof in TLAPS***From:*Balaji Arun

**References**:**[tlaplus] MinMax Refinement Proof in TLAPS***From:*Balaji Arun

**Re: [tlaplus] MinMax Refinement Proof in TLAPS***From:*Stephan Merz

**Re: [tlaplus] MinMax Refinement Proof in TLAPS***From:*Balaji Arun

- Prev by Date:
**Re: [tlaplus] Message "Successor state is not completely specified" when overriding a Action in Java** - Next by Date:
**[tlaplus] Cannot figure out how to make editor colors like those seen in video** - Previous by thread:
**Re: [tlaplus] MinMax Refinement Proof in TLAPS** - Next by thread:
**Re: [tlaplus] MinMax Refinement Proof in TLAPS** - Index(es):