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 的 Type pendant:

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 个参数，因为 vec A n 中的 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é运行（2004 年）一书 "Interactive Theorem Proving and Program Development (Coq'Art: The Calculus of Inductive Constructions)" 的 14.1.3 ... 14.1.6。

Prop 和 Type 的不同归纳原理

Different induction principles for Prop and Type

coq

`eqT_rect`的类型

类型 `eq_rect`

如何生成最大归纳原理

参考资料

Prop 和 Type 的不同归纳原理

Different induction principles for Prop and Type

coq

eqT_rect的类型

类型 eq_rect

如何生成最大归纳原理

参考资料

`eqT_rect`的类型

类型 `eq_rect`