coq中的標準形式的定義

Question

在作者B. Pierce的「類型和編程語言」一書中，作者引入了一種小語言來介紹本書中使用的不同概念。

語言是：

t::= 
    true 
    false 
    if t then t else t 
v::= 
    true 
    false 

有三個減速規則：

if true then t2 else t3 \rightarrow t2 

if false then t2 else t3 \rightarrow t3 

t1 \rightarrow t1' 
------------------ 
if t1 then t2 else t3 \rightarrow if t1' then t2 else t3 

我想證明，每個範式是一種價值。

我用下面的定義爲範式：

Definition normal_form (t:term) := 
    ~(exists t', step t t'). 

我堅持，因爲在一個點上，我有東西，看起來像：

~ ~(exists t : term, ...) 

和我不噸看我怎麼能推斷

exists t : term, ... 

因爲我們在一個在tuitionistic邏輯。

這裏是整個證明：

Inductive term : Set := 
| true : term 
| false : term 
| ifthenelse : term -> term -> term -> term. 


Definition normal_form (t:term) := 
    ~(exists t', step t t'). 

Inductive is_value : term -> Prop := 
| vtrue : is_value true 
| vfalse : is_value false. 


Lemma normal_form_implies_value : forall t, normal_form t -> is_value t. 
Proof. 
    intro. 
    induction t. 
    intros. 
    apply vtrue. 
    intros. 
    apply vfalse. 
    intros. 
    unfold normal_form in H. 
    destruct t1. 
    unfold not in H. 
    assert (exists t' : term, step(ifthenelse true t2 t3) t'). 
    exists t2. 
    apply eiftrue. 
    apply H in H0. 
    contradiction. 
    assert (exists t' : term, step(ifthenelse false t2 t3) t'). 
    exists t3. 
    apply eiffalse. 
    apply H in H0. 
    contradiction. 
    assert(~(is_value (ifthenelse t1_1 t1_2 t1_3))). 
    intro. 
    inversion H0. 
    assert(~(normal_form(ifthenelse t1_1 t1_2 t1_3))). 
    intro. 
    apply IHt1 in H1. 
    contradiction. 
    unfold normal_form in H1. 
    unfold not in H1. 

我應該使用其他定義的正常形態？沒有任何經典公理就可以完成證明嗎？

Answer 1

is_value是可判定的，

Lemma is_value_dec : forall t, {is_value t} + {~is_value t}. 
Proof. 
    induction t; 
    try (left; constructor); 
    destruct IHt1; 
    right; intro C; inversion C. 
Qed. 

這樣你就可以考慮這兩種情況下可能證明normal_form_implies_value（與destruct），像這樣：

Lemma normal_form_implies_value : forall t, normal_form t -> is_value t. 
Proof. 
    induction t; 
    try constructor; 
    intros; 
    destruct (is_value_dec t1), t1; 
    apply False_ind; 
    apply H; 
    try (eexists; constructor; fail); 
    try (inversion i; fail). 
    contradict n; 
    apply IHt1; 
    intros [tt C]; 
    eauto using scomp. 
Qed. 

scomp是一個構造step，使用此定義：

Inductive step : term -> term -> Prop := 
| strue: forall t1 t2, step (ifthenelse true t1 t2) t1 
| sfalse: forall t1 t2, step (ifthenelse false t1 t2) t2 
| scomp: forall t1 t1' t2 t3, step t1 t1' -> 
      step (ifthenelse t1 t2 t3) (ifthenelse t1' t2 t3). 

Answer 2

一個有趣的定理，證明是反轉引理指出，如果ifthenelse b l r處於正常形式再等等都是b，l和r。

Lemma normal_form_ifthenelse (b l r : term) : 
    normal_form (ifthenelse b l r) -> 
    normal_form b /\ normal_form l /\ normal_form r. 

如果您願意使用自動化機械的大量幫助，那麼可以很容易地證明這一點。

Proof. 
    intros H  (* assumption "normal_form (ifthenelse b l r)" *) 
; repeat split (* split the big conjunction into 3 goals *) 
; intros [t redt] (* introduce the "exists t', step t t'" proofs 
         all the goals are now "False" *) 
; apply H   (* because we know that "step t t'", we are going to 
         be able to prove that "step (ifthenelse ...) ..." 
         which H says is impossible *) 
; eexists   (* we let Coq guess which term we are going to step to *) 
; constructor  (* we pick the appropriate constructor between the structural ones *) 
; eapply redt. (* finally we lookup the proof we were given earlier *) 
Qed. 

如果這是你有點過分自動化，您可以嘗試手動證明如下（簡單）引理，因爲它是位我們將需要在最終證明：

Lemma normal_form_ifthenelse (b l r : term) : 
    normal_form (ifthenelse b l r) -> normal_form b. 

然後可以很快證明您的引理：在引導的兩個第一種情況下，使用constructor將選擇合適的is_value構造函數。

在最後一節，我們提供了一個歸納假設​​說，只要t1是normal_form那麼is_value。我們可以使用我們的中間引理來證明normal_form t1基於我們知道normal_form (ifthenelse t1 t2 t3)並得出結論is_value t1的事實。

但事實證明，t1是一種價值相矛盾的事實normal_form (ifthenelse t1 t2 t3)：我們確實可以加強要麼t2或t3取決於t1是true或false。False_ind是我們說「的一種方式，現在我們得出了一個矛盾」。

Lemma normal_form_implies_value : forall t, normal_form t -> is_value t. 
Proof. 
intro t; induction t; intro ht. 
    - constructor. 
    - constructor. 
    - destruct (normal_form_ifthenelse _ _ _ ht) as [ht1 _]. 
    apply False_ind, ht; destruct (IHt1 ht1); eexists; constructor. 
Qed.