Bug in Generating Proof Obligation?

[Erick Lavoie]

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

[Stephan Merz]

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

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

[Erick Lavoie]

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

    

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ABCC0A14-1CCF-4C3D-A561-AABB74ED8E99%40gmail.com.

[Stephan Merz]

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?

Exactly – but as I said, this design decision could be revised, or perhaps more likely one could imagine an iterative deepening procedure that searches for useful facts and adds them to the proof so that the user doesn’t have to track them down manually.

Stephan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAF6T5KpSJ7dq0CDusqwR32QtA4OE_fmfVvGiV3ixOmBqurTvjw%40mail.gmail.com.

[Damien Doligez]

Hi Erick,

It may become less confusing if you know that omitting the name of the step makes the assumptions available again (because you can't add them with BY, they don't have a name anymore):

<1> ASSUME NEW u, NEW v, u \equiv v

     PROVE Op(u,r) \equiv Op(v,r)

  OBVIOUS

<1> QED OBVIOUS

The difference is not between global statements and local steps, it's more between numbered and unnumbered statements.

Best regards,

-- 

Damien