Re: [tlaplus] Bug in Generating Proof Obligation?

On Thursday, May 8, 2025 at 10:57:25 AM UTC+2 Erick Lavoie wrote:

Dear Stephan,

I see, thank you for the clarification. As a beginner, the inconsistency between a global statement that can be proven obviously:

LEMMA ASSUME NEW u, NEW v, u \equiv v
PROVE u \equiv v
OBVIOUS

and a step that requires restating the assumption:
...
<1>1 ASSUME NEW u, NEW v, u \equiv v
PROVE u \equiv v
BY u \equiv v
...
was really confusing. I only got out of that confusion by chance when looking at the proof obligation being generated. I initially
assumed that if I was mentioning something as an assumption, then it was always used in a proof obligation.

Was this done because the number of facts that can be effectively handled by the provers is limited, and in a step
there is typically a larger number of facts being tracked from previous steps?

Best regards,

Erick



On Tue, May 6, 2025 at 4:19 PM Stephan Merz <stepha...@xxxxxxxxx> wrote:
In general, all assumptions and facts used in the proof of a step have to be listed in the BY clause. So, you’d have to write

BY <1>1

instead of OBVIOUS in the proof of step <1>1. (Within the proof of step <1>1, the fact <1>1 refers to the assumptions of that step, whereas it refers to the ASSUME PROVE sequent outside of that proof.)

The exception to this general rule is that top-level assumptions, domain assumptions corresponding to declarations "NEW x \in S", as well as facts corresponding to unnumbered steps are used implicitly.

Of course, these are debatable design decisions.

Regards,
Stephan

On 6 May 2025, at 13:14, Erick Lavoie <erick....@xxxxxxxxx> wrote:

Dear TLA+ community,

I believe I have stumbled upon a bug when generating proof obligations with TLAPS. The following example cannot be proven by TLAPS:

LEMMA InnerSym3 ==
ASSUME NEW p, NEW q, NEW r, NEW Op(_,_),
   ASSUME NEW u, NEW v
   PROVE Op(u,v) \equiv Op(v,u)
PROVE Op(Op(p,q),r) \equiv Op(Op(q,p),r)
<1>1 ASSUME NEW u, NEW v, u \equiv v
   PROVE Op(u,r) \equiv Op(v,r)
  OBVIOUS
<1> QED BY <1>1

The proof obligation that is generated for step <1>1 is the following:

ASSUME NEW CONSTANT p,
   NEW CONSTANT q,
   NEW CONSTANT r,
   NEW CONSTANT Op(_, _),
   ASSUME NEW CONSTANT u,
NEW CONSTANT v
   PROVE Op(u, v) <=> Op(v, u) ,
   NEW CONSTANT u,
   NEW CONSTANT v

PROVE Op(u, r) <=> Op(v, r)

Notice how the assumption that 'u \equiv v' is missing from the obligation. Replacing OBVIOUS by 'BY u \equiv v', now allows TLAPS to prove step <1>1, and the LEMMA because the missing 'u \equiv v' is now added.

LEMMA InnerSym3 ==
ASSUME NEW p, NEW q, NEW r, NEW Op(_,_),
   ASSUME NEW u, NEW v
   PROVE Op(u,v) \equiv Op(v,u)
PROVE Op(Op(p,q),r) \equiv Op(Op(q,p),r)
<1>1 ASSUME NEW u, NEW v, u \equiv v
   PROVE Op(u,r) \equiv Op(v,r)
BY u \equiv v

<1> QED BY <1>1

Is this expected? If so, why? Otherwise, where is the best place to report the bug?

Best regards,

Erick

--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAF6T5Kpup8A9QMsVvFDS-59w9rp6MYTCXatW_vCZO-AR%2BGb3pw%40mail.gmail.com.

--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ABCC0A14-1CCF-4C3D-A561-AABB74ED8E99%40gmail.com.