coq一步一步簡化？

Question

有沒有辦法一次簡化一個步驟？

假設有f1 (f2 x)兩者均可以依次經由單個simpl被簡化，是有可能簡化f2 x作爲第一步，檢查中間結果然後簡化f1？

就拿定理：

Theorem pred_length : forall n : nat, forall l : list nat, 
    pred (length (n :: l)) = length l. 
Proof. 
    intros. 
    simpl. 
    reflexivity. 
Qed. 

的simpl戰術簡化Nat.pred (length (n :: l))到length l。有沒有辦法打破這種成兩步簡化即：

Nat.pred (length (n :: l)) --> Nat.pred (S (length l)) --> length l 

Answer 1

您還可以將simpl用於特定模式。

Theorem pred_length : forall n : nat, forall l : list nat, 
    pred (length (n :: l)) = length l. 
Proof. 
intros. 
simpl length. 
simpl pred. 
reflexivity. 
Qed. 

如果你有像length的圖案，可以被簡化的重複出現，則可以通過給予該發生的位置（從左至右），例如進一步限制簡化的結果simpl length at 1或simpl length at 2第一次或第二次出現。

Answer 2

我們可以把簡化爲pred關，簡化它的參數，並重新打開它：

Theorem pred_length : forall n : nat, forall l : list nat, 
    pred (length (n :: l)) = length l. 
Proof. 
    intros. 
    Arguments pred : simpl never. (* do not unfold pred *) 
    simpl. 
    Arguments pred : simpl nomatch. (* unfold if extra simplification is possible *) 
    simpl. 
    reflexivity. 
Qed. 

請參見參考的§8.7.4手冊瞭解更多詳情。