我注意到 Coq 综合了关于 Prop 和 Type 等式的不同归纳原理。有人对此有解释吗？

平等定义为

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

与之相关的归纳原理有以下类型：

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

现在让我们定义一个 eq 的 Type 挂件：

Inductive eqT {A:Type}(x:A):A->Type:= eqT_refl: eqT x x.

自动生成归纳原理为

eqT_ind
 : forall (A : Type) (x : A) (P : forall a : A, eqT x a -> Prop),
   P x (eqT_refl x) -> forall (y : A) (e : eqT x y), P y e

Note: 我要用_rect原则无处不在，而不是_ind, since _ind原则通常通过_rect ones.

Type of eqT_rect

让我们看一下谓词P。 当处理归纳族时，参数的数量P等于数量非参数参数（索引）+ 1。

让我举一些例子（可以很容易地跳过）。

• 自然数根本没有参数：

  Inductive nat : Set :=  O : nat | S : nat -> nat.
  

  所以，谓词P将是类型nat -> Type.

• 列表有一个参数参数 (A):

  Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A.
  

  Again, P只有一个参数：P : list A -> Type.

• 向量则不同：

  Inductive vec (A : Type) : nat -> Type :=
    nil : vec A 0
  | cons : A -> forall n : nat, vec A n -> vec A (S n).
  

  P有 2 个参数，因为n in vec A n是一个非参数参数：

  P : forall n : nat, vec A n -> Type
  

以上解释了eqT_rect（而且当然，eqT_ind结果），因为之后的论证(x : A)是非参数的，P有 2 个参数：

P : forall a : A, eqT x a -> Type

这证明了整体类型的合理性eqT_rect:

eqT_rect
     : forall (A : Type) (x : A) (P : forall a : A, eqT x a -> Type),
       P x (eqT_refl x) -> forall (y : A) (e : eqT x y), P y e

这样得到的归纳原理称为最大归纳原理.

Type of eq_rect

归纳谓词的生成归纳原则（例如eq）被简化为表达证明无关性（术语是简化归纳原理).

定义谓词时P，Coq 只是删除谓词的最后一个参数（这是正在定义的类型，它位于Prop）。这就是为什么使用谓词eq_rect是一元的。这一事实塑造了eq_rect:

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

如何产生极大归纳原理

我们还可以让 Coq 生成非简化归纳原理eq:

Scheme eq_rect_max := Induction for eq Sort Type.

结果类型是

eq_rect_max :
  forall (A : Type) (x : A) (P : forall a : A, x = a -> Type),
         P x eq_refl -> forall (y : A) (e : x = y), P y e

它的结构与eqT_rect.

参考

更详细的解释参见章节。 Bertot 和 Castéran (2004) 所著的《交互式定理证明和程序开发（Coq'Art：归纳构造微积分）》一书的 14.1.3 ... 14.1.6。