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手册了解更多详情。