道具和类型的不同归纳原理 [英] Different induction principles for Prop and Type

问题描述

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

I noticed that Coq synthesizes different induction principles on equality for Prop and Type. Does anybody have an explanation for that?

等式定义为

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

并且相关的归纳原理具有以下类型：

And the associated induction principle has the following type:

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

现在让我们定义eq的Type垂饰：

Now let's define a Type pendant of 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

推荐答案

注意：我将在各处使用 _rect 原理，而不是 _ind ，因为 _ind 原则通常是通过 _rect 原则实现的。

Note: I'm going to use _rect principles everywhere instead of _ind, since _ind principles are usually implemented via the _rect ones.

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

Let's take a look at the predicate P. When dealing with inductive families, the number of arguments of P is equal to the number of non-parametric arguments (indices) + 1.

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

Let me give some examples (they can be easily skipped).

• 自然数根本没有参数：

• Natural numbers don't have parameters at all:

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

因此，谓词 P 为键入 nat->键入。

列表具有一个参数自变量（ A ）：

Lists have one parametric argument (A):

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

再次， P 仅具有一个参数： P：列表A->键入。

Again, P has only one argument: 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中的c $ c> n A n 是一个非参数参数：

P has 2 arguments, because n in vec A n is a non-parameteric argument:

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

上面的内容解释了 eqT_rect （当然还有 eqT_ind ），因为自变量（x：A）是非参数的， P 有2个参数：

The above explains eqT_rect (and, of course, eqT_ind as a consequence), since the argument after (x : A) is non-parametric, P has 2 arguments:

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

可以证明 eqT_rect 的总体类型是合理的：

which justifies the overall type for 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

在此获得的归纳原理这种方式称为最大归纳原理。

The induction principle obtained in this way is called a maximal induction principle.

简化生成的归纳谓词归纳原理（例如 eq ）以表示不相关的证明（该术语为简化的归纳原理）。

The generated induction principles for inductive predicates (such as eq) are simplified to express proof irrelevance (the term for this is simplified induction principle).

在定义谓词 P 时，Coq只会删除最后一个参数谓词（定义的类型，位于 Prop 中）。这就是为什么 eq_rect 中使用谓词的原因。这个事实决定了 eq_rect 的类型：

When defining a predicate P, Coq simply drops the last argument of the predicate (which is the type being defined, and it lives in Prop). That's why the predicate used in eq_rect is unary. This fact shapes the type of eq_rect:

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

如何生成最大归纳原理

我们也可以让Coq为 eq 生成非简化的归纳原理：

How to generate maximal induction principle

We can also make Coq generate non-simplified induction principle for 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。

For more detailed explanation see sect. 14.1.3 ... 14.1.6 of the book "Interactive Theorem Proving and Program Development (Coq'Art: The Calculus of Inductive Constructions)" by Bertot and Castéran (2004).

这篇关于道具和类型的不同归纳原理的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！