le的归纳原理 [英] Induction principle for `le`

问题描述

对于归纳类型nat，生成的归纳原理在其语句中使用构造函数O和S:

For the inductive type nat, the generated induction principle uses the constructors O and S in its statement:

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:

But for le, the generated statement does not uses the constructors le_n and 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相同的形状的归纳原理:

However it is possible to state and prove an induction principle following the same shape as the one for 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之类的其他证明助手又如何呢?

I guess the generated one is more convenient. But how does Coq chooses the shape for its generated induction principle? If there is any rule, I cannot find them in the reference manual. What about other proof assistants such as Agda?

推荐答案

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

You can manually generate an induction principle for an inductive type by using the command Scheme (see the documentation).

命令有两种形式:

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

• Scheme scheme := Induction for Sort Prop generates the standard induction scheme.
• Scheme scheme := Minimality for Sort Prop generates a simplified induction scheme more suited to inductive predicates.

如果在Type中定义归纳类型，则生成的归纳原理是第一类.如果在Prop中定义归纳类型(即归纳谓词)，则生成的归纳原理是第二种.

If you define an inductive type in Type, the generated induction principle is of the first kind. If you define an inductive type in Prop (i.e. an inductive predicate), the generated induction principle is of the second kind.

要获得在le情况下所需的归纳原理，可以在Type中对其进行定义:

To obtain the induction principle that you want in the case of le, you can define it in 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生成预期的归纳原理:

or you can manually ask Coq to generate the expected induction principle:

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
*)

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