Coqを使って "タイプとプログラミング言語"の定理3.5.4を証明する方法？

Question

更新：Arthur Azevedo De Amorimの助けを借りて、私はついにそれを管理します。コードは質問の最後に添付されています。

---

私は本 "タイプとプログラミング言語」を読んでいます、と私はのCoQを使用して、この本の中で、各定理（補題）を証明しようとしています。定理3.5.4になったとき、私はそれを試して管理できませんでした。ここに問題の説明があります。

ASTと小さな言語：

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

評価ルールは以下のとおりです。

1. if true then t2 else t3 -> t2 (eval_if_true) 
2. if false then t2 else t3 -> t3 (eval_if_false) 
3.    t1 -> t1' 
     ------------------------ (eval_if) 
     if t1 then t2 else t3 -> 
      if t1' then t2 else t3 

私が証明したい定理は次のとおりです。任意の時刻t1 t2のt3のため、与えられた時刻t1 - > t2からt1の - > t3であれば、t2 = t3となる。

そして、私は以下のようにコックを入力し、提案を構築する：

Inductive t : Type := 
| zhen (* represent true *) 
| jia (* represent false *) 
| if_stat : t -> t -> t -> t. 

Inductive eval_small_step : t -> t -> Prop := 
| ev_if_true : forall (t2 t3 : t), 
    eval_small_step (if_stat zhen t2 t3) t2 
| ev_if_false : forall (t2 t3 : t), 
    eval_small_step (if_stat jia t2 t3) t3 
| ev_if : forall (t1 t2 t3 t4 : t), 
    eval_small_step t1 t2 -> 
    eval_small_step (if_stat t1 t3 t4) (if_stat t2 t3 t4). 

Theorem determinacy : forall (t1 t2 t3 : t), 
    eval_small_step t1 t2 -> eval_small_step t1 t3 -> t2 = t3. 

そして、私は本の中で述べたようにeval_small_step t1 t2に誘導しようとしました。しかし、私は失敗しました：

Proof. 
    intros t1 t2 t3. 
    intros H1 H2. 
    induction H1. 
    - inversion H2. reflexivity. inversion H4. 
    - inversion H2. reflexivity. inversion H4. 
    - assert (H: eval_small_step (if_stat t1 t0 t4) (if_stat t2 t0 t4)). 
    { 
     apply ev_if. apply H1. 
    } 
    Abort. 

帰納仮説は一般的ではないため、私は失敗しました。

IHeval_small_step : eval_small_step t1 t3 -> t2 = t3 

私はこの証明を手伝ってもらえますか？

---

証明：

Inductive t : Type := 
| zhen (* represent true *) 
| jia (* represent false *) 
| if_stat : t -> t -> t -> t. 

Inductive eval_small_step : t -> t -> Prop := 
| ev_if_true : forall (t2 t3 : t), 
    eval_small_step (if_stat zhen t2 t3) t2 
| ev_if_false : forall (t2 t3 : t), 
    eval_small_step (if_stat jia t2 t3) t3 
| ev_if : forall (t1 t2 t3 t4 : t), 
    eval_small_step t1 t2 -> 
    eval_small_step (if_stat t1 t3 t4) (if_stat t2 t3 t4). 

Theorem determinacy : forall (t1 t2 t3 : t), 
    eval_small_step t1 t2 -> eval_small_step t1 t3 -> t2 = t3. 

Proof. 
    intros t1 t2 t3. 
    intros H1. 
    revert t3. 
    induction H1. 
    - intros t0. intros H. 
    inversion H. 
    + reflexivity. 
    + inversion H4. 
    - intros t0. intros H. 
    inversion H. 
    + reflexivity. 
    + inversion H4. 
    - intros t0. 
    intros H. 
    assert(H': eval_small_step (if_stat t1 t3 t4) (if_stat t2 t3 t4)). 
    { 
     apply ev_if. apply H1. 
    } 
    inversion H. 
    + rewrite <- H2 in H1. inversion H1. 
    + rewrite <- H2 in H1. inversion H1. 
    + assert(H'': t2 = t6). 
     { 
     apply IHeval_small_step. 
     apply H5. 
     } 
     rewrite H''. reflexivity. 
Qed. 

Answer 1

これは初心者のための典型的な罠です。誘導の前にt3を導入したので、誘導仮説は十分に一般的ではなく、t3を「すべての誘導ステップにわたって」固定するという効果があります。あなたのケースでは、​​を導入してH1を紹介して紹介する必要があるので、t3をrevertまたはgeneralize dependentの手法を使ってコンテキストに戻すことができます。単純にこのようなあなたの証明を始める：

Proof. 
    intros t1 t2 t3. 
    intros H1. 
    revert t3. 
    induction H1. (* ... *) 

この問題は、Software Foundations bookで説明されているが、単純に "generalize dependent"を検索してください。 （私はこの質問が既にスタックオーバーフローにも出てきたと確信していますが、誰かが助けようとしているなら、参照を見つけることができませんでした）