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 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 it was possible to make a reflection in Prop, and not Set, and stumble upon it. My question is not how to correctly reflect, I just want to know why it is constructorso slow in the first case compared to the second case. (Maybe this has something to do with the fact that he constructorcan immediately see (without any abbreviations) that the constructor should be eq_reflin the second case? But it still needs to decrease later ...)
, , constructor, , , . , , , , , , ( )?