[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLA Proof System - the syntax has impact on provability ?
Dear Stephan,
Thank you for your answer.
You mentioned that unofficial forthcoming version proved lemma5.
VARIABLE C, D
LEMMA lemma5 ==
C \subseteq [s : Nat]
/\
D = {[s|->x.s] : x \in C}
=>
C = {[s|->x.s] : x \in D}
OBVIOUS
Could you please tell which prover (TLA-Zenon, TLA-Isabelle, TLA-Z3, ...) of unofficial version of TLA Proof System proved lemma5 ?
Also, maybe there are settings in the TLA Proof System which may have impact on provability of such lemma (lemma5)?
Maybe settings of my TLA Proof System is different from yours.
Harold
On Tuesday, 19 March 2019 17:12:13 UTC+2, Stephan Merz wrote:
> Hello Harold,
>
> you are certainly not doing any mistake, it just means that there was some little progress between the official release and the forthcoming version. We are planning for a new release in spring but have to fix a few bugs that we are aware of.
>
> Best,
> Stephan
>
>
> > On 18 Mar 2019, at 19:26, haroldas.giedra@xxxxxxxxx wrote:
> >
> > 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.
--
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.