我注意到 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
注意：我将_rect在各处使用原则而不是_ind，因为_ind原则通常是通过_rect原则来实现的。
eqT_rect让我们看一下谓词P。\n处理归纳族时，参数的数量P等于非参数的数量参数（索引）的数量 + 1。
让我举一些例子（可以很容易地跳过）。
\n\n自然数根本没有参数：
\n\nInductive nat : Set := O : nat | S : nat -> nat.\n因此，谓词的P类型为nat -> Type。
列表有一个参数 ( A)：
Inductive list (A : Type) : Type :=\n nil : list A | cons : A -> list A -> list A.\n同样，P只有一个参数：P : list A -> Type。
向量则不同：
\n\nInductive vec (A : Type) : nat -> Type :=\n nil : vec A 0\n| cons : A -> forall n : nat, vec A n -> vec A (S n).\nP有 2 个参数，因为ninvec A n是非参数参数：
P : forall n : nat, vec A n -> Type\n上面解释了eqT_rect（当然，因此eqT_ind），因为后面的参数(x : A)是非参数的，P所以有 2 个参数：
P : forall a : A, eqT x a -> Type\n这证明了整体类型的合理性eqT_rect：
eqT_rect\n : forall (A : Type) (x : A) (P : forall a : A, eqT x a -> Type),\n P x (eqT_refl x) -> forall (y : A) (e : eqT x y), P y e\n这样得到的归纳原理称为最大归纳原理。
\n\neq_rect归纳谓词的生成归纳原理（例如eq）被简化以表达证明无关性（术语是简化归纳原理）。
当定义谓词 时P，Coq 只是删除谓词的最后一个参数（这是正在定义的类型，它位于 中Prop）。这就是为什么 中 使用的谓词eq_rect是一元的。这一事实塑造了以下类型eq_rect：
eq_rect : \n forall (A : Type) (x : A) (P : A -> Type),\n P x -> forall y : A, x = y -> P y\n我们还可以让 Coq 生成 的非简化归纳原理eq：
Scheme eq_rect_max := Induction for eq Sort Type.\n结果类型是
\n\neq_rect_max :\n forall (A : Type) (x : A) (P : forall a : A, x = a -> Type),\n P x eq_refl -> forall (y : A) (e : x = y), P y e\n并且它的结构与 相同eqT_rect。
更详细的解释参见章节。Bertot 和 Cast\xc3\xa9ran (2004) 所著的《交互式定理证明和程序开发（Coq\'Art：归纳构造微积分）》一书的 14.1.3 ... 14.1.6。
\n| 归档时间： |
|
| 查看次数： |
474 次 |
| 最近记录： |