(* 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.