Require Import Arith. 

SearchAbout lt.

Section CaseDistinctions.

(* Definitions using case distinctions *)

Check eq_nat_dec.

Definition CaseDist1: nat -> nat := 
fun n =>
( if (eq_nat_dec n 2) then 0 else 1).

(* Another way of doing the same: *)

Definition CaseDist2: nat -> nat := 
fun n =>
match (eq_nat_dec n 2) with
| left _ => 0
| right _ => 1
end.

Lemma Test: (CaseDist2 1) = 1.
unfold CaseDist2.
simpl.
reflexivity.
Save.

(* More complicated case distinction: *)

Check lt_eq_lt_dec.

(* this is a nested construction:

inleft _ : ( {n<m} + {n=m} )
inleft (left _ ): {n<m}
inleft (right _): {n=m}
inright _: {m<n}

This should clarify what the following definition does: *)

Definition CaseDist3: nat -> nat :=
fun n =>
match (lt_eq_lt_dec n 3) with
| inleft (left _) => 1
| inleft (right _) => 3
| inright _ => 5
end.

(* An example of a trivial proofi where we distinguish the cases: *)

Lemma trivial: forall (n:nat), 6 > CaseDist3 n.
Proof.
intro. 

(* to make our definition explicit: *)
unfold CaseDist3.
(* warning: be wise when to use "unfold" -needed here- and when "simpl". *)

destruct (lt_eq_lt_dec n 3).
destruct s.

(* we take the easy way and let "intuition" solve the three cases: *)
intuition.
intuition.
intuition.
Qed.

(* If we Print the definition above, we see an alternative way 
of doing the same, using "if-then": *)

Print CaseDist3.

Definition CaseDist3a: nat -> nat :=
fun n =>
match (lt_eq_lt_dec n 3)  with
|inleft s => (if  s then 1 else 3)
|inright _ => 5
end. 

End CaseDistinctions.