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

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，而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规范的一部分。