如何弄清楚CoQ中不同类型的"="是什么意思

 等号符号只是eq谓词的特殊中缀语法。也许令人惊讶的是，它对每种类型的定义都是一样的，我们甚至可以要求Coq为我们打印它：

Print eq.
(* Answer: *)
Inductive eq (A : Type) (x : A) : Prop :=
| eq_refl : eq x x.

这个定义太小了，可能很难理解发生了什么。粗略地说，它说，证明两个表达式相等的最基本方法是通过自反性——也就是说，当它们完全相同时。例如，我们可以用eq_refl来证明5 = 5或[4] = [4]:

Check eq_refl : 5 = 5.
Check eq_refl : [4] = [4].

这个定义远不止眼前所见。首先，Coq认为在简化之前相等的任何两个表达式都是相等的。在这些情况下，我们可以使用eq_refl来证明它们也是相等的。例如：

Check eq_refl : 2 + 2 = 4.

这是因为Coq知道自然数上加法的定义，并且能够机械地简化表达式2 + 2，直到它到达4。

此外，上面的定义告诉我们如何使用平等来证明其他事实。由于归纳类型在Coq中的工作方式，我们可以显示以下结果：

eq_elim : 
forall (A : Type) (x y : A),
x = y ->
forall (P : A -> Prop), P x -> P y

换句话说，当两个事物相等时，任何成立第一个的事实也成立第二个。当您调用rewrite策略时，这个原则大致就是Coq在幕后使用的。

最后，平等以有趣的方式与其他类型相互作用。你问list的平等定义是什么。我们可以证明以下引理是有效的：

forall A (x1 x2 : A) (l1 l2 : list A),
x1 :: l1 = x2 :: l2 -> x1 = x2 / l1 = l2
forall A (x : A) (l : list A),
x :: l <> nil.

大写：

1. 如果两个非空列表相等，则它们的头和尾相等；

2. 非空列表不同于CCD_ 10。

更一般地说，如果T是一个归纳型，我们可以证明：

1. 如果以同一构造函数开头的两个表达式相等，则它们的参数相等(也就是说，构造函数是内射)；和

2. 以不同构造函数开头的两个表达式总是不同的(也就是说，不同的构造函数是不相交的)。

严格来说，这些事实不是平等定义的一部分，而是归纳类型在Coq中工作的结果。不幸的是，它不适用于Coq中的其他类型；特别是，Coq中函数相等的概念不是很有用，除非你愿意在理论中添加额外的公理。