The Coq mailing list

[Matthieu Baty <matthieu.baty AT epfl.ch>]

Hi Gaëtan and thanks for your answer,

> Elaboration of the user syntax "(@eq_refl nat 0)" to a term with 
expected type "slow = 0" runs unification.

I still fail to see why it is required at this stage: any possible error 
should be detected by the subsequent kernel checks anyways, right?

Thanks,

Matthieu

On 18/04/2023 14:55, Gaëtan Gilbert wrote:
> > 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