The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Hi,

It seems that Coq is performing a beta/iota (?) reduction (?) of the
proof term when it encounters the commands Qed and Defined. Moreover, it
seems that Coq performs the reduction before it type-checks the term. I
did not find anything relevant in the documentation.

I have noticed this reduction because it has an adverse effect on some
of my scripts: Coq is wasting noticeably more time in Qed than in the
body of the proof script (while it is usually the opposite when scripts
do not invoke "no_check" tactics).

The following self-contained script is a toy example that reproduces
this behavior:

        Definition a := (3 * 49 * 49 = 3 * 7 * 7 * 7 * 7)%nat.
        Lemma b : a /\ a /\ a /\ a /\ a /\ a /\ a.
        refine ((fun p => conj p (conj p (conj p (conj p (conj p (conj p 
p)))))) _).
        (*refine (let p := _ in conj p (conj p (conj p (conj p (conj p (conj 
p p)))))).*)
        Time exact (refl_equal _).
        Show Proof.
        Qed.
        Print b.

(Depending on the speed of your Coq interpreter, you may want to
decrease or increase the factor 3 in Definition a.)

When printing b, you will notice that (refl_equal ...) appears seven
times in the proof term, which may explain why handling Qed takes 80% of
the whole script. Notice that, at Show Proof time, (refl_equal ...)
appears only once; it has not yet been replicated.

When replacing ((fun p => ...) _) by (let p := _ in ...), one occurrence
of (refl_equal ...) only is present in the final term. Qed takes only
30% of the whole script, and Coq is 3x faster overall. Moreover, there
are no differences between the pre-Qed term and the post-Qed term.

So this "let" mechanism is an efficient workaround for the slowdown I
have experienced. But I'm still surprised by this behavior. So here are
a few questions:

      * What is the rationale for this reduction? Is it meant to
        simplify the proof term?
      * If it is, why not apply it to "let" constructs too?
      * Why expand applications with several occurrences of their
        variable?
      * Why perform the type-checking after the reduction? For extra
        confidence?

Best regards,

Guillaume