(** * IndPrinciples: Induction Principles *)
(** With the Curry-Howard correspondence and its realization in Coq in
mind, we can now take a deeper look at induction principles. *)
Set Warnings "-notation-overridden,-parsing".
From LF Require Export ProofObjects.
(* ################################################################# *)
(** * Basics *)
(** The automatically generated _induction principle_ for [nat]: *)
Check nat_ind.
(* ===> nat_ind :
forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n *)
(** In English: Suppose [P] is a property of natural numbers (that is,
[P n] is a [Prop] for every [n]). To show that [P n] holds of all
[n], it suffices to show:
- [P] holds of [0]
- for any [n], if [P] holds of [n], then [P] holds of [S n]. *)
(** We can directly use the induction principle with [apply]: *)
Theorem mult_0_r' : forall n:nat,
n * 0 = 0.
Proof.
apply nat_ind.
- (* n = O *) reflexivity.
- (* n = S n' *) simpl. intros n' IHn'. rewrite -> IHn'.
reflexivity. Qed.
(** Why the [induction] tactic is nicer than [apply]:
- [apply] requires extra manual bookkeeping (the [intros] in the
inductive case)
- [apply] requires [n] to be left universally quantified
- [apply] requires us to manually specify the name of the induction
principle. *)
(** If we define type [t] with constructors [c1] ... [cn],
Coq generates:
t_ind : forall P : t -> Prop,
... case for c1 ... ->
... case for c2 ... -> ...
... case for cn ... ->
forall n : t, P n
The specific shape of each case depends on the arguments to the
corresponding constructor. *)
(** An example with no constructor arguments: *)
Inductive time : Type :=
| day
| night.
Check time_ind.
(* ===> time_ind : forall P : time -> Prop,
P day ->
P night ->
forall t : time, P t *)
(** An example with constructor arguments: *)
Inductive natlist : Type :=
| nnil
| ncons (n : nat) (l : natlist).
Check natlist_ind.
(* ===>
natlist_ind :
forall P : natlist -> Prop,
P nnil ->
(forall (n : nat) (l : natlist),
P l -> P (ncons n l)) ->
forall n : natlist, P n *)
(** In general, the automatically generated induction principle for
inductive type [t] is formed as follows:
- Each constructor [c] generates one case of the principle.
- If [c] takes no arguments, that case is:
"P holds of c"
- If [c] takes arguments [x1:a1] ... [xn:an], that case is:
"For all x1:a1 ... xn:an,
if [P] holds of each of the arguments of type [t],
then [P] holds of [c x1 ... xn]"
*)
(* ################################################################# *)
(** * Induction Principles in [Prop] *)
(** Coq also automatically produces induction priniciples for
inductive propositions: *)
Print even.
(* ===>
Inductive even : nat -> Prop :=
| ev_0 : even 0
| ev_SS : forall n : nat, even n -> even (S (S n))
*)
Check even_ind.
(* ===> 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 *)
(** In English, [even_ind] says: Suppose [P] is a property of natural
numbers (that is, [P n] is a [Prop] for every [n]). To show that [P n]
holds whenever [n] is even, it suffices to show:
- [P] holds for [0],
- for any [n], if [n] is even and [P] holds for [n], then [P]
holds for [S (S n)]. *)
(** The precise form of an [Inductive] definition can affect the
induction principle Coq generates. *)
Inductive le1 : nat -> nat -> Prop :=
| le1_n : forall n, le1 n n
| le1_S : forall n m, (le1 n m) -> (le1 n (S m)).
Notation "m <=1 n" := (le1 m n) (at level 70).
(** [n] could instead be a parameter: *)
Inductive le2 (n:nat) : nat -> Prop :=
| le2_n : le2 n n
| le2_S m (H : le2 n m) : le2 n (S m).
Notation "m <=2 n" := (le2 m n) (at level 70).
Check le1_ind.
(* ===> forall P : nat -> nat -> Prop,
(forall n : nat, P n n) ->
(forall n m : nat, n <=1 m -> P n m -> P n (S m)) ->
forall n n0 : nat, n <=1 n0 -> P n n0 *)
Check le2_ind.
(* ===> forall (n : nat) (P : nat -> Prop),
P n ->
(forall m : nat, n <=2 m -> P m -> P (S m)) ->
forall n0 : nat, n <=2 n0 -> P n0 *)
(** The latter is simpler, and corresponds to Coq's own
definition. *)