Require Export Omega.
Require Export Plus.

Coercion bool2Prop (x : bool) := if x then True else False.
Ltac fomega := try (exfalso;omega)||contradiction.

(********************************************************************************
 
 andb_prod:
  A lemma like andb_true_eq from the Coq.Bool.Bool library but more comfortable
  to use.
 
 rewrite_andb_and:
  A lemma allowing to rewrite a bool-conjunction to a Prop-conjuction.

********************************************************************************)
Lemma andb_and {a b: bool}(e : (a && b)%bool): a /\ b.
Proof.
destruct a,b;
repeat split;
assumption.
Defined.

Lemma rewrite_andb_and {a b: bool}: a /\ b -> (a && b)%bool.
Proof.
intros [e1 e2].
destruct a,b ;
auto.
Defined.

Lemma orb_or {a b: bool}(e : (a || b)%bool): a \/ b.
Proof.
destruct a,b; tauto.
Defined.

Lemma rewrite_orb_or {a b: bool}: a \/ b -> (a || b)%bool.
Proof.
intros [e1 | e2];
destruct a,b ;
cbv in *; auto.
Defined.

Definition nat_eq_cert (n m:nat): {n=m}+{n<>m}.
decide equality.
Defined.

Lemma nat_eq_cert_refl : forall n, nat_eq_cert n n = left (n<>n) (eq_refl n).
Proof.
  induction n; simpl.
    reflexivity.
    rewrite IHn. reflexivity.
Defined.

Definition nat_eq (n m: nat): bool :=
  if nat_eq_cert n m then true else false.

Lemma informative_trichotomy (n m: nat) : {n > m} +  {m > n} + {n = m}.
revert m;
induction n;
destruct m.
auto.
left. right. omega.
left. left. omega.
destruct (IHn m) as [ [A | A]| A ].
left. left. omega.
left. right. omega.
auto.
Defined.

Definition bool_eq_cert (b b' :bool) : {b=b'}+{b<>b'}.
decide equality.
Defined.

Definition gtb (n m: nat) : {n>m} + {n<=m}.
revert m.
induction n; destruct m;
try (left; omega);
try (right; omega).
destruct (IHn m);
try (left; omega);
try (right; omega).
Defined.


Definition ltb (n m: nat) : {n<m} + {n>=m}.
revert m.
induction n; destruct m;
try (left; omega);
try (right; omega).
destruct (IHn m);
try (left; omega);
try (right; omega).
Defined.

Definition max2 (a b :nat) := 
if gtb a b then a else b.

Definition max3 (a b c :nat) :=
max2 (max2 a b) c.

Lemma max3_correct (a b c: nat ): S (max3 a b c) > a /\ S (max3 a b c) > b /\ S (max3 a b c) > c.
unfold max3;
unfold max2.
destruct (gtb a b), (gtb a c), (gtb b c);
omega.
Qed.

Lemma size_induction {X : Type} (f : X -> nat) (p: X ->Prop) :
( forall x, ( forall y,  (f y) < (f x) -> p y) -> p x) -> forall x, p x.
Proof.
intros A x.
apply A.
induction (f x).
 intros; destruct (f y); try inversion H.
 
 intros y B.
 apply A.
 intros z C.
 apply IHn.
 omega.
Defined.

Lemma double_size_induction {X : Type} (f : X -> nat) (p: X -> X->Prop) :
( forall x1 x2, ( forall y1 y2,( (f y1) + (f y2) < (f x1) + (f x2) -> p y1 y2)) -> p x1 x2)
-> forall x1 x2, p x1 x2.
Proof.
intros A y y'.
apply A .
induction (f y + f y').
intros. inversion H.

 intros y1 y2 B.
 apply A.
 intros z z' L.
 apply IHn.
 omega.
Defined.