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

[haroldas.giedra@xxxxxxxxx]

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.