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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 18 Mar 2019 13:31:43 +0100*Ironport-data*: A9a23:/e/iTqv69NUNDWwG3bWpBGjEKufnOphVZvagV/efNr3duWXG1xXLv4 Ln58rqaCYexETQT0S+Sj+hDh3ZbPCQHIZof3erfkBaiV8n4FO/FGsan950bx0ydrxwbMnIql vCsmnrCMp5ZwwEHudruyXPqlxzhsLNWoTnvlIZ68hXQS0tUZ0YiMHMG0XsYKCPw1Keq/2S9N jKOQDVgAgZs2f2RJwB3UFtkXrgpnQvChj4PvMQf8aTdttSz6r5ffT4bRiWfAyFptyyhtaP5j QD/4fuejGsBD1OOokTyx/ITCcFGJjABQbhBBwHQ3EOef+yvgseM43quHBoJh825vjb7isum/ 9hflbGB+iVzfP+SXsugcBl7bEv2MYqWkh9OuLDrWObznyvtJ2lV61oqp391jBBQamYa0NQkW oi6DQvWEV18TYbRSc6Kt6K6pRCADbZtu8UcBfQkwxn06frlv/niytCr4lWZ3HYoI+0mR9zJl lqiHoXVpLgFWyUaEHLRHgTX//0kDHOs4nZuzhUKczDrFe3vrkA4K4zNcpsaWvZBQWL0h3gGZ jb0leGTxL52if2kXjSPZdbqfyz2tTF6wr9xkYZdx9mk4PiY4+wi5+jqvwmHj5+3JpuiuNKUj tTTB75urkj6XUeegyraI8kCdm/Gqv8NegUwCu3LASycoqj8Zz2HFb5f4EAwtizBanqCBd7Fl LRpDHPXc1g4xKFb/d+v1nP2VgwM7kTRlpeYwXAoF/dPplhy7boZGft3DRB1Mhf8ED8xOdAdA bscxftWHKOCAETxC2/SATIbLaN1lkGvDSlOTdGW9L2mpmN5dP13WIJvduScw/sEzGXvhCS7m sQiIpFT5iUPg/hwLr+t21mbMZtxWn+GWLGqJY5U3TKomTH/JkM5twmqZBXM0X8TiVwp3HH9D Yq0mMAiQrERFwrFUwnZJjnsVF0FnsjmVRKnc9+G5YU62Jx9DiPxPIjx4nqNU0WWgXUpq9tfI EcHa7E*References*: <a6d1fe97-2abe-45fa-816b-351d34f8b3bb@googlegroups.com> <B7C0DB61-0C23-40FD-9106-B4343C9D2820@gmail.com> <0c852494-4bf0-4510-a499-6b45609971ca@googlegroups.com>

My version proves this "BY OBVIOUS", but it may be because I'm using a pre-release version. "BY Z3" may work for the official release of TLAPS, assuming that you have Z3 installed. The proof (and perhaps the spec) would become easier if C and D were just sets of natural numbers instead of one-field records. Stephan > On 18 Mar 2019, at 12:29, haroldas.giedra@xxxxxxxxx wrote: > > > Thank you very much for your answer, Stephan. > > The example I gave came from the problem I want to solve. I want to prove such lemma: > > VARIABLE C, D > > LEMMA lemma5 == > C \subseteq [s : Nat] > /\ > D = {[s|->x.s] : x \in C} > => > C = {[s|->x.s] : x \in D} > > Is it possible to prove such lemma in TLA Proof System ? > > Harold > > On Monday, 18 March 2019 10:07:54 UTC+2, Stephan Merz wrote: >> Hello, >> >> theorem proving is indeed driven by syntax and unfortunately, TLAPS's automatic backends may fail to prove lemmas that are true, even if their truth is obvious to a human. Recognizing the elements of the set expression [s:{0}] requires reasoning about the extension of the set, whereas the set { [s |-> 0] } is just a singleton whose sole element is explicitly given. >> >> I am happy to report that your lemma1 will (also) be proved by SMT in the upcoming release, as well as >> >> LEMMA lemma3 == >> ASSUME NEW C, NEW D, >> C = {[s|->0]}, >> D = {[s|->x.s] : x \in C} >> PROVE C = D >> OBVIOUS >> >> The proof of lemma2 currently seems to require a somewhat roundabout proof: >> >> LEMMA lemma2 == >> ASSUME NEW C, NEW D, >> C = [s : {0}], >> D = {[s|->x.s] : x \in C} >> PROVE C = {[s|->x.s] : x \in D} >> <1>1. C = {[s |-> 0]} OBVIOUS >> <1>2. QED BY ONLY <1>1, D = {[s|->x.s] : x \in C} >> >> where step <1>1 is proved by Isabelle and step <1>2 by either SMT or Isabelle (but both backends fail if the assumption about C is not hidden). Thanks for reporting this, we'll try to add a suitable rewrite rule for automating the handling of similar expressions. >> >> Stephan >> >> >>> On 17 Mar 2019, at 20:50, haroldas.giedra@xxxxxxxxx wrote: >>> >>> >>> Hello, >>> >>> I have example of two lemmas which have the same meaning but slightly differs in the syntax. >>> >>> LEMMA lemma1 == C = {[s|->0]} >>> /\ >>> D = {[s|->x.s] : x \in C} >>> => >>> C = {[s|->x.s] : x \in D} >>> OBVIOUS >>> >>> LEMMA lemma2 == C = [s : {0}] >>> /\ >>> D = {[s|->x.s] : x \in C} >>> => >>> C = {[s|->x.s] : x \in D} >>> OBVIOUS >>> >>> lemma1 has been proved by "TLA - Isabelle", but "TLA - SMT", "TLA - Zenon", "TLA - Isabelle" fail to prove lemma2. >>> >>> I don't understand why TLA proof system fails to prove lemma2, which is different from lemma1 only in the syntax of TLA records. Meaning: >>> >>> C = {[s|->0]} >>> and >>> C = [s : {0}] >>> >>> which are the same for me. >>> >>> Harold >>> >>> -- >>> 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. >>> Visit this group at https://groups.google.com/group/tlaplus. >>> For more options, visit https://groups.google.com/d/optout. > > -- > 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. > Visit this group at https://groups.google.com/group/tlaplus. > For more options, visit https://groups.google.com/d/optout. -- 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:**Re: [tlaplus] TLA Proof System - the syntax has impact on provability ?***From:*haroldas . giedra

**References**:**[tlaplus] TLA Proof System - the syntax has impact on provability ?***From:*haroldas . giedra

**Re: [tlaplus] TLA Proof System - the syntax has impact on provability ?***From:*Stephan Merz

**Re: [tlaplus] TLA Proof System - the syntax has impact on provability ?***From:*haroldas . giedra

- Prev by Date:
**Re: [tlaplus] TLA Proof System - the syntax has impact on provability ?** - Next by Date:
**Re: [tlaplus] Re: Conjoining Specifications lemma1.2** - Previous by thread:
**Re: [tlaplus] TLA Proof System - the syntax has impact on provability ?** - Next by thread:
**Re: [tlaplus] TLA Proof System - the syntax has impact on provability ?** - Index(es):