如何弄清楚“=”在coq中不同类型的含义

Question

给定 Coq 中的一个类型（如 List），我如何弄清楚等号“=”在该类型中的含义？我应该输入什么命令来找出定义？

Answer 1

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

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

这个定义太小了，可能很难理解发生了什么。粗略地说，它表示证明两个表达式相等的最基本方法是 reflexivity —— 即当它们完全相同时。例如，我们可以使用 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.

换言之：

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

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

how to figure out what "=" means in different types in coq