IndPrinciplesInduction Principles
Check nat_ind :
∀ P : nat → Prop,
P 0 →
(∀ n : nat, P n → P (S n)) →
∀ n : nat, P n.
∀ P : nat → Prop,
P 0 →
(∀ n : nat, P n → P (S n)) →
∀ 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:
We can directly use the induction principle with apply:
- P holds of 0
- for any n, if P holds of n, then P holds of S n.
Theorem mul_0_r' : ∀ n:nat,
n × 0 = 0.
Proof.
apply nat_ind.
- (* n = O *) reflexivity.
- (* n = S n' *) simpl. intros n' IHn'. rewrite → IHn'.
reflexivity. Qed.
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:
If we define type t with constructors c1 ... cn,
Coq generates:
t_ind : ∀ P : t → Prop,
... case for c1 ... →
... case for c2 ... → ...
... case for cn ... →
∀ n : t, P n The specific shape of each case depends on the arguments to the corresponding constructor.
An example with no constructor arguments:
- 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.
Coq generates induction principles for every datatype defined with Inductive, including those that aren't recursive.
t_ind : ∀ P : t → Prop,
... case for c1 ... →
... case for c2 ... → ...
... case for cn ... →
∀ n : t, P n The specific shape of each case depends on the arguments to the corresponding constructor.
Inductive time : Type :=
| day
| night.
Check time_ind :
∀ P : time → Prop,
P day →
P night →
∀ t : time, P t.
| day
| night.
Check time_ind :
∀ P : time → Prop,
P day →
P night →
∀ t : time, P t.
Inductive natlist : Type :=
| nnil
| ncons (n : nat) (l : natlist).
Check natlist_ind :
∀ P : natlist → Prop,
P nnil →
(∀ (n : nat) (l : natlist),
P l → P (ncons n l)) →
∀ l : natlist, P l.
| nnil
| ncons (n : nat) (l : natlist).
Check natlist_ind :
∀ P : natlist → Prop,
P nnil →
(∀ (n : nat) (l : natlist),
P l → P (ncons n l)) →
∀ l : natlist, P l.
- 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]" But that oversimplifies a little. An assumption about P holding of an argument x of type t actually occurs immediately after the quantification of x.
Inductive natlist' : Type :=
| nnil'
| nsnoc (l : natlist') (n : nat).
| nnil'
| nsnoc (l : natlist') (n : nat).
Now the induction principle case for nsnoc1 is a bit different
than the earlier case for ncons:
Check natlist'_ind :
∀ P : natlist' → Prop,
P nnil' →
(∀ l : natlist', P l → ∀ n : nat, P (nsnoc l n)) →
∀ n : natlist', P n.
∀ P : natlist' → Prop,
P nnil' →
(∀ l : natlist', P l → ∀ n : nat, P (nsnoc l n)) →
∀ n : natlist', P n.
Induction Principles for Propositions
Print ev.
(* ===>
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)))
*)
Check ev_ind :
∀ P : nat → Prop,
P 0 →
(∀ n : nat, ev n → P n → P (S (S n))) →
∀ n : nat, ev n → P n.
(* ===>
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)))
*)
Check ev_ind :
∀ P : nat → Prop,
P 0 →
(∀ n : nat, ev n → P n → P (S (S n))) →
∀ n : nat, ev n → P n.
In English, ev_ind says: Suppose P is a property of natural
numbers. 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 : ∀ n, le1 n n
| le1_S : ∀ n m, (le1 n m) → (le1 n (S m)).
Notation "m <=1 n" := (le1 m n) (at level 70).
| le1_n : ∀ n, le1 n n
| le1_S : ∀ n m, (le1 n m) → (le1 n (S m)).
Notation "m <=1 n" := (le1 m n) (at level 70).
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).
| 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 :
∀ P : nat → nat → Prop,
(∀ n : nat, P n n) →
(∀ n m : nat, n <=1 m → P n m → P n (S m)) →
∀ n n0 : nat, n <=1 n0 → P n n0.
Check le2_ind :
∀ (n : nat) (P : nat → Prop),
P n →
(∀ m : nat, n <=2 m → P m → P (S m)) →
∀ n0 : nat, n <=2 n0 → P n0.
∀ P : nat → nat → Prop,
(∀ n : nat, P n n) →
(∀ n m : nat, n <=1 m → P n m → P n (S m)) →
∀ n n0 : nat, n <=1 n0 → P n n0.
Check le2_ind :
∀ (n : nat) (P : nat → Prop),
P n →
(∀ m : nat, n <=2 m → P m → P (S m)) →
∀ n0 : nat, n <=2 n0 → P n0.
The latter is simpler, and corresponds to Coq's own
definition.
Explicit Proof Objects for Induction (Optional)
Check nat_ind :
∀ P : nat → Prop,
P 0 →
(∀ n : nat, P n → P (S n)) →
∀ n : nat, P n.
∀ P : nat → Prop,
P 0 →
(∀ n : nat, P n → P (S n)) →
∀ n : nat, P n.
There's nothing magic about this induction lemma: it's just
another Coq lemma that requires a proof. Coq generates the proof
automatically too...
Print nat_ind.
We can rewrite that more tidily as follows:
Fixpoint build_proof
(P : nat → Prop)
(evPO : P 0)
(evPS : ∀ n : nat, P n → P (S n))
(n : nat) : P n :=
match n with
| 0 ⇒ evPO
| S k ⇒ evPS k (build_proof P evPO evPS k)
end.
Definition nat_ind_tidy := build_proof.
(P : nat → Prop)
(evPO : P 0)
(evPS : ∀ n : nat, P n → P (S n))
(n : nat) : P n :=
match n with
| 0 ⇒ evPO
| S k ⇒ evPS k (build_proof P evPO evPS k)
end.
Definition nat_ind_tidy := build_proof.
Recursive function build_proof thus pattern matches against
n, recursing all the way down to 0, and building up a proof
as it returns.
We can also define non-standard induction principles
in this style. Recall this troublesome thoerem:
Lemma even_ev : ∀ n: nat, even n = true → ev n.
Proof.
induction n; intros.
- apply ev_0.
- destruct n.
+ simpl in H. inversion H.
+ simpl in H.
apply ev_SS.
Abort.
Proof.
induction n; intros.
- apply ev_0.
- destruct n.
+ simpl in H. inversion H.
+ simpl in H.
apply ev_SS.
Abort.
Attempts to prove this by standard induction on n fail in the case for
S (S n), because the induction hypothesis only tells us something about
S n, which is useless. There are various ways to hack around this problem;
for example, we can use ordinary induction on n to prove this (try it!):
Lemma even_ev' : ∀ n : nat,
(even n = true → ev n) ∧ (even (S n) = true → ev (S n)).
But we can make a much better proof by defining and proving a
non-standard induction principle that goes "by twos":
Definition nat_ind2 :
∀ (P : nat → Prop),
P 0 →
P 1 →
(∀ n : nat, P n → P (S(S n))) →
∀ n : nat , P n :=
fun P ⇒ fun P0 ⇒ fun P1 ⇒ fun PSS ⇒
fix f (n:nat) := match n with
0 ⇒ P0
| 1 ⇒ P1
| S (S n') ⇒ PSS n' (f n')
end.
∀ (P : nat → Prop),
P 0 →
P 1 →
(∀ n : nat, P n → P (S(S n))) →
∀ n : nat , P n :=
fun P ⇒ fun P0 ⇒ fun P1 ⇒ fun PSS ⇒
fix f (n:nat) := match n with
0 ⇒ P0
| 1 ⇒ P1
| S (S n') ⇒ PSS n' (f n')
end.
Once you get the hang of it, it is entirely straightforward to
give an explicit proof term for induction principles like this.
Proving this as a lemma using tactics is much less intuitive.
The induction ... using tactic variant gives a convenient way to
utilize a non-standard induction principle like this.
Lemma even_ev : ∀ n, even n = true → ev n.
Proof.
intros.
induction n as [ | |n'] using nat_ind2.
- apply ev_0.
- simpl in H.
inversion H.
- simpl in H.
apply ev_SS.
apply IHn'.
apply H.
Qed.
Proof.
intros.
induction n as [ | |n'] using nat_ind2.
- apply ev_0.
- simpl in H.
inversion H.
- simpl in H.
apply ev_SS.
apply IHn'.
apply H.
Qed.