lambda 演算定理

Question

我必须解决这个练习：

制定并证明 lambda 演算的汇合定理（即证明如果 λ 表达式 e 都约简为 e1 和 e2，则存在 e' 使得 e1 和 e2 约简为 e'）。

这就是我的方法：

Notation "'λ' x , t" := (t_abs x t) (at level 60).
Notation "t1 @ t2" := (t_app t1 t2) (at level 50, left associativity).
Fixpoint subst (t : Term) (x : string) (s : Term) : Term :=
  match t with
  | t_var y => if String.eqb x y then s else t
  | t_abs y t1 => if String.eqb x y then t_abs y t1 else t_abs y (subst t1 x s)
  | t_app t1 t2 => t_app (subst t1 x s) (subst t2 x s)
  end.

Inductive beta_reduction : Term → Term → Prop :=
| beta_step : forall x t1 t2,
    beta_reduction (t_abs x t1 @ t2) (subst t1 x t2)
| beta_left : forall t1 t2 t1',
    beta_reduction t1 t1' → beta_reduction (t_app t1 t2) (t_app t1' t2)
| beta_right : forall t1 t2 t2',
    beta_reduction t2 t2' → beta_reduction (t_app t1 t2) (t_app t1 t2').
Inductive beta_reduction_star : Term → Term → Prop :=
| beta_refl : forall t, beta_reduction_star t t
| beta_trans : forall t1 t2 t3,
    beta_reduction t1 t2 → beta_reduction_star t2 t3 → beta_reduction_star t1 t3.
Lemma confluence : forall t t1 t2,
  beta_reduction_star t t1 →
  beta_reduction_star t t2 →
  exists t', beta_reduction_star t1 t' ∧ beta_reduction_star t2 t'.
Proof.
  intros t t1 t2 H1 H2.
  induction H1 as [| t t0 t1 H Hstar IH].
  - (* cazul de bază: t1 = t *)
    exists t2.
    split.
    + exact H2.
    + apply beta_refl.
  - assert (beta_reduction_star t0 t2) as Hstep.
    {
      apply beta_trans with (t2 := t).
      - exact H. (* here is the problem *)
      - exact H2.
    }
    destruct (IH Hstep) as [t' [H3 H4]].
    exists t'.
    split.
    + apply beta_trans with (t2 := t0).
      * exact Hstar. (* t0 ->* t1 *)
      * exact H3.    (* t1 ->* t' *)
    + exact H4. (* t2 ->* t' *)
Qed.

问题是我收到此错误：

In environment
t2, t, t0, t1 : Term
H : beta_reduction t t0
Hstar : beta_reduction_star t0 t1
H2 : beta_reduction_star t t2
IH : beta_reduction_star t0 t2 → ∃ t' : Term, beta_reduction_star t1 t' ∧ beta_reduction_star t2 t'
The term "H" has type "beta_reduction t t0" while it is expected to have type "beta_reduction t0 t".

我在产生错误的断行代码旁边添加了注释。

• 精确的H。（*这就是问题*）

Answer 1

顺便说一句，您的替换代码不正确，因为它不是“捕获避免”！我可以建议改用 De Bruijn 处理活页夹吗？