Consider the following code:
Inductive Even : nat -> Prop :=
| EO : Even O
| ESS : forall n, Even n -> Even (S (S n)).
Fixpoint is_even_prop (n : nat) : Prop :=
match n with
| O => True
| S O => False
| S (S n) => is_even_prop n
end.
Theorem is_even_prop_correct : forall n, is_even_prop n -> Even n.
Admitted.
Example Even_5000 : Even 5000.
Proof.
apply is_even_prop_correct.
Time constructor. (* ~0.45 secs *)
Undo.
Time (constructor 1). (* ~0.25 secs *)
Undo.
(* The documentation for constructor says that "constructor 1"
should be the same thing as doing this: *)
Time (apply I). (* ~0 secs *)
Undo.
(* Apparently, if there's only one applicable constructor,
reflexivity falls back on constructor and consequently
takes as much time as that tactic: *)
Time reflexivity. (* Around ~0.45 secs also *)
Undo.
(* If we manually reduce before calling constructor things are
faster, if we use the right reduction strategy: *)
Time (cbv; constructor). (* ~0 secs *)
Undo.
Time (cbn; constructor). (* ~0.5 secs *)
Qed.
Theorem is_even_prop_correct_fast : forall n, is_even_prop n = True -> Even n.
Admitted.
Example Even_5000_fast : Even 5000.
Proof.
apply is_even_prop_correct_fast.
(* Everything here is essentially 0 secs: *)
Time constructor.
Undo.
Time reflexivity.
Undo.
Time (apply eq_refl). Qed.
I just wanted to see if you could do reflection in Prop rather than Set and stumbled upon this. My question is not how to do the reflection properly, I just want to know why constructor is so slow in the first case compared to the second case. (Maybe it has something to do with that constructor can immediately see (without any reductions) that the constructor must be eq_refl in the second case? But it must still reduce afterwards...)
Also, while trying to figure out what constructor is doing I noticed that the documentation does not say which reduction strategy will be used by the tactic. Is this omission intentional, and the idea is that you should explicitly say which reduction strategy you want if you want one in particular (otherwise the implementation is free to pick any)?