The Coq mailing list

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

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
Fixpoint slow_comp (n: nat) :=
  match n with
  | S n' => slow_comp n' + slow_comp n'
  | 0 => 0
  end.
Definition slow := slow_comp 20.
Set Printing Implicit.



Lemma ex1_refl: slow = 0.
Proof.
  Time reflexivity.                     (* 0.6s *)
  Show Proof.
Time Qed.                               (* 0.6s *)

(* Faster way of getting this version of the proof through the kernel: *)
Lemma ex2_change_no_check: slow = 0.
Proof.
  Time exact_no_check (@eq_refl nat 0). (* 0.0s *)
  Show Proof.                           (* Same as above *)
Time Qed.                               (* 0.6s *)



(* This is about as slow as TWO unifications of slow and 0, why is that? *)
Time Definition ex3_definition: slow = 0 := (@eq_refl nat 0).  (* 1.2s *)
(* Same behavior with Check... *)
Time Check (@eq_refl nat 0: slow = 0).                         (* 1.2s *)
(* ...but not if we use inline ltac with exact_no_check: *)
Time Check (ltac:(exact_no_check (@eq_refl nat 0)): slow = 0). (* 0.6s *)
(* It looks like there is some redundant checking going on. *)



(* Bonus contents: name validity checks occur between the two phases. We reuse
   a previously defined name to highlight this behavior (don't do this at
   home!). *)
Fail Time Definition ex3_definition: slow = 0 := (@eq_refl nat 0). (* 0.6s *)
Fail Time Definition ex3_definition: slow = 0 :=                   (* 0.0s *)
  (ltac:(exact_no_check (@eq_refl nat 0))).
Time Definition fresh_name: slow = 0 :=                            (* 0.6s *)
  (ltac:(exact_no_check (@eq_refl nat 0))).

(* Shouldn't the (usually) much faster name check run before the slower
   unification pass(es)? *)

(* Here's another illustration of why this ordering of checks can be annoying
   (not quite the same as there are no duplicated computations here): *)
Time Definition no_fail := Eval vm_compute in (slow_comp 24).
Fail Time Definition ex3_definition := Eval vm_compute in (slow_comp 24).
(* It took the same time as no_fail, but it could have failed instantaneously
   had the name check occurred before the computation. *)