(** * Inductive Types *)

(** Booleans *)
Check bool.
Print bool.

Check bool_ind.

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

Print neg.

(** There is some useful syntactic sugar for the type bool *)
Definition negg (b : bool) := if b then false else true.

Print negg.

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

(** Distinct constructors of an inductive type are different:
   [true] and [false] are different #<br>#
   There is a simple tactic [congruence] that proves -- among other things -- that 
   distinct constructors of an inductive type are different: *)
Lemma dist : ~ true = false.
Proof.
congruence.
Qed.

(** Natural Numbers *)
Print nat.
Print plus.

(** To define plus, we would type the following *)
Fixpoint plus' (n m : nat) {struct n} : nat :=
  match n with
  | O => m
  | S p => S (plus' p m)
  end.

Print plus'.

Lemma nat1 : forall n : nat, plus n 0 = n.
Proof.
intro n.
induction n.
(** Also try [destruct n] and notice it doesn't work: 
   [destruct] only does a case analysis, but doesn't give you an induction hypothesis *)
- simpl. 
  reflexivity.
- simpl. 
  rewrite IHn.
  reflexivity.
Qed.

Print plus.

Lemma nat2 : forall n : nat, plus 0 n = n.
Proof.
simpl.
(** Note: this works because [plus] is defined by recursion 
   over the first argument:#<br>#
     [plus  0    n = n] #<br>#
     [plus (S m) n = S(plus m n)]
*)
auto.
Qed.

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


(** Logical connectives are also defined as inductive types *)
Print True.
Print False.
(** [False] is the inductive type with no constructors *)
Check False_ind.

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

Print and.
(** [conj : A -> B -> A /\ B] is conjunction introduction *)
Check and_ind.
(** [and_ind
     : forall A B P : Prop,
       (A -> B -> P) -> A /\ B -> P] #<br>#
is a generalised form of conjunction elimination. #<br>#
We use [split] for introduction, [destruct] for elimination. *) 
Print or.
Check or_ind.

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

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

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

(** Example of a _wrong_ Inductive definition!
   Try to feed this to Coq 
<<
Inductive Lambda : Set :=
  | var : nat -> Lambda
  | app : Lambda -> Lambda -> Lambda
  | abs : (Lambda -> Lambda) -> Lambda.
>>
*)