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 रणनीति length l करने के लिए Nat.pred (length (n :: 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 देखें वहाँ एक रास्ता एक दो चरणों सरलीकरण यानी कि तोड़ने के लिए है अधिक जानकारी के लिए मैनुअल।