coq - `le` 的归纳原理
问题描述
对于归纳类型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
然而,可以陈述和证明遵循与 相同形状的归纳原理nat
:
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.
我想生成的更方便。但是 Coq 是如何为其生成的归纳原理选择形状的呢?如果有任何规则,我在参考手册中找不到它们。Agda 等其他证明助手呢?
解决方案
您可以使用命令手动生成归纳类型的归纳原理Scheme
(请参阅文档)。
该命令有两种形式:
Scheme scheme := Induction for Sort Prop
生成标准归纳方案。Scheme scheme := Minimality for Sort Prop
生成更适合归纳谓词的简化归纳方案。
如果在 中定义归纳类型Type
,则生成的归纳原理属于第一类。如果在中定义了一个归纳类型Prop
(即一个归纳谓词),则生成的归纳原理属于第二种。
要在 的情况下获得您想要的归纳原理,le
您可以在 中定义它Type
:
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
*)
推荐阅读
- sql - 使用 SQL 列表中的变量运行 for 循环
- javascript - Laravel Fav/Unfav 功能,实现 ajax
- html - 当它们之间没有空格时,为什么不回绕到下一行
- php - 通过 Ruby/other 访问 Filemaker 13 Pro 数据库
- javascript - 从服务器 nginx+php-fpm 获取下载文件
- python - itertools.product 和列表理解之间的性能差异
- java - 如何将 json 数组从 recyclerView 传递到另一个活动
- javascript - 如何在js中创建对象到数组
- reactjs - 无法使用“useContext”挂钩破坏上下文提供程序中传递的值
- python - 将特征值传递给子工厂 Django