Check bool.
Print bool.

Check bool_ind.

Definition neg (b : bool) : bool :=
match b with
  true => false
| false => true
end.

Print neg.

Lemma bool1 : forall b : bool, neg (neg b) = b.
intro b.
(* destruct b case b elim b *)
elim b.
simpl. 
reflexivity.
simpl. 
reflexivity.
(* or chain the last 5 lines into 
   elim b; simpl; reflexivity.
*)
Qed.

Print nat.
Print plus.

Lemma nat1 : forall n : nat, plus n 0 = n.
induction n.
simpl. 
reflexivity.
simpl. 
rewrite IHn.
reflexivity.
Qed.

Lemma nat2 : forall n : nat, plus 0 n = n.
simpl.
(* NOTE: this works because plus is defined by recursion 
   over the first argument:
     plus  0    n = n
     plus (S m) n = S(plus m n)
*)
auto.
Qed.

(* EXERCISE 1: 
   [a] Define plus' by recursion over the second argument 
   [b] Prove "forall n : nat, plus' n 0 = n" by a simple script 
       as in Lemma nat2
*)


(* Example of a WRONG Fixpoint definition!
   Try to feed this to Coq
Fixpoint f (n : nat) {struct n} : nat :=
   match n with
    0 => 0
   | S p => f (f p)
end.
*)


(* Illustrating that logical connectives are also defined as inductive types *)
Print True.
Print False.

Lemma False1 : forall A:Prop, False -> A.
intros A HF.
(* contradiction. *)
elim HF.
Qed.
 
Check False_ind.

Print and.
Print or.

Lemma triv1 :forall A B :Prop, A /\ B -> A\/B.
intros A B.
intro H.
destruct H.
(* OR: induction H. 
       case H.
       elim H.*)
left.
exact H.
Qed.

Lemma triv2 :forall A B C :Prop, (A->C) \/ (B->C) -> A/\B -> C.
intros A B C H1 H2.
destruct H1.
destruct H2.
apply H; auto.
apply H; auto.
destruct H2.
auto.
Qed.