The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

> When proving a lemma through reflexivity, I expect unification to run twice:
> once while building the proof term interactively (can be skipped with
> exact_no_check eq_refl) and once at Qed time.

Technically at Qed time is only conversion (no existential variables may 
remain), but this does not matter here.


> Alternatively, I could bypass interactive proof term construction and 
provide my
> proof as a definition. I would then expect the validation of the term to 
take as
> long as the previous `Qed` (i.e. x seconds). Alas, I would be wrong, as it 
ends
> up taking twice that time.

Elaboration of the user syntax "(@eq_refl nat 0)" to a term with expected type 
"slow = 0" runs unification.
Then the kernel checks the produced term which involves running conversion.

Gaëtan Gilbert

On 18/04/2023 14:51, Matthieu Baty wrote:
> Hello coq-club,
>
> I recently ran into a puzzling Coq behavior regarding the typechecking of 
> manual
> proof terms definitions and  I would appreciate some pointers. The attached 
> file
> contains a runnable example of what I describe in here.
>
> When proving a lemma through reflexivity, I expect unification to run twice:
> once while building the proof term interactively (can be skipped with
> exact_no_check eq_refl) and once at Qed time.
>
> Lemma interactive_proof: slow = 0.
> Proof.
>    Time reflexivity. (* x seconds *)
> Time Qed.           (* also x seconds *)
>
> Alternatively, I could bypass interactive proof term construction and provide 
> my
> proof as a definition. I would then expect the validation of the term to take 
> as
> long as the previous `Qed` (i.e. x seconds). Alas, I would be wrong, as it 
> ends
> up taking twice that time.
>
> Time Definition raw_proof: slow = 0 := (@eq_refl nat 0). (* 2x seconds *)
>
> This is not a `Definition` issue, as using `Check` with the appropriate type
> annotations yields the same behavior.
>
> Time Check (@eq_refl nat 0: slow = 0). (* also 2x seconds *)
>
> Tactics in terms can help with this: replacing the body of the previous
> definition with ltac:(exact_no_check (<my_proof>)) makes it run in the time I
> expect it to (x seconds). I can't see why all proof definitions don't behave
> like this.
>
> What exactly is going on? Is there a good reason for this behavior?
>
> Thanks,
> Matthieu Baty