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.
Prop
而不是
Set
constructor
建造师
可以立即看到(没有任何减少)构造函数必须是
eq_refl
在第二种情况下?但之后仍必须减少……)
建造师
我注意到文档中没有说明该策略将使用哪种减少策略。这种省略是故意的吗?如果你特别想要一种减少策略,那么你应该明确地说你想要哪种减少策略(否则实现可以自由选择任何一种)?
