[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLA Proof System - the syntax has impact on provability ?
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.