Require Import Arith.
Require Import listT.

(*-----------------------------------------------------------------------------
this file provides some lemmas about the maximun
-----------------------------------------------------------------------------*)



Lemma inf_dec :forall  (a b : nat),  {(lt a b)} + {~ (lt a b)}.
intros.
assert ({le b a}+{(lt a b)}).
apply le_lt_dec.
case H.
intro;right;intuition.
intro;left;auto.
Qed.


Definition max_2_elt (a b : nat) : nat :=
   match (inf_dec a b) with (left _) => b | (right _) => a end.
 
Fixpoint max_elt ( a : nat)( l : (listT nat)){struct l} : nat :=
 match l with   nilT => a
             | (consT m ms) => (max_elt (max_2_elt a m) ms) end.

Lemma max_0_r:forall (a : nat) , (max_2_elt (0) a) = a.
intros.
case a.
unfold max_2_elt.
case (inf_dec (0) (0)).
intuition.
intuition.
intros.
unfold max_2_elt.
case (inf_dec (0) (S n)).
intuition.
intuition.
Qed.


Lemma max_0:forall (a : nat) , (max_2_elt a (0)) = a.
intros.
case a.
unfold max_2_elt.
case (inf_dec (0) (0)).
intuition.
intuition.
intros.
unfold max_2_elt.
case (inf_dec (S n) (0)).
intuition.
intuition.
Qed.


Lemma max2_le:forall (a b c : nat), (le b c) ->  (max_2_elt a b) <=(max_2_elt a c) .
intros.
unfold max_2_elt.
case (inf_dec a b).
case (inf_dec a c).
intros;auto.
intros.
assert (lt a c).
apply lt_le_trans with b;auto.
intuition.
case (inf_dec a c).
simpl;intros.
auto with *.
simpl;intros.
auto with *.
Qed.

Lemma max2_sym:forall (a b  : nat),   (max_2_elt a b) =(max_2_elt b a) .
intros.
unfold max_2_elt.
case (inf_dec a b).
case (inf_dec b a).
intros;intuition.
auto with *.
case (inf_dec b a).
auto with *.
intros;intuition.
Qed.

Lemma max_2_le:forall (a b c : nat),a<=b->a<=max_2_elt c b.
intros.
unfold max_2_elt.
case (inf_dec c b).
auto with *.
simpl;intros.
assert (b<=c);auto with *.
Qed.

Lemma max_2_le_le:forall (a b c d: nat),a<=b->c<=d->
                                                              max_2_elt a c<=max_2_elt b d.
intros.
unfold max_2_elt.
case (inf_dec a c).
case (inf_dec b d).
simpl;intros;auto.
simpl;intros.
assert (d<=b);auto with *.
case (inf_dec b d).
simpl;intros.
assert (lt a d);auto with *.
simpl;intros;auto.
Qed.

Lemma le_max2_S:forall (a b : nat),S (max_2_elt a b)<=max_2_elt (S a) (S b).
intros.
unfold max_2_elt.
case (inf_dec a b).
case (inf_dec (S a) (S b)).
simpl;intros;auto.
simpl;intros;auto with *.
case (inf_dec (S a) (S b)).
simpl;intros;auto with *.
simpl;intros;auto with *.
Qed.


Lemma inf_max:forall (a n : nat), (lt a n) ->  (max_2_elt a n) = n.
intros.
unfold max_2_elt.
case (inf_dec a n).
auto.
intuition.
Qed.
 
Lemma max_inf:forall (a b n : nat), (lt (max_2_elt n a) b) ->  (lt n b) /\ (lt a b).
intros a b n.
unfold max_2_elt.
case (inf_dec n a).
intros.
split.
apply lt_trans with (m := a).
try exact l.
try exact H.
try exact H.
intros.
split.
auto.
assert (le a n).
apply not_gt.
try exact n0.
apply le_lt_trans with (m := n).
try exact H0.
try exact H.
Qed.
 
Lemma inf_max_max:forall
 (l : (listT nat)) (n a : nat), (le n a) ->  (le (max_elt n l) (max_elt a l)).
induction l.
simpl.
auto with *.
simpl.
intros.
case (inf_dec n a).
intros.
rewrite inf_max.
case (inf_dec a0 a).
intros.
rewrite inf_max.
auto with *.
auto with *.
intros.
assert (le a a0).
apply not_gt.
try exact n0.
cut ((max_2_elt a0 a) = a0).
intros.
rewrite H1.
apply (IHl a a0).
auto with *.
unfold max_2_elt.
case (inf_dec a0 a).
intuition.
auto with *.
auto with *.
intros.
assert (le a n).
apply not_gt.
try exact n0.
cut ((max_2_elt n a) = n).
intros.
rewrite H1.
assert (le a a0).
auto with *.
cut ((max_2_elt a0 a) = a0).
intros.
rewrite H3.
apply (IHl n a0).
auto with *.
unfold max_2_elt.
case (inf_dec a0 a).
intuition.
auto with *.
unfold max_2_elt.
case (inf_dec n a).
intuition.
auto with *.
Qed.
 
Lemma inf_max_el:forall (n : nat) (l : (listT nat)),  (le n (max_elt n l)).
intros.
induction l.
simpl.
auto.
simpl.
case (inf_dec n a).
intros.
rewrite inf_max.
intros.
apply le_trans with (m := (max_elt n l)).
try exact IHl.
apply inf_max_max.
auto with *.
auto with *.
intros.
assert (le a n).
apply not_gt.
auto with *.
cut ((max_2_elt n a) = n).
intros.
rewrite H0.
try exact IHl.
unfold max_2_elt.
case (inf_dec n a).
intuition.
auto with *.
Qed.
 
Lemma inf_inf_max_el:forall
 (n a : nat) (l : (listT nat)), (lt n a) ->  (lt n (max_elt a l)).
induction l.
simpl.
auto.
intros.
simpl.
apply lt_le_trans with (m := (max_2_elt a a0)).
apply lt_le_trans with (m := a).
exact H.
unfold max_2_elt.
case (inf_dec a a0).
intro.
apply lt_le_weak.
auto with *.
auto with *.
apply inf_max_el.
Qed.
 
Lemma le_max:forall (a b : nat) ,(le a b) ->  (max_2_elt b a) = b.
intros.
unfold max_2_elt.
case (inf_dec b a).
intuition.
auto.
Qed.
 
Lemma max_2_ass:forall (a  b c : nat),(max_2_elt (max_2_elt a b) c) = (max_2_elt a (max_2_elt b c)).
intros.
unfold max_2_elt.
case (inf_dec a b).
case (inf_dec b c).
case (inf_dec a c).
auto.
intuition.
case (inf_dec a b).
auto.
intuition.
case (inf_dec a c).
case (inf_dec b c).
case (inf_dec a c).
auto.
intuition.
case (inf_dec a b).
intuition.
intuition.
case (inf_dec b c).
case (inf_dec a c).
intuition.
auto.
case (inf_dec a b).
intuition.
auto.
Qed.
 
Lemma max_el_max_2el:forall (l :(listT nat)) (a n : nat),  (max_elt (max_2_elt n a) l) = (max_2_elt n (max_elt a l)).
induction l.
simpl.
auto.
intros.
simpl.
case (inf_dec (max_2_elt n a0) a).
intros.
rewrite inf_max with (a := (max_2_elt n a0)).
intros.
assert ((lt n a) /\ (lt a0 a)).
apply max_inf.
try exact l0.
rewrite inf_max with (a := a0).
assert (lt n (max_elt a l)).
apply inf_inf_max_el.
intuition.
rewrite inf_max.
auto with *.
auto with *.
intuition.
auto with *.
intros.
rewrite <- (IHl (max_2_elt a0 a) n).
rewrite max_2_ass.
auto.
Qed.
 
Lemma max_el_0:forall (l : (listT nat)) (n : nat),  (max_elt n l) = (max_2_elt n (max_elt (0) l)).
induction l.
simpl.
intros.
rewrite max_0.
auto.
intros.
simpl.
rewrite max_0_r.
apply max_el_max_2el.
Qed.





Lemma max_eq:forall (a:nat)(l:listT nat),a<=max_elt (max_2_elt 0 a) l.
intros.
rewrite max_0_r.
apply inf_max_el.
Qed.

Lemma le_max2el: forall  (a b:nat), a <= max_2_elt b a.
unfold max_2_elt;intros.
case (inf_dec b a).
auto with *.
auto with *.
Qed.




Lemma InT_max:forall  (l:listT nat)(a b:nat),InT a l->a<=max_elt b l.
induction l.
simpl;intros.
intuition.
simpl;intros.
elim H;intros heq.
rewrite heq.
apply le_trans with (m:=max_2_elt b a0).
apply le_max2el.
apply inf_max_el.
apply IHl.
auto.
Qed.

Lemma max_elt_app:forall (u v:listT nat)(n:nat),
max_elt n (appT u v)=max_elt (max_elt n u) v.
induction u.
simpl;intros;auto with * .
simpl;intros.
rewrite IHu.
auto with * .
Qed.