coq - 为什么构造函数在这里需要这么长时间？

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 中进行反射(reflection)而不是 Set并偶然发现了这一点。我的问题不是如何正确地进行反射，我只想知道为什么 constructor与第二种情况相比，第一种情况是如此缓慢。 (也许它与 constructor 可以立即看到(没有任何减少)构造函数必须是 eq_refl 在第二种情况下有关？但它仍然必须在之后减少......)

此外，在试图弄清楚 constructor我注意到文档没有说明该策略将使用哪种减少策略。这种遗漏是故意的吗？这个想法是，如果您特别想要一种减少策略，您应该明确说明您想要哪种减少策略(否则实现可以自由选择任何一种)？

Answer 1

简短的回答:它花时间试图找出你的目标是哪个归纳家庭的一部分(两次，在 constructor 的情况下)，使用 hnf .

更长的答案:做一些来源潜水，它看起来像 constructor calls Tactics.any_constructor , 而 constructor 1 calls Tactics.constructor_tac . Tactics.any_constructor 依次调用Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind确定归纳类型以计算构造函数，然后调用 Tactics.constructor_tac依次在每个可能的构造函数上。对于 True , 因为只有一个构造函数，所以 constructor 的时间大约是 constructor 1 时间的两倍;我猜测时间因此花在reduce_to_quantified_ind上。 . Tacred.reduce_to_quantified_ind ，反过来，调用 reduce_to_ind_gen , 依次调用 hnf_constr .而且，确实，它看起来像 Time hnf和 Time constructor 1差不多。此外，Time constructor在手动 hnf 之后立即生效.不知道是什么策略hnf内部使用。文档遗漏几乎肯定不是故意的(至少，我认为无论当前的策略是什么，都应该出现在脚注中，所以请随时报告错误)，但我不清楚 constructor 使用的缩减策略在确定您的目标属于哪个归纳系列时，应该是 constructor 规范的一部分.