0

我正在尝试在 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*)
4

2 回答 2

1

你能多说一下这个定义在 HOL 中应该如何工作吗？如果我猜ALPHA对了，如果它的参数不是 alpha 可转换的，那么它应该是一个无法进行类型检查的东西？在 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.
于 2021-11-11T23:21:46.280 回答
0

这不是一个统一问题，它确实是一个打字问题。 REFL t1有类型t1 == t1和REFL t2有类型t2 == t2，因为错误消息告诉你。传递性只有在某种程度上t1和t2相同的情况下才会起作用，但事实并非如此。

也许你写的不是你认为你写的。如果我们只使用t1，则TRANS (REFL t1) (REFL t1)有类型t1 == t1。你期待ALPHA t1 t2有 typet1 == t2吗？如果是这样，那么你的EQ关系将是全部的。

于 2021-11-11T12:42:09.050 回答