The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

I was a little puzzled by the behaviour of auto lately: it seems that
it is able to unfold opaque symbols and perform computations. I find
the later disturbing, because it gives very little (if any) control on
what auto will do, but I guess there is a good reason. However, the
following piece of code rise another question: how is it possible for
auto to be faster than apply ?

Could someone elaborate on this ?

( with coq 8.3, v 13027)

Axiom P : bool -> Prop.
Fixpoint f (x : nat) := match x with O => true | S n =>
                          let x :=  f n in
                            let y := f n in
                                   andb x y
                        end.
Definition n:= 18.
Time Eval vm_compute in f n. (* 0.04 *)
Time Eval lazy in f n. (* 1.19 *)
Time Eval compute in f n. (* 0.33 *)

Hypothesis H : P true.
Hint Resolve H.
Opaque f.

Goal P (f n). Time apply H. Time Qed. (* 2.94 | 1.4 *)
Goal P (f n). Time refine H. Time Qed. (* 2.95 | 1.5 *)
Goal P (f n). Time exact H. Time Qed. (* 2.95 | 1.5 *)
Goal P (f n). Time vm_compute. apply H.  Time Qed. (* 0.03 | 0.03 *)
Goal P (f n). Time auto. Time Qed. (* 1.5 | 1.4 *)

With best regards,
thomas