Re: [tlaplus] Bug in Generating Proof Obligation?

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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