Sıklıkla adım adım basitleştirme?

Question

Her seferinde bir adımı basitleştirmenin bir yolu var mı?

bu bir ilk adım olarak f2 x basitleştirmek ara sonucu incelemek ve sonra f1 basitleştirmek mümkündür, sen f1 (f2 x) her ikisi de tek bir simpl vasıtasıyla sırayla basitleştirilmiş olabilir var ki? örneğin

Al teoremi:

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

simpl taktik length l için Nat.pred (length (n :: l)) kolaylaştırır.

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

Answer 1

Belirli bir model için simpl'u da kullanabilirsiniz. durumda

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

Eğer daha fazla (soldan sağa) o oluşma bir pozisyon, örneğin vererek basitleştirme sonucunu kısıtlayabilir, basitleştirilmiş olabilir length gibi bir desen çeşitli olaylar var Birinci veya ikinci durum için simpl length at 1 veya simpl length at 2.

Answer 2

Biz pred off için basitleştirilmesi çevirmek onun argüman basitleştirmek ve tekrar açın edebilirsiniz:

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. 

Referans §8.7.4 Bkz iki aşamalı sadeleştirme yani içine kırmak için bir yol var mı Daha fazla bilgi için el kitabı.