The Coq mailing list

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

It may seem obvious to a human how to translate that string to a term 
understood by the kernel, but the general algorithm runs unification.

Gaëtan Gilbert

On 20/04/2023 17:12, Matthieu Baty wrote:
> 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