Lambda演算汇合性定理Coq证明报错排查

问题核心 #

在证明Lambda演算汇合性（Church-Rosser定理）时，调用beta_trans传递性引理出现类型错误：当前假设H : beta_reduction t t0，但引理要求的前提类型是beta_reduction t0 t。

原因分析 #

1. 传递性引理的参数顺序：
   标准的beta归约传递性引理beta_trans定义为：

   Lemma beta_trans : forall t1 t2 t3, beta_reduction t1 t2 -> beta_reduction t2 t3 -> beta_reduction t1 t3.
   

   即要求第一个前提是左项归约到中间项，第二个前提是中间项归约到右项，最终得到左项到右项的归约。报错说明你调用时颠倒了前提的方向，或是错误地要求了反向归约的前提。

2. 归约方向混淆：
   汇合性定理针对的是beta收缩（从含redex的项化简为更简单的项），而非beta展开。如果误将展开操作当作归约，会导致归约方向完全颠倒，引发类型不匹配。

解决方案 #

1. 确认并匹配引理的参数顺序 #

先核对你的beta_trans定义是否符合标准的左到右传递逻辑。如果是标准定义，调用时需保证前提顺序正确：

• 若有H : beta_reduction t t0（t一步归约到t0），则需要另一个前提H' : beta_reduction t0 e'（t0一步归约到e'），再通过beta_trans得到t到e'的归约：

  apply beta_trans with (t2 := t0); exact H; exact H'.
  

2. 引入反向传递引理（若需反向推理） #

如果证明中确实需要反向的传递逻辑（比如处理对称分支），可以单独证明一个反向传递引理：

Lemma beta_trans_rev : forall t1 t2 t3, beta_reduction t2 t1 -> beta_reduction t3 t2 -> beta_reduction t3 t1.
Proof.
  intros t1 t2 t3 H1 H2.
  apply beta_trans with (t2 := t2); exact H2; exact H1.
Qed.

之后在需要反向传递的场景调用beta_trans_rev即可。

3. 梳理汇合性证明的结构 #

汇合性定理的标准证明通常依赖并行归约或Tait-Martin-Löf方法，而非直接嵌套单步传递性。如果你的证明逻辑是直接组合单步归约路径，可能需要切换到多步归约（beta_reduction_star）的传递性：

Lemma beta_star_trans : forall t1 t2 t3, beta_reduction_star t1 t2 -> beta_reduction_star t2 t3 -> beta_reduction_star t1 t3.

多步归约的传递性更适合汇合性定理中“任意多步归约到e1和e2”的场景。

内容的提问来源于stack exchange，提问作者Vlad