(* This time, we prove forall n, 0 <= n by proving the principal premises first. *)
(* Before we prove the principal premises, though, we need to figure out how to express
the property we're proving. *)
Definition O_le := fun n => 0 <= n.
(* Now we prove the principal premises. The first is easy. *)
Lemma O_le_O : O_le 0.
Proof.
apply le_n.
Qed.
(* The second principle premise is not so hard either. *)
Lemma n_le_Sn : forall n, O_le n -> O_le (S n).
Proof.
(* To help us keep track of what's going on we can choose to replace O_le with its
definition. *)
unfold O_le in *.
apply le_S.
Qed.
(* Now we can proceed to prove our goal using nat_ind. *)
(* First we check nat_ind to remind us what the its arguments are. *)
Check nat_ind.
Goal forall n, 0 <= n.
Proof.
apply nat_ind.
apply O_le_O.
apply n_le_Sn.
Defined.
(* If we print le_O_n, the official proof of the above fact, we can see that it uses the
induction principle just like we did. *)
Require Import Arith.Le.
Print le_O_n.
(* For practice, we'll prove the structural induction principle for nat. *)
Definition nat_ind' : forall (P : nat -> Prop)
(HO : P O)
(HS : forall n : nat, P n -> P (S n)),
forall n, P n.
intros P HO HS.
(* Since we're defining an induction principle, we shouldn't use an induction principle. *)
(* Instead, we explicitly write the fixpoint. *)
exact (fix F (n : nat) : P n :=
match n with
| O => HO
| S n => HS n (F n)
end).
Defined.
(* nat_ind is defined in terms of nat_rect. If we compare nat_rect and our induction
principle we'll see that they are about the same. *)
Print nat_rect.
Print nat_ind'.
(* What's the type of the match statement? *)
(* Of course, structural induction is just one variant of well-founded induction. It is not
the only form and not necessarily the form that will allow us to actually prove our
desired goal. *)