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

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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.