Coq 中 HOL 式 alpha 转换的统一问题（匹配等式）

Question

我正在尝试在 Coq 中嵌入 HOL4 证明的可能性。

在 HOL 中可以给出这样的定义

fun ALPHA t1 t2 = TRANS (REFL t1) (REFL t2)

是否可以用类似的方式在 Coq 中定义这个函数？由于

，我在最后一行的尝试失败了

The term "REFL t2" has type "t2 == t2"
while it is expected to have type "t1 == ?t3" (cannot unify 
"t2" and "t1").

代码：

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).
Definition ALPHA t1 t2 := TRANS (REFL t1) (REFL t2).

已添加：也许有一种定义 ALPHA 的方法，我们可以假设 t1=t2？（我的意思是，在 Coq 的标准平等意义上）。我无法添加假设 (H:t1=t2)，但我需要以某种方式进行匹配。如何进行相等匹配？

Definition ALPHA (t1 t2:T) (H:t1=t2) : t1==t2 :=
match H with
| eq_refl _ => TRANS (REFL t1) (REFL t2)
end
. (*fails*)

Answer 1

这不是一个统一问题，它确实是一个打字问题。 REFL t1 的类型为 t1 == t1，REFL t2 的类型为 t2 == t2，正如错误消息告诉您的那样。传递性只有在 t1 和 t2 相同的情况下才有效，但事实并非如此。

也许你写的不是你认为的那样。如果我们只使用 t1，那么 TRANS (REFL t1) (REFL t1) 的类型是 t1 == t1。您是否期望 ALPHA t1 t2 具有类型 t1 == t2？如果是这样，那么您的 EQ 关系将是完整的。

Answer 2

您能详细说明一下这个定义在 HOL 中应该如何运作吗？如果我猜对了，ALPHA 如果它的参数不是 alpha-convertible，它应该是一个无法进行类型检查的东西？在 Coq 中，你可以使用

Notation ALPHA t1 t2 := (TRANS (REFL t1) (REFL t2)).

你也可以

Notation ALPHA t1 t2 := (REFL t1 : t1 == t2).

或

Notation ALPHA t1 t2 := (eq_refl : t1 = t2).

那你可以写成Check ALPHA foo bar之类的，看看两个东西是不是可以转换的。但我认为这在大多数情况下都没有用。如果您正在寻找战术编程，也许您正在寻找 unify 战术或 constr_eq 战术？

或者，如果您希望 match 语句起作用，您可以编写

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

Coq 中 HOL 式 alpha 转换的统一问题（匹配等式）

Unification problem with HOL-style alpha-conversion in Coq (matching the equality)

coq

hol