gistfile1.coq

(* Reading:
http://www.cis.upenn.edu/~bcpierce/sf/ProofObjects.html
http://www.cis.upenn.edu/~bcpierce/sf/MoreInd.html
*)

Require Import Arith.

Print nat.
(*
Inductive nat : Set :=  O : nat | S : nat -> nat.
*)

Print nat_ind.
Print nat_rect.
Check nat_ind.

Lemma nat_ind'
     : forall P : nat -> Prop,
       P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n.
Proof.
  intros P P0 PSn. fix 1. (* tauto. apply nat_ind'. *)
  destruct n as [|n']. apply P0. apply PSn. apply nat_ind'.
Qed.

Definition nat_ind''
  (* intros P P0 PSn n *)
  (P : nat -> Prop) (P0 : P O) (PSn : forall n : nat, P n -> P (S n)) :=
  (* fix 1. *)
  fix nat_ind''' (n : nat) : P n :=
  (* destruct n as [|n']. *)
  match n with
  | O => P0 (* apply P0. *)
  | S n' => PSn n' (nat_ind''' n') (* apply PSn. apply nat_ind'. *)
  end.

Lemma blah : forall n, n + 0 = n.
Proof.
  intros n. induction n. reflexivity. simpl; rewrite IHn; reflexivity.
Qed.

Print blah. (* uses nat_ind *)

Unset Elimination Schemes.

Inductive nat' : Set :=  O' : nat' | S' : nat' -> nat'.

Lemma blah' : forall n : nat', n = O'.
Proof.
  intros n. (* induction n. 
Toplevel input, characters 0-11:
Error: Cannot find the elimination combinator nat'_ind, the elimination of
the inductive definition nat' on sort Prop is probably not allowed. *)
Abort.

Set Elimination Schemes.

Lemma blah' : forall n, n + 0 = n.
Proof.
  intros n. induction n using nat_ind''.
  reflexivity. simpl; rewrite IHn; reflexivity.
Qed.
Print blah'.

Lemma blah'' : forall n, n + 0 = n.
Proof. apply nat_ind''; eauto. Qed.

Lemma blah_elim : forall n, n + 0 = n.
Proof. intro n. elim n; eauto. Qed.
Print blah_elim. (* also uses nat_ind *)

Goal forall P Q : Prop, P /\ Q -> P.
Proof. intros P Q H. destruct H as [HP HQ]. Show Proof. assumption.
Qed.

Goal forall P Q : Prop, P /\ Q -> P.
Proof. intros P Q H. induction H as [HP HQ]. Show Proof. assumption.
Qed.

(* same as induction here *)
Goal forall P Q : Prop, P /\ Q -> P.
Proof. intros P Q H. elim H. intros HP HQ.  Show Proof. assumption.
Qed.
Check and_ind.

Goal forall P : Prop, P \/ P -> P.
Proof. intros P H. induction H; assumption. Show Proof. Qed.
Check or_ind.

Goal forall P : Prop, P \/ P -> P.
Proof. intros P H. elim H; trivial. Show Proof. Qed.