coq - Prop 和 Type 的不同归纳原则

Question

我注意到 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 的类型挂件:

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

Answer 1

注意:我将使用 _rect无处不在的原则，而不是 _ind , 自 _ind原则通常通过 _rect 实现那些。
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.

再次，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在 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

这样得到的归纳原理称为极大归纳原理。
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 所著的“交互式定理证明和程序开发(Coq'Art:归纳构造微积分)”一书的 14.1.3 ... 14.1.6(2004 年)。