为什么构造函数在这里花费这么长时间？

Question

考虑以下代码：

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 在第一种情况下与第二种情况相比如此慢。（可能跟constructor可以立马看到（没有任何归约）构造函数必须是第二种情况下的eq_refl有关？但是之后还是一定要归约...）

此外，在试图弄清楚 constructor 正在做什么时，我注意到文档没有说明该策略将使用哪种缩减策略。这种遗漏是有意的吗，如果你特别想要一个减少策略，你应该明确地说出你想要的减少策略（否则实现可以自由选择任何一个）？

Answer 1

简短回答：它会花时间尝试找出您的目标属于哪个归纳家族（两次，在 constructor 的情况下），使用 hnf.

更长的答案：做一些源代码潜水，它看起来像 constructor calls Tactics.any_constructor, while constructor 1 calls Tactics.constructor_tac. Tactics.any_constructor in turn calls Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind to determine the inductive type to count the constructors, and then calls Tactics.constructor_tac on each possible constructor in turn. For True, since there is one constructor, it's suggestive that the time for constructor is about double the time for constructor 1; I'm guessing that the time is therefore spent in reduce_to_quantified_ind. Tacred.reduce_to_quantified_ind, in turn, calls reduce_to_ind_gen，它又调用 hnf_constr。而且，确实，Time hnf 和 Time constructor 1 看起来差不多。此外，Time constructor 紧随手动 hnf 之后。我不确定 hnf 内部使用什么策略。文档遗漏几乎肯定不是故意的（至少，无论当前策略是什么，我认为都应该出现在脚注中，所以请随时报告错误），但我不清楚 [=10 使用的缩减策略=] 在确定您的目标属于哪个归纳家族时应该是 constructor.

规范的一部分

为什么构造函数在这里花费这么长时间？

Why does constructor take such a long time here?

coq