Library graph_construction


Require Import List.

Require Import ZArith.

Require Import quicksort.

Require Import lex_sort.

Require Import strict_ord.

Require Import nat_quicksort.

Require Import strict_inc_and_dec.




Parameter edges_list : list (nat*nat).




Definition lto_edges (l : list (nat*nat)) : list (nat*nat) :=

               nat_nat_elim_dup (lex_sort (order l)).




Lemma is_sorted_lto_edges :

            forall (l : list (nat*nat)), is_lex_sorted (lto_edges l).




Proof.

intros;unfold lto_edges;apply lex_sort_nat_nat_elim_dup;

apply is_lex_sorted_lex_sort.

Qed.




Lemma is_strict_ord_lto_edges :

            forall (l : list (nat*nat)), is_strict_ord (lto_edges l).




Proof.

intros;unfold lto_edges;apply strict_ord_nat_nat_elim_dup;

apply strict_ord_lex;apply strict_ord_order.

Qed.




Lemma NoDup_lto_edges :

            forall (l : list (nat*nat)), NoDup (lto_edges l).




Proof.

unfold lto_edges;intros;apply NoDup_nat_nat_elim_dup.

apply is_lex_sorted_lex_sort.

Qed.




Lemma correct_lto_edges1 :

            forall (l : list (nat*nat)) (x y : nat),

                 In (x,y) (lto_edges l) 

            -> In (x,y) l \/ In (y,x) l.




Proof.

unfold lto_edges;intros.

assert (In (x,y) (nat_nat_elim_dup (lex_sort(order l))) -> In (x,y) (lex_sort(order l))).

apply in_nat_nat_elim_dup.

assert (In (x,y) (lex_sort (order l)) -> In (x,y) (order l)).

assert (Permutation (order l) (lex_sort (order l))).

apply is_perm_lex_sort.

apply Permutation_in;apply Permutation_sym;assumption.

eapply only_in_order.

apply (H1 (H0 H)).

Qed.




Lemma correct_lto_edges_aux2 :

           forall (l : list (nat*nat)) (x y : nat),

                In (x,y) l

           -> x <> y

           -> In (x,y) (lto_edges l) \/ In (y,x) (lto_edges l).




Proof.

unfold lto_edges;intros.

assert (In (x,y) (nat_nat_elim_dup (lex_sort (order l))) \/ In (y,x) (nat_nat_elim_dup (lex_sort (order l)))).

assert (In (x,y) (lex_sort (order l)) \/ In (y,x) (lex_sort (order l))).

assert (In (x,y) (order l) \/ In (y,x) (order l)).

apply all_in_order;assumption.

assert (forall (x y : nat), In (x,y) (order l) -> In (x,y) (lex_sort (order l)));intros.

assert (Permutation (order l) (lex_sort (order l))).

apply is_perm_lex_sort.

eapply Permutation_in;eassumption.

decompose [or] H1;[left | right];apply H2;assumption.

decompose [or] H1;[left | right];apply in_nat_nat_dup;assumption.

decompose [or] H1;[left | right];apply H2;assumption.

Qed.




Fixpoint edges_to_vertices_aux (edges : list (nat*nat)) {struct edges} : list nat :=

match edges with

| nil => nil

| (x,y) :: edges' => x :: y :: (edges_to_vertices_aux edges')

end.




Definition edges_to_vertices (edges : list (nat*nat)) : list nat :=

                nat_elim_dup(nat_quicksort (edges_to_vertices_aux edges)).




Lemma is_strict_inc_vertices :

            forall (l : list (nat*nat)),

            is_strict_inc (edges_to_vertices l).




Proof.

intros;unfold edges_to_vertices;

unfold nat_quicksort;apply sort_NoDup_strict_inc;

[apply is_sorted_elim_dup | apply NoDup_nat_elim_dup];

apply is_sorted_quicksort;

[| intros;destruct (le_gt_dec a b) | | intros;destruct (le_gt_dec a b) ];

intuition.

Qed.




Lemma in_vertices_aux :

            forall (l : list (nat*nat)) (x y : nat),

                 In (x,y) l

            -> In x (edges_to_vertices_aux l) /\ In y (edges_to_vertices_aux l).




Proof.

induction l;[|destruct a];simpl;intros.




intuition.




split;decompose [or] H;

[inversion H0;intuition | right;right;apply (proj1 ((IHl x y) H0)) |
 inversion H0;intuition | right;right;apply (proj2 ((IHl x y) H0)) ].

Qed.




Lemma in_vertices :

            forall (l : list (nat*nat)) (x y : nat),

                 In (x,y) l

            -> In x (edges_to_vertices l) /\ In y (edges_to_vertices l).




Proof.

split;unfold edges_to_vertices;intros;apply in_nat_dup;

apply Permutation_in with (l := edges_to_vertices_aux l);

[unfold nat_quicksort;apply permutation_quicksort |
apply (proj1 ((in_vertices_aux l x y) H)) |
unfold nat_quicksort;apply permutation_quicksort |
apply (proj2 ((in_vertices_aux l x y) H)) ].

Qed.




Lemma in_edges_only_aux :

            forall (l : list (nat*nat)) (x : nat),

                 In x (edges_to_vertices_aux l)

            -> In x (edges_to_vertices l).




Proof.

intros;unfold edges_to_vertices.

apply in_nat_dup.

assert (Permutation (edges_to_vertices_aux l) (nat_quicksort (edges_to_vertices_aux l))).

unfold nat_quicksort;apply permutation_quicksort.

eapply Permutation_in;eassumption.

Qed.




Lemma in_edges_only :

            forall (l : list (nat*nat)) (x : nat),

                 In x (edges_to_vertices l) 

            -> exists y, In (x,y) l \/ In (y,x) l.




Proof.

induction l;[|destruct a];unfold edges_to_vertices;intros.

inversion H.

simpl in H;apply in_nat_elim_dup in H.

assert (In x (n :: n0 :: edges_to_vertices_aux l)).

eapply Permutation_in.

apply Permutation_sym;unfold nat_quicksort;apply permutation_quicksort.

unfold nat_quicksort in H;eassumption.

simpl in H0;decompose [or] H0.

subst;exists n0;intuition.

subst;exists n;intuition.

assert (exists y : nat, In (x,y) l \/ In (y,x) l).

apply IHl;apply in_edges_only_aux;assumption.

inversion H1.

decompose [or]H3;exists x0;intuition.

Qed.




Record graph : Set := Graph{

vertices : list nat;

edges : list (nat*nat);

is_lex_sorted_edges : is_lex_sorted edges;

is_strict_ord_edges : is_strict_ord edges;

NoDup_edges : NoDup edges;

vertices_edges : vertices = edges_to_vertices edges

}.




Definition my_graph : graph :=

Graph  (edges_to_vertices (lto_edges edges_list)) 

           (lto_edges edges_list)

           (is_sorted_lto_edges edges_list)

           (is_strict_ord_lto_edges edges_list)

           (NoDup_lto_edges edges_list)

           (refl_equal (edges_to_vertices (lto_edges edges_list))).




Inductive is_clique : graph -> list nat -> nat -> Prop :=

is_clique_cons : forall (g : graph) (l : list nat) (k : nat),

                             NoDup l

                        -> length l = k

                        -> (forall (x y :nat),

                                   In x l

                              -> In y l

                              -> x <> y 

                              -> In (x,y) (edges g) \/ In (y,x) (edges g))

                        -> (forall (x : nat),

                              In x l

                              -> In x (vertices g))

                        -> is_clique g l k.




Inductive sv : nat -> list nat -> list (nat*nat) -> Prop :=

sv_cons : forall (rl : list nat) (edg : list (nat*nat)) (x : nat),

                         In x rl

                    -> (forall (y z : nat),

                              x <> y

                         -> x <> z

                         -> y <> z

                         -> In y rl

                         -> In z rl

                         -> In (x,y) edg \/ In (y,x) edg

                         -> In (x,z) edg \/ In (z,x) edg

                         -> In (y,z) edg \/ In (z,y) edg)

                    -> sv x rl edg.




Inductive _peo : list nat -> list nat -> list (nat*nat) -> Prop :=

peo_cons : forall (l vert : list nat) (edg : list (nat*nat)),

                  Permutation vert l

                  -> (forall (x : nat) (ll rl : list nat),

                            l = ll ++ x :: rl

                       -> sv x (x :: rl) edg)

                  -> _peo l vert edg.




Definition peo (l : list nat) (g : graph) : Prop :=

               _peo l (vertices g) (edges g).




Axiom ax1 : exists unknown_peo : list nat,

                  peo unknown_peo my_graph.