(* 2008 - 03 - 03 *)

(* Here we try to prove forall n, 0 <= n again using nat_ind. 
We can do this if we apply nat_ind to (fun n => 0 <= n), 
since the application is not a higher order function. *)
Goal forall n, 0 <= n.
apply (nat_ind (fun n => 0 <= n)); auto.
Qed.

(* We could also pass (nat_ind (fun n => 0 <= n)) to the auto tactic.
The auto tactic will no longer reject it as ill formed, since the type 
of (nat_ind (fun n => 0 <= n)) is no longer abstracted over P as the
type of nat_ind is.*)
Check nat_ind.
Check (nat_ind (fun n => 0 <= n)).

Goal forall n, 0 <= n.
intros n.
auto using (nat_ind (fun n => 0 <= n)).
Qed.


(* We can use the pattern tactic so that Coq synthesizes P for us. 
Then we can apply nat_ind without explicitly supplying P. *)

Goal forall n, 0 <= n.
Proof.
intros n.
pattern n.
apply nat_ind; auto.
Qed.

(* We can use the elim tactic which does two things:
1) uses the pattern tactic to infer P
2) selects the appropriate induction principle based on the type of the term specified,
and applies it
*)

Goal forall n, 0 <= n.
Proof.
intros n.
elim n; auto.
Qed.

(* Finally, we can use the induction tactic which wraps the elim tactic in 
some pre-processing and post-processing steps. 
1) It introduces all variables up to the named variable.
2) It runs the elim tactic.
3) It does intros on every subgoal generated by the elim tactic. *)
Goal forall n, 0 <= n.
Proof.
induction n; auto.
Qed.


(* Sometimes, we are not interested in recursion, but only in matching each
constructor of our inductive type. In that case, the destruct tactic is
appropriate. Here we define a function that maps natural numbers to booleans in
the usual way.*)
Goal nat -> bool.
Proof.
intro n.
destruct n.
Show Proof.
exact (false).
exact (true).
Qed.