代码之家 › 专栏 › 技术社区 › Bob

归纳法原理`

parametric-polymorphism induction agda coq

Bob · 技术社区 · 5 年前

对于感应式 nat ,生成归纳原理使用构造器 O 和 S 在声明中:

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

nat_ind
 : forall P : nat -> Prop,
   P 0 ->
   (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

le ,生成的语句不使用构造函数 le_n 和 le_S :

Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m

le_ind
 : forall (n : nat) (P : nat -> Prop),
   P n ->
   (forall m : nat, n <= m -> P m -> P (S m)) ->
   forall n0 : nat, n <= n0 -> P n0

然而,它是有可能的陈述和证明一个归纳原理遵循相同的形状,为 纳特 :

Lemma le_ind' : forall n (P : forall m, le n m -> Prop),
P n (le_n n) ->
(forall m (p : le n m), P m p -> P (S m) (le_S n m p)) ->
forall m (p : le n m), P m p.
Proof.
fix H 6; intros; destruct p.
apply H0.
apply H1, H.
apply H0.
apply H1.
Qed.

1 回复 | 直到 5 年前

eponier 5 年前

可以使用命令为归纳类型手动生成归纳原理 Scheme (参见 documentation

该命令有两种风格:

Scheme scheme := Induction for Sort Prop 生成标准导入方案。
Scheme scheme := Minimality for Sort Prop 生成更适合归纳谓词的简化归纳方案。

如果你在 Type 生成归纳原理是第一类。如果你在 Prop

得到你想要的归纳原理 le 类型 :

Inductive le (n : nat) : nat -> Type :=
| le_n : le n n
| le_S : forall m : nat, le n m -> le n (S m).

Check le_ind.
(* forall (n : nat) (P : forall n0 : nat, le n n0 -> Prop),
   P n (le_n n) ->
   (forall (m : nat) (l : le n m), P m l -> P (S m) (le_S n m l)) ->
   forall (n0 : nat) (l : le n n0), P n0 l
*)

或者您可以手动要求Coq生成预期的归纳原理:

Inductive le (n : nat) : nat -> Prop :=
| le_n : le n n
| le_S : forall m : nat, le n m -> le n (S m).

Check le_ind.
(* forall (n : nat) (P : nat -> Prop),
   P n ->
   (forall m : nat, le n m -> P m -> P (S m)) ->
   forall n0 : nat, le n n0 -> P n0
*)

Scheme le_ind2 := Induction for le Sort Prop.
Check le_ind2.
(* forall (n : nat) (P : forall n0 : nat, le n n0 -> Prop),
   P n (le_n n) ->
   (forall (m : nat) (l : le n m), P m l -> P (S m) (le_S n m l)) ->
   forall (n0 : nat) (l : le n n0), P n0 l
*)

推荐文章

Mei Zhang · 定义“依赖类型”模函子

6 年前

Jason Hu · 参见Ltac中的Hintbase

6 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

6 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

6 年前

user9335697 · 实例化参数以评估函数定义

6 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

6 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

6 年前

jmite · Coq:在校样脚本编写期间查看校样术语

6 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

6 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

7 年前