Software Foundations: Induction Principles

IndPrinciples.v

Theorem mult_0_r : forall n,
  n * 0 = 0.
Proof.
  apply nat_ind.
  - reflexivity.
  - intros.
    assumption.
Qed.

Theorem plus_1_r : forall n,
  n + 1 = S n.
Proof.
  apply nat_ind.
  - reflexivity.
  - intros. apply (@f_equal _ _ S) in H.
    assumption.
Qed.

Inductive tsil : Type :=
| lin : tsil
| snoc : nat -> tsil -> tsil.

(*
tsil_ind
     : forall P : tsil -> Prop,
       P lin ->
       (forall (n : nat) (t : tsil), P t -> P (snoc n t)) ->
       forall t : tsil, P t
*)
Check tsil_ind.

Inductive tree : Type :=
| empty : tree
| leaf : bool -> tree
| branch : bool -> tree -> tree -> tree.

(*
tree_ind
     : forall P : tree -> Prop,
       P empty ->
       (forall b : bool, P (leaf b)) ->
       (forall (b : bool) (t : tree),
        P t -> forall t0 : tree, P t0 -> P (branch b t t0)) ->
       forall t : tree, P t
*)
Check tree_ind.

Inductive ex : Type :=
| c1 : bool -> ex
| c2 : nat -> ex -> ex.

(*
ex_ind
     : forall P : ex -> Prop,
       (forall b : bool, P (c1 b)) ->
       (forall (n : nat) (e : ex), P e -> P (c2 n e)) ->
       forall e : ex, P ex
*)
Check ex_ind.

Module Polymorphism.

Inductive tree {A} : Type :=
| leaf : A -> tree
| node : tree -> tree -> tree.

(*
tree_ind
     : forall (A : Type) (P : tree -> Prop),
       (forall a : A, P (leaf a)) ->
       (forall t : tree, P t -> forall t0 : tree, P t0 -> P (node t t0)) ->
       forall t : tree, P t
*)
Check tree_ind.

Inductive foo {A B} : Type :=
| bar : A -> foo
| baz : B -> foo
| quxx : (nat -> foo) -> foo.

(*
foo_ind
     : forall (A B : Type) (P : foo -> Prop),
       (forall a : A, P (bar a)) ->
       (forall b : B, P (baz b)) ->
       (forall f1 : nat -> foo, (forall n : nat, P (f1 n)) -> P (quxx f1)) ->
       forall f2 : foo, P f2
*)
Check foo_ind.

Inductive list' {A} : Type :=
| nil' : list'
| cons' : list A -> list' -> list'.

(*
list'_ind
     : forall (A : Type) (P : list' -> Prop),
       P nil' ->
       (forall (l : list A) (l0 : list'), P l0 -> P (cons' l l0)) ->
       forall l : list', P l
*)
Check list'_ind.

End Polymorphism.

Definition P n := n * 0 = 0.

Theorem mult_0_r' : forall n,
  P n.
Proof.
  apply nat_ind.
  - reflexivity.
  - intros. assumption.
Qed.

Inductive even : nat -> Prop :=
| even_O : even 0
| even_S : forall n, even n -> even (S (S n)).

(*
even_ind
     : forall P : nat -> Prop,
       P 0 ->
       (forall n : nat, even n -> P n -> P (S (S n))) ->
       forall n : nat, even n -> P n
*)
Check even_ind.

Inductive even' : nat -> Type :=
| even'_O : even' 0
| even'_S : forall {n}, even' n -> even' (S (S n)).

(*
even'_ind
     : forall P : forall n : nat, even' n -> Prop,
       P 0 even'_O ->
       (forall (n : nat) (e : even' n), P n e -> P (S (S n)) (even'_S e)) ->
       forall (n : nat) (e : even' n), P n e
*)
Check even'_ind.

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

(*
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
*)
Check le_ind.

Inductive le' : nat -> nat -> Prop :=
| le'_n : forall n, le' n n
| le'_S : forall m n, le' n m -> le' n (S m).

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