如何使用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. (* ... *)

软件基础书中也解释了这个问题; 只需在generalize dependent那里查找" ".(我确信这个问题已经出现在Stack Overflow上,但如果有人愿意提供帮助,则无法找到参考.)