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

*From*: haroldas.giedra@xxxxxxxxx*Date*: Mon, 18 Mar 2019 04:29:23 -0700 (PDT)*Ironport-data*: A9a23:MlzYYKAQHyVxTBVWkefolJn8SiHEJp4JvSvL7qdilV2FuWadymW3s8 GPNDWAz3nHWqDng/+BGzHqvF9PM/8pOXFJN2D4mJu7Pzhn3zAqKgqjw5Yv4qEH8mYqKjwID+ QYFh7RLYSHlsVisligjVnEEGDN/pwpmGNDsEziGs2qpL3UAwlWfw/nPiJyFOZskZvJaKoyWW rmHIZzODGVXC85MUx9H2Ga8IEP9T4Fup4JFz6Hp+lS3QSqYVDf+w1JJ1Hf2/O1kLVpJ7NuVT fegv9cgFuBSU2MeZ1Nycv0Kc8cJSu7bBBfOKGxqzCCZyIlrLGfnwCDewaQa3pzXYLy1U4jOs xTlUExgz4G6WYtXTqhpEIIOWnpkHgK35HUf8ZF/FQJy+dZxT49RnVmF99SnER0U0DZFhE0KH SVK66NK5Z1wKOi5dOjAwmCtEFPFwOJjD8SNK+2Haa7/d5h6L3X3mvfjSQe+e3PwIb4Cg4eCu C7FBskVxpvRONv4ldKLkdJfZnKmfcOWx+Fx924ZITcZepgJTv0wPMOmUl8U/Ujr3l99Scm2E f7ny2b0F57PGCJ6M+yvGFiwWBMqLvw5UCesJkU436kFtIgFfaayckDFwwuV15eEKk9/AVL/g /DTr6wLiONE09iB0nwucxMnDW2whuvQ3R8fjCg4UlggqUZQ6I/fxaHiaBJLP2EnQIcEvOqmm SYTPANcv176RONpEm1zXMjmPuLMlcfYNLjYAK9uZv7nl2vIMJsC5yDz+6WTh02BUhQiSkjFK eG2r5aGPq1U0pEyQd5EbHFAWNBuQhr6aVD/qEUkA0sDne3/lwKN6Ai3k/o5R8Er8IC+xQlem ukPHnldnwoZDvqLL+FXff7fWKXpJr4emeo9fcWDYKHUKe9VjLe6HPVPwGy/gK0nvF9KNfVex dEzolUtyN+CKkuivN/vFKayop9OBWacyzFtjMfoE1nhTa0Shl2hGXwJHz6ThOBVLDCCs1XUQ ==*References*: <a6d1fe97-2abe-45fa-816b-351d34f8b3bb@googlegroups.com> <B7C0DB61-0C23-40FD-9106-B4343C9D2820@gmail.com>

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.

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

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