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

*From*: haroldas.giedra@xxxxxxxxx*Date*: Mon, 18 Mar 2019 11:26:04 -0700 (PDT)*References*: <a6d1fe97-2abe-45fa-816b-351d34f8b3bb@googlegroups.com> <B7C0DB61-0C23-40FD-9106-B4343C9D2820@gmail.com> <0c852494-4bf0-4510-a499-6b45609971ca@googlegroups.com> <CAF72706-3B10-4D83-BD5D-4D58E424F909@gmail.com>

I tried to prove: LEMMA lemma5 == C \subseteq [s : Nat] /\ D = {[s|->x.s] : x \in C} => C = {[s|->x.s] : x \in D} BY Z3 TLA Proof System showed: status: z3: failed (timeout) Am I doing something wrong ? I can not change records to set Nat, because the original problem consists of records [s: SET1, st: SET2, d: SET3]. The example I gave is just simplified version of the problem. Maybe you know, when the new version of TLA Proof System will be released ? Thank you, Harold On Monday, 18 March 2019 14:31:46 UTC+2, Stephan Merz wrote: > 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:*Stephan Merz

**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

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

- Prev by Date:
**Re: [tlaplus] Re: Conjoining Specifications lemma1.2** - Next by Date:
**Re: [tlaplus] TLA Proof System - the syntax has impact on provability ?** - 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):