Library chordal_graph_optimality

Require Import List.
Require Import ZArith.
Require Import chordal_graph_coloring.
Require Import chordal_graph_coloring.
Require Import quicksort.
Require Import graph_construction.
Require Import nat_quicksort.
Require Import max_color.
Require Import lth_in_proof.

Record chordal_graph : Set := Chordal_graph{
gph : graph;
self_peo : forall (x : nat),
                       In x (vertices gph)
                  -> is_clique gph (x :: get_nghbs gph x) (length (get_nghbs gph x) + 1)
}.

Lemma get_avcolor_le_lth_aux :
           forall (l : list nat) (acc : nat),
           get_available_color__aux l acc <= (length l) + acc.

Proof.
unfold get_available_color_aux;induction l;intros;simpl.

intuition.

destruct (gt_eq_gt_dec a acc).
destruct s.
intuition.
rewrite plus_n_Sm;apply IHl.
intuition.
Qed.

Lemma get_avcolor_le_lth :
           forall (l : list nat),
           get_available_color_aux l <= length l +1.

Proof.
unfold get_available_color_aux;intros;
apply get_avcolor_le_lth_aux.
Qed.

Lemma get_used_colors2_lth_le :
            forall (l : list nat) (l' : list (nat*nat)),
            length (get_used_colors2 l l') = length l.

Proof.
induction l;intros.
reflexivity.

simpl.
apply eq_S;apply IHl.
Qed.

Lemma graph_coloring_le_lth :
            forall (g : graph) (x : nat),
            get_available_color g x (graph_coloring g)
            <= length (get_nghbs g x) +1.

Proof.
unfold get_available_color;intros.
assert (get_available_color_aux (nat_elim_dup(nat_quicksort(get_used_colors2 (get_nghbs g x) (graph_coloring g)))) <= length (nat_elim_dup(nat_quicksort (get_used_colors2 (get_nghbs g x) (graph_coloring g)))) +1).
apply get_avcolor_le_lth.
assert (length (nat_elim_dup(nat_quicksort(get_used_colors2 (get_nghbs g x) (graph_coloring g)))) <= length (nat_quicksort(get_used_colors2 (get_nghbs g x) (graph_coloring g)))).
apply lth_nat_elim_dup.
assert (length (nat_quicksort (get_used_colors2 (get_nghbs g x) (graph_coloring g))) = length (get_used_colors2 (get_nghbs g x) (graph_coloring g))).
apply lth_quicksort.
assert (length (get_used_colors2 (get_nghbs g x) (graph_coloring g)) = length (get_nghbs g x)).
apply get_used_colors2_lth_le.
intuition.
Qed.

Lemma clique_le_graph_coloring :
           forall (g : chordal_graph) (x : nat),
                In x (vertices (gph g))
           -> exists l' : list nat, exists n : nat, is_clique (gph g) l' n
                /\ get_available_color (gph g) x (graph_coloring (gph g)) <= n.

Proof.
intros;exists (x :: get_nghbs (gph g) x).
exists (length (get_nghbs (gph g) x) +1).
split.
apply self_peo;assumption.
apply graph_coloring_le_lth.
Qed.

Lemma diff_color_clique :
           forall (g : graph) (l : list nat) (k : nat) (col : list (nat*nat)),
           is_coloring g col
           -> is_clique g l k
           -> (forall (a b x y : nat),
                     In a l
                -> In x l
                -> In (a,b) col
                -> In (x,y) col
                -> a <> x
                -> b <> y).

Proof.
induction l;intros.
inversion H1.
inversion H0.
assert (In (a0,x) (edges g) \/ In (x,a0) (edges g)).
apply H8;intuition.
inversion H;decompose [or] H13.
apply sym_not_eq;apply (H15 a0 x b y);assumption.
apply (H15 x a0 y b);assumption.
Qed.

Lemma clique_le_max_color :
           forall (g : graph) (l : list nat) (k : nat) (col : list (nat*nat)),
                is_coloring g col
           -> l <> nil
           -> is_clique g l k
           -> k <= max_color col.

Proof.
intros.
inversion H1;inversion H.
subst;apply lth_in;try assumption.
intros;apply (proj1 (H9 x));inversion H1.
apply H13;assumption.
apply (diff_color_clique g l (length l) col);assumption.
Qed.

Lemma graph_coloring_optimality :
           forall (g : chordal_graph) (col : list (nat*nat)),
                is_coloring (gph g) col
           -> max_color (graph_coloring (gph g)) <= max_color col.

Proof.
intros.
assert ({vertices (gph g) = nil}+{vertices (gph g) <> nil}).
induction (vertices (gph g)).
intuition.
right;intro;inversion H0.
destruct H0.
unfold graph_coloring.
rewrite e;simpl.
unfold max_color;simpl;intuition.
assert (exists x : nat, In (x,max_color (graph_coloring (gph g))) (graph_coloring (gph g))).
apply in_max_color.
intros.
assert (1 <= y).
assert (y = get_available_color (gph g) x (graph_coloring (gph g))).
apply in_avcolor_get;assumption.
rewrite H1.
apply (correct_graph_coloring3).
intuition.
unfold graph_coloring.
induction (vertices (gph g)).
intuition.
simpl;assert (In (a,get_available_color (gph g) a nil) (graph_coloring_aux (gph g) l ((a,get_available_color (gph g) a nil) :: nil))).
apply in_acc_graph_coloring.
intuition.
unfold not;intro;rewrite H1 in H0.
inversion H0.
inversion H0.
assert (exists l' : list nat, exists n : nat, is_clique (gph g) l' n /\ get_available_color (gph g) x (graph_coloring (gph g)) <= n).
apply clique_le_graph_coloring.
eapply correct_graph_coloring2_aux1;eassumption.
assert (forall (l : list nat) (k : nat), l <> nil -> is_clique (gph g) l k -> k <= max_color col).
intros;apply (clique_le_max_color (gph g) l k col);assumption.
inversion H2;inversion H4.
decompose [and] H5.
assert (x1 <= max_color col).
assert ({x0 = nil}+{x0 <> nil}).
induction x0.
intuition.
right;intro;inversion H8.
destruct H8.
inversion H6.
subst;intuition.
apply (H3 x0 x1);assumption.
assert (max_color (graph_coloring (gph g)) = (get_available_color (gph g) x (graph_coloring (gph g)))).
apply in_avcolor_get;assumption.
rewrite <-H9 in H7.
intuition.
Qed.