Coq中HOL风格alpha转换的相等匹配合一问题

你给出的直接定义逻辑上要求t1和t2必须是同一个项才能成立：TRANS 公理要求两个输入证明的中间项必须统一，即第一个证明的右端点等于第二个证明的左端点。你传入的第一个证明是REFL t1（类型t1 == t1），第二个是REFL t2（类型t2 == t2），要求中间点同时等于t1和t2，也就是必须满足t1 = t2，没有这个前提的话类型永远无法统一，自然会报类型匹配错误。
HOL4中的ALPHA函数本身就作用于alpha等价的两个项，隐含了两个项语义相等的前提，所以你补充问题中提到的添加Coq标准相等假设的思路是完全正确的。

你之前的匹配写法报错有两个原因：

1. 定义中的类型参数T没有作为参数传入，属于自由变量
2. Coq默认不会自动把相等假设的作用扩散到分支内的变量类型，你需要显式给match加返回值注解，告诉Coq当H是eq_refl时，t2就等于t1，这时候REFL t2的类型会自动统一为t1 == t1，就能匹配TRANS的参数要求。

修复后的完整代码如下：

Axiom EQ : forall {aa:Type}, aa -> aa -> Prop.
Notation " x == y " := (@EQ _ x y)  (at level 80).
Axiom REFL : forall {aa:Type} (a:aa), a == a.
Axiom TRANS :forall {T:Type}{t1 t2 t3:T},
 (t1 == t2) -> (t2 == t3) -> (t1 == t3).

(* 显式注解match返回值的写法 *)
Definition ALPHA {T:Type} (t1 t2:T) (H:t1 = t2) : t1 == t2 :=
  match H in (_ = t2') return t1 == t2' with
  | eq_refl => TRANS (REFL t1) (REFL t1)
  end.

如果你一定要在分支里保留REFL t2的写法，可以用Program Definition让Coq自动处理相等上下文：

Program Definition ALPHA {T:Type} (t1 t2:T) (H:t1 = t2) : t1 == t2 :=
  match H with
  | eq_refl => TRANS (REFL t1) (REFL t2)
  end.

也可以用标准库的相等消去实现更简洁的写法，不需要显式写match：

Definition ALPHA {T} (t1 t2:T) (H:t1 = t2) : t1 == t2 :=
  eq_rect t1 (fun x => t1 == x) (REFL t1) t2 H.

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