Induction principle for le

Link:: https://stackoverflow.com/q/55196816

Display all goals and responses

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

Arguments S _%nat_scopenat_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

Arguments le (_ _)%nat_scope
Arguments le_n _%nat_scope
Arguments le_S (_ _)%nat_scope _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.forall (n : nat) (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p
Proof.forall (n : nat) (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p
  fix H 6.H: forall (n : nat)
  (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p
forall (n : nat) (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p intros.H: forall (n : nat)
  (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p
n: nat
P: forall m : nat, n <= m -> Prop
H0: P n (le_n n)
H1: forall (m : nat) (p : n <= m),
P m p -> P (S m) (le_S n m p)
m: nat
p: n <= m
P m p destruct p.H: forall (n : nat)
  (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p
n: nat
P: forall m : nat, n <= m -> Prop
H0: P n (le_n n)
H1: forall (m : nat) (p : n <= m),
P m p -> P (S m) (le_S n m p)
P n (le_n n)
H: forall (n : nat)
  (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p
n: nat
P: forall m : nat, n <= m -> Prop
H0: P n (le_n n)
H1: forall (m : nat) (p : n <= m),
P m p -> P (S m) (le_S n m p)
m: nat
p: n <= m
P (S m) (le_S n m p)
  -H: forall (n : nat)
  (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p
n: nat
P: forall m : nat, n <= m -> Prop
H0: P n (le_n n)
H1: forall (m : nat) (p : n <= m),
P m p -> P (S m) (le_S n m p)
P n (le_n n) apply H0.
  -H: forall (n : nat)
  (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p
n: nat
P: forall m : nat, n <= m -> Prop
H0: P n (le_n n)
H1: forall (m : nat) (p : n <= m),
P m p -> P (S m) (le_S n m p)
m: nat
p: n <= m
P (S m) (le_S n m p) apply H1, H.H: forall (n : nat)
  (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p
n: nat
P: forall m : nat, n <= m -> Prop
H0: P n (le_n n)
H1: forall (m : nat) (p : n <= m),
P m p -> P (S m) (le_S n m p)
m: nat
p: n <= m
P n (le_n n)
H: forall (n : nat)
  (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p
n: nat
P: forall m : nat, n <= m -> Prop
H0: P n (le_n n)
H1: forall (m : nat) (p : n <= m),
P m p -> P (S m) (le_S n m p)
m: nat
p: n <= m
forall (m : nat) (p : n <= m),
P m p -> P (S m) (le_S n m p) apply H0.H: forall (n : nat)
  (P : forall m : nat, n <= m -> Prop),
P n (le_n n) ->
(forall (m : nat) (p : n <= m),
 P m p -> P (S m) (le_S n m p)) ->
forall (m : nat) (p : n <= m), P m p
n: nat
P: forall m : nat, n <= m -> Prop
H0: P n (le_n n)
H1: forall (m : nat) (p : n <= m),
P m p -> P (S m) (le_S n m p)
m: nat
p: n <= m
forall (m : nat) (p : n <= m),
P m p -> P (S m) (le_S n m p) 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?

Answer

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.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.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.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