coq - 如何使用 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。

我在 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的作用“跨越所有诱导步骤”。在你的情况下，你需要介绍t3以便您介绍H1并对其进行归纳，因此您可以简单地输入 t3使用 revert 返回上下文或 generalize dependent策略。只需像这样开始你的证明:

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

这个问题在Software Foundations book中也有说明。 ;只需在那里查找“generalize dependent”。 (我确信这个问题也已经出现在 Stack Overflow 上，但如果有人愿意提供帮助，我找不到引用。)