Induction principle for `le`

Question

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

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

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.

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?

I didn't understand this: the generated statement does not uses the constructors le_n and le_S. When doing induction on n <= m you do consider two cases: le_n and le_S. — user2956272
@dyukha I am talking about the statement (i.e. the type) of le_ind. You can clearly see that le_n and le_S do not occur. — Bob
Try to find access to "Interactive Theorem Proving and Program Development, CoqArt: The Calculus of Inductive Constructions" what you are asking for is described in chapt. 14. — Yves
I only found the French version online and Chapter 14 seems to be about coinduction. By the way, it is a pity that such a great book is not better publicized. — Bob

eponier eponier · Accepted Answer · 2019-04-04T16:14:50

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

The command comes in two flavours :

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.

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.

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

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

Induction principle for `le`

1 Answers