为什么我可以使用构造函数策略来证明自反性？

Question

构造函数策略允许您通过自动应用构造函数来实现归纳数据类型的目标。然而，定义相等在 Coq 中不是归纳产品。那么为什么 Coq 接受这个证明呢？

Example zeqz : 0 = 0. constructor.

Answer 1

Coq 中的相等类型定义如下

Inductive eq (A : Type) (x : A) : A -> Prop :=  
   eq_refl : x = x

也就是说它有一个自反性构造函数。

为了证明0 = 0你需要构造一个这种类型的术语。做到这一点的唯一方法是调用eq_refl. 然而，为了调用eq_refl类型检查器需要知道0可转换为0（即它们在定义上相等）。

类型eq是相等的语义概念，而定义相等是句法概念。这意味着证明助手无法区分定义相等的术语，但可以区分语义相等的术语。所以构造函数eq_refl可以被看作是定义（句法）相等包含语义相等的保证。

询问术语是否可以在语义上相等而不在句法上相等是富有成效的。这样的例子只能通过公理得到。例如，根据自然数的递归（nat_rec，或者更专业地说，nat_ind）的定义，或者通过外延公理。