如何用Coq证明《Types and Programming Languages》定理3.5.4？

Question

更新：在 Arthur Azevedo De Amorim 的帮助下，我终于成功了。问题最后附上代码

我正在看《Types and Programming Languages》这本书，我正在尝试用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。

我在 Coq 中构建类型和命题如下：

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 "across all induction steps" 的效果。在你的情况下，你需要引入 t3 以便你可以引入 H1 并对其进行归纳，因此你可以使用 revert 简单地将 t3 放回上下文中或 generalize dependent 策略。只需像这样开始您的证明：

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

这个问题在Software Foundations book中也有解释；只需在那里查找“generalize dependent”。（我确信这个问题也已经出现在 Stack Overflow 上，但找不到参考，如果有人愿意提供帮助的话。）

如何用Coq证明《Types and Programming Languages》定理3.5.4？

how to prove Theorem 3.5.4 in 《Types and Programming Languages》using Coq?

proof

coq