Library max_color
Require Import List.
Require Import ZArith.
Fixpoint max_color_aux (l : list (nat*nat)) (acc : nat) {struct l} : nat :=
match l with
| nil => acc
| (x,y) :: l' => match (le_gt_dec y acc) with
| left _ => max_color_aux l' acc
| right _ => max_color_aux l' y
end
end.
Definition max_color (l : list (nat*nat)) :=
max_color_aux l 0.
Lemma ge_max_color_acc :
forall (l : list (nat*nat)) (acc : nat),
acc <= max_color_aux l acc.
Proof.
induction l;intros;[|destruct a];simpl.
intuition.
destruct (le_gt_dec n0 acc).
apply IHl.
assert (n0 <= max_color_aux l n0);[apply IHl|intuition].
Qed.
Lemma max_color_nil_0 :
forall (l : list (nat*nat)),
(forall (x y : nat), In (x,y) l -> 1 <= y)
-> max_color l = 0
-> l = nil.
Proof.
unfold max_color;induction l;intros;[|destruct a;simpl].
reflexivity.
simpl in H0;destruct (le_gt_dec n0 0).
assert (1 <= n0).
apply (H n n0);intuition.
apply False_ind;intuition.
assert (n0 <= max_color_aux l n0).
apply ge_max_color_acc.
apply False_ind;intuition.
Qed.
Lemma in_max_color_aux :
forall (l : list (nat*nat)) (acc : nat),
(exists x : nat, In (x,max_color_aux l acc) l)
\/ max_color_aux l acc = acc.
Proof.
unfold max_color;induction l;intros;[|destruct a];simpl.
intuition.
destruct (le_gt_dec n0 acc).
assert ((exists x : nat, In (x,max_color_aux l acc) l) \/ max_color_aux l acc = acc).
apply IHl.
decompose [or] H;[left;inversion H0;exists x | ];intuition.
assert ((exists x : nat, In (x,max_color_aux l n0) l) \/ max_color_aux l n0 = n0).
apply IHl.
decompose [or] H;left;[inversion H0;exists x | exists n];intuition.
Qed.
Lemma in_max_color :
forall (l : list (nat*nat)),
(forall (x y : nat), In (x,y) l -> 1 <= y)
-> l <> nil
-> exists x : nat, In (x,max_color l) l.
Proof.
unfold max_color;intros.
assert ((exists x : nat, In (x,max_color_aux l 0) l) \/ max_color_aux l 0 = 0).
apply in_max_color_aux.
decompose [or] H1.
assumption.
assert (l = nil).
apply max_color_nil_0;assumption.
apply False_ind;intuition.
Qed.
Lemma max_max_color_aux :
forall (l : list (nat*nat)) (x y acc : nat),
In (x,y) l
-> y <= max_color_aux l acc.
Proof.
induction l;intros;[|destruct a];simpl.
inversion H.
destruct (le_gt_dec n0 acc).
simpl in H;decompose [or] H.
assert (acc <= max_color_aux l acc).
apply ge_max_color_acc.
inversion H0;intuition.
eapply IHl;eassumption.
simpl in H;decompose [or] H.
inversion H0;rewrite <-H3.
apply ge_max_color_acc.
eapply IHl;eassumption.
Qed.
Lemma max_max_color :
forall (l : list (nat*nat)) (x y :nat),
In (x,y) l
-> y <= max_color l.
Proof.
unfold max_color;intros.
eapply max_max_color_aux;eassumption.
Qed.