爲什麼構造函數在這裏花了很長時間？

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規範的一部分。