coqでのステップバイステップの簡略化

Question

一度に1つのステップを簡略化する方法はありますか？

あなたは、単一のsimplを経由して順番に簡略化することができ、どちらもf1 (f2 x)があると、それは、最初のステップとして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戦術がlength lからNat.pred (length (n :: l))を簡素化します。 2段階の簡素化、すなわちにそれを破るためにそこに方法がある：

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

Answer 1

simplを特定のパターンに使用することもできます。あなたは、簡略化することができlengthようなパターンのいくつかのオカレンスを有する場合

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

は、さらに、例えば、（左から右へ）、その出現位置を与えることによって、簡略化の結果を制限することができsimpl length at 1またはsimpl length at 2を最初または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を参照してください。詳細はマニュアルを参照してください。