Library renaming
Require Import List.
Require Import ZArith.
Require Import strict_inc_and_dec.
Require Import peo_search.
Require Import graph_construction.
Require Import chordal_graph_coloring.
Require Import lex_sort.
Require Import strict_ord.
Require Import nat_quicksort.
Require Import chordal_graph_optimality.
Fixpoint rank (l : list nat) (acc x : nat) {struct l} : nat :=
match l with
| nil => S acc
| y :: l' => match (eq_nat_dec x y) with
| left _ => acc
| right _ => rank l' (S acc) x
end
end.
Lemma acc_le_rank_in :
forall (l : list nat) (acc x : nat),
In x l
-> acc <= rank l acc x.
Proof.
induction l;intros.
inversion H.
simpl.
destruct (eq_nat_dec x a).
intuition.
assert (S (acc) <= rank l (S acc) x).
apply IHl;simpl in H;decompose [or]H;subst;intuition.
intuition.
Qed.
Fixpoint rename_fun_aux (l : list nat) (acc : nat) {struct l} : list (nat*nat) :=
match l with
| nil => nil
| x :: l' => (x,rank l acc x) :: rename_fun_aux l' (S acc)
end.
Definition rename_fun (l : list nat) : list (nat * nat) :=
rename_fun_aux l 1.
Fixpoint rename_vert_aux (l l' : list nat) {struct l} : list nat :=
match l with
| nil => nil
| x :: l'' => rank l' 1 x :: rename_vert_aux l'' l'
end.
Definition rename_vert (l : list nat) : list nat :=
rename_vert_aux l l.
Fixpoint rename_edg (l : list (nat*nat)) (l' : list nat) {struct l } : list (nat*nat) :=
match l with
| nil => nil
| (x,y) :: l'' => (rank l' 1 x, rank l' 1 y) :: rename_edg l'' l'
end.
Fixpoint rename_vert_inv__aux (l : list (nat*nat)) (x : nat) {struct l} : nat :=
match l with
| nil => 0
| (y,z) :: l' => match x with
|0 => 0
|1 => y
|S n => rename_vert_inv__aux l' n
end
end.
Fixpoint rename_vert_inv_aux (l : list nat) (l' : list (nat*nat)) {struct l}: list nat :=
match l with
| nil => nil
| x :: l'' => rename_vert_inv__aux l' x :: rename_vert_inv_aux l'' l'
end.
Definition rename_vert_inv (l l': list nat) : list nat :=
rename_vert_inv_aux l (rename_fun l').
Definition my_l : list nat := 3 :: 4 :: 1 :: 5 :: 2 :: nil.
Definition my_v : list nat := 1 :: 2 :: 3 :: 4 :: 5 :: nil.
Lemma positive_in_rename :
forall (l l' : list nat) (x : nat),
(forall (y : nat),
In y l
-> In y l')
-> In x (rename_vert_aux l l')
-> 0 < x.
Proof.
induction l;simpl;intros.
intuition.
decompose [or]H0.
assert (1 <= rank l' 1 a).
apply acc_le_rank_in.
intuition.
intuition.
eapply IHl;intuition.
Qed.
Lemma rank_S :
forall (l : list nat) (acc x : nat),
rank l (S acc) x = S (rank l acc x).
Proof.
induction l;intros;simpl.
reflexivity.
destruct (eq_nat_dec x a).
reflexivity.
apply IHl.
Qed.
Lemma rename_fun_fst :
forall (l : list nat) (x y z : nat),
rename_vert_inv__aux (rename_fun_aux l x) z
= rename_vert_inv__aux (rename_fun_aux l y) z.
Proof.
induction l;intros;simpl.
reflexivity.
destruct z.
reflexivity.
destruct z.
reflexivity.
apply IHl.
Qed.
Lemma rename_not_in :
forall (l l' : list nat) (x : nat),
NoDup l
-> NoDup l'
-> ~In x l
-> (forall (y : nat),
In y l
-> In y l')
-> rename_vert_inv_aux (rename_vert_aux l (x :: l')) (rename_fun (x :: l'))
=
rename_vert_inv_aux (rename_vert_aux l l') (rename_fun l').
Proof.
induction l;intros.
intuition.
simpl;destruct (eq_nat_dec a x).
apply False_ind;subst;intuition.
assert (2 <= rank l' 2 a).
apply acc_le_rank_in.
apply H2;intuition.
assert (exists y : nat, rank l' 2 a = S y).
destruct (rank l' 2 a).
apply False_ind;intuition.
exists n0;reflexivity.
inversion H4;rewrite H5.
assert (exists y : nat, x0 = S y).
destruct x0.
apply False_ind;intuition.
exists x0;reflexivity.
inversion H6;rewrite H7.
rewrite rank_S in H5.
apply eq_add_S in H5.
rewrite H5.
rewrite <-H7.
rewrite IHl.
unfold rename_fun;rewrite (rename_fun_fst l' 2 1 x0).
reflexivity.
inversion H;assumption.
assumption.
intuition.
intuition.
Qed.
Lemma rename_inv__aux :
forall (l : list nat) (x : nat),
NoDup (x :: l)
->
rename_vert_inv_aux (rename_vert_aux l (x :: l)) (rename_fun (x :: l))
= rename_vert_inv (rename_vert l) l.
Proof.
induction l;intros.
simpl.
unfold rename_vert_inv;simpl.
reflexivity.
unfold rename_vert_inv.
unfold rename_vert.
simpl in *.
destruct (eq_nat_dec a x).
apply False_ind;subst;inversion H;intuition.
destruct (eq_nat_dec a a).
rewrite rename_not_in.
reflexivity.
inversion H;inversion H3;assumption.
inversion H;assumption.
inversion H;intuition.
intuition.
intuition.
Qed.
Lemma rename_inv_aux :
forall (l : list nat),
NoDup l
-> rename_vert_inv (rename_vert l) l = l.
Proof.
induction l;intros.
unfold rename_vert_inv;unfold rename_vert;reflexivity.
unfold rename_vert_inv;unfold rename_vert;simpl.
destruct (eq_nat_dec a a).
simpl.
rewrite rename_inv__aux.
rewrite IHl.
reflexivity.
inversion H;assumption.
inversion H;assumption.
intuition.
Qed.
Lemma rename_inv :
forall (l l' : list nat),
NoDup l
-> rename_vert l = l'
-> l = rename_vert_inv l' l.
Proof.
intros;rewrite <-H0;symmetry;apply rename_inv_aux;assumption.
Qed.
Definition new_edg : list (nat*nat) :=
rename_edg
(edges my_graph)
(rev (peo_search my_graph)).
Definition my_chordal_gph_edg : list (nat*nat) :=
lto_edges new_edg.
Definition my_chordal_gph_vert : list nat :=
edges_to_vertices my_chordal_gph_edg.
Definition my_chordal_gph : graph :=
Graph my_chordal_gph_vert my_chordal_gph_edg
(is_sorted_lto_edges new_edg)
(is_strict_ord_lto_edges new_edg)
(NoDup_lto_edges new_edg)
(refl_equal (edges_to_vertices (lto_edges new_edg))).
Lemma rev_app :
forall (l ll rl : list nat) (x : nat),
l = ll ++ x :: rl
-> rev l = rev rl ++ x :: rev ll.
Proof.
induction l;intros.
assert (In x nil).
rewrite H;intuition.
inversion H0.
simpl.
destruct ll.
inversion H.
subst.
simpl;reflexivity.
inversion H.
simpl.
assert (rev (ll ++ x :: rl) = rev rl ++ x :: rev ll).
rewrite <-H2;apply IHl;assumption.
rewrite H0.
rewrite app_ass;rewrite <-app_comm_cons;reflexivity.
Qed.
Lemma strict_inc_app_r :
forall (l ll rl : list nat) (x : nat),
is_strict_inc l
-> l = ll ++ x :: rl
-> is_strict_inc (x :: rl).
Proof.
induction l;intros.
assert (In x nil).
rewrite H0;intuition.
inversion H1.
destruct ll.
inversion H0.
subst.
assumption.
inversion H0.
eapply IHl.
eapply is_strict_inc_tail;eassumption.
eassumption.
Qed.
Lemma in_rev_sv :
forall (g : graph) (ll rl : list nat) (x y : nat),
In x (get_nghbs g y)
-> vertices g = ll ++ y :: rl
-> In x (rev ll).
Proof.
intros.
assert (Permutation ll (rev ll)).
apply Permutation_rev.
eapply Permutation_in.
eassumption.
assert (In (x,y) (edges g)).
apply edges_nghbs;assumption.
assert (x < y).
eapply strict_in.
apply is_strict_ord_edges.
eassumption.
assert (In x (vertices g)).
rewrite vertices_edges;
apply (proj1 ((in_vertices (edges g) x y) H2)).
assert (In x ll \/ In x (y :: rl)).
apply in_app_or.
rewrite <-H0;assumption.
decompose [or] H5.
assumption.
simpl in H6;decompose [or] H6.
apply False_ind;intuition.
assert (y < x).
apply (in_strict_sort rl y x).
apply (strict_inc_app_r (vertices g) ll rl y).
rewrite vertices_edges;apply is_strict_inc_vertices.
assumption.
assumption.
apply False_ind;intuition.
Qed.
Lemma rename_inv_app :
forall (ll l rl : list nat) (x : nat),
~In 0 ll
->
rename_vert_inv (ll ++ x :: rl) l
=
rename_vert_inv ll l ++ rename_vert_inv (x :: rl) l.
Proof.
induction ll;intros.
simpl.
reflexivity.
unfold rename_vert_inv in *.
simpl in *.
destruct (eq_nat_dec a 0).
rewrite e.
apply False_ind;intuition.
assert (exists y : nat, a = S y).
destruct a.
intuition.
exists a;reflexivity.
inversion H0.
rewrite H1.
simpl.
rewrite IHll.
reflexivity.
intuition.
Qed.
Lemma renaming_perm :
forall (l l' l'' : list nat),
Permutation l l'
-> Permutation (rename_vert_aux l l'') (rename_vert_aux l' l'').
Proof.
induction 1;simpl.
constructor.
constructor;assumption.
constructor;reflexivity.
apply Permutation_trans with ( l' := rename_vert_aux l' l'');assumption.
Qed.
Lemma in_rename_in_aux :
forall (l : list nat) (x : nat),
NoDup l
-> In x l
-> rename_vert_inv__aux (rename_fun l) (rank l 1 x) = x.
Proof.
induction l;intros.
inversion H0.
simpl.
destruct (eq_nat_dec x a).
intuition.
assert (2 <= rank l 2 x).
apply acc_le_rank_in.
simpl in H0;decompose [or]H0.
subst;intuition.
assumption.
assert (exists y : nat, rank l 2 x = S y).
destruct (rank l 2 x).
apply False_ind;intuition.
exists n0;reflexivity.
inversion H2;rewrite H3.
assert (exists y : nat, x0 = S y).
destruct x0.
apply False_ind;intuition.
exists x0;reflexivity.
inversion H4;rewrite H5.
assert (rank l (S 1) x = S (rank l 1 x)).
apply rank_S.
simpl in H0;decompose [or]H0.
subst;apply False_ind;intuition.
rewrite H6 in H3.
apply eq_add_S in H3.
rewrite <-H3 in H5.
rewrite <-H5.
unfold rename_fun in IHl.
rewrite (rename_fun_fst l 2 1 (rank l 1 x)).
apply IHl.
inversion H;assumption.
simpl in H0;decompose [or]H0.
subst;apply False_ind;intuition.
assumption.
Qed.
Lemma rank_eq :
forall (l : list nat) (x y : nat),
In x l
-> In y l
-> NoDup l
-> rank l 1 x = rank l 1 y
-> x = y.
Proof.
induction l;intros.
inversion H.
simpl in H2.
destruct (eq_nat_dec x a).
subst.
destruct (eq_nat_dec y a).
intuition.
assert (2 <= rank l 2 y).
apply acc_le_rank_in.
simpl in H0;decompose [or] H0.
subst;apply False_ind;intuition.
assumption.
apply False_ind;intuition.
destruct (eq_nat_dec y a).
subst.
assert (2 <= rank l 2 x).
apply acc_le_rank_in.
simpl in H;decompose [or] H.
apply False_ind;intuition.
assumption.
apply False_ind;intuition.
rewrite rank_S in H2.
rewrite (rank_S l 1 y) in H2.
apply eq_add_S in H2.
apply IHl.
simpl in H;decompose [or]H.
subst;apply False_ind;intuition.
assumption.
simpl in H0;decompose [or]H0.
subst;apply False_ind;intuition.
assumption.
inversion H1;assumption.
assumption.
Qed.
Lemma not_in_rank :
forall (l : list nat) (x : nat),
~In x l
-> rank l 1 x = S (S (length l)).
Proof.
induction l;intros;simpl.
reflexivity.
destruct (eq_nat_dec x a).
apply False_ind;subst;intuition.
rewrite rank_S.
apply eq_S.
apply IHl;intuition.
Qed.
Lemma rank_le_lth :
forall (l : list nat) (x : nat),
In x l
-> rank l 1 x <= length l.
Proof.
induction l;intros.
inversion H.
simpl.
destruct (eq_nat_dec x a).
intuition.
rewrite rank_S.
apply le_n_S.
apply IHl.
simpl in H;decompose [or]H.
apply False_ind;intuition.
assumption.
Qed.
Lemma in_rename_in :
forall (edg : list (nat*nat)) (l : list nat) (x y : nat),
NoDup l
-> (forall (a b : nat),
In (a,b) edg
-> In a l /\ In b l)
-> In (x,y) (rename_edg edg l)
-> In (rename_vert_inv__aux (rename_fun l) x,rename_vert_inv__aux (rename_fun l) y) edg.
Proof.
induction edg;intros.
inversion H1.
destruct a;simpl.
assert (In n l /\ In n0 l).
apply H0;intuition.
simpl in H1;decompose [or]H1.
inversion H3;subst.
rewrite (in_rename_in_aux).
rewrite (in_rename_in_aux).
left;reflexivity.
assumption.
intuition.
assumption.
intuition.
right.
apply IHedg.
assumption.
intros;apply H0;intuition.
assumption.
Qed.
Lemma in_rename_in_inv__aux :
forall (l : list nat) (x : nat),
x <= length l
-> x <> 0
-> In (rename_vert_inv__aux (rename_fun l) x) l.
Proof.
induction l;intros.
apply False_ind;intuition.
simpl.
destruct x.
apply False_ind;intuition.
destruct x.
intuition.
right.
rewrite (rename_fun_fst l 2 1).
unfold rename_fun in IHl.
apply IHl;intuition.
Qed.
Lemma in_rename_in_inv_aux :
forall (l : list nat) (x : nat),
x <= length l
-> x <> 0
-> NoDup l
-> rank l 1 (rename_vert_inv__aux (rename_fun l) x) = x.
Proof.
induction l;intros.
assert (x = 0).
intuition.
intuition.
simpl.
destruct x.
intuition.
destruct x.
destruct (eq_nat_dec a a).
reflexivity.
intuition.
destruct (eq_nat_dec (rename_vert_inv__aux (rename_fun_aux l 2) (S x))).
assert (In a l).
rewrite <-e.
assert (In (rename_vert_inv__aux (rename_fun l) (S x)) l).
apply in_rename_in_inv__aux.
intuition.
intuition.
rewrite (rename_fun_fst l 2 1).
unfold rename_fun in H2;assumption.
inversion H1;apply False_ind;intuition.
rewrite rank_S.
apply eq_S.
rewrite (rename_fun_fst l 2 1).
unfold rename_fun in IHl.
apply IHl.
intuition.
intuition.
inversion H1;assumption.
Qed.
Lemma in_rename_in_inv :
forall (edg : list (nat*nat)) (l : list nat) (x y : nat),
x <= length l
-> y <= length l
-> x <> 0
-> y <> 0
-> NoDup l
-> In (rename_vert_inv__aux (rename_fun l) x,rename_vert_inv__aux (rename_fun l) y) edg
-> In (x,y) (rename_edg edg l).
Proof.
induction edg;intros.
inversion H4.
destruct a;simpl.
simpl in H4;decompose [or]H4.
inversion H5.
subst.
rewrite in_rename_in_inv_aux;intuition.
rewrite in_rename_in_inv_aux;intuition.
right;apply IHedg;assumption.
Qed.
Lemma rename_vert_diff :
forall (l : list nat) (x y : nat),
NoDup l
-> x <= length l
-> y <= length l
-> x <> 0
-> y <> 0
-> x <> y
-> rename_vert_inv__aux (rename_fun l) x <> rename_vert_inv__aux (rename_fun l) y.
Proof.
induction l;intros.
assert (x = 0).
intuition.
apply False_ind;intuition.
simpl.
destruct x.
apply False_ind;intuition.
destruct y.
apply False_ind;intuition.
destruct x.
destruct y.
apply False_ind;intuition.
assert (In (rename_vert_inv__aux (rename_fun l) (S y)) l).
apply in_rename_in_inv__aux.
intuition.
intuition.
rewrite (rename_fun_fst l 2 1).
unfold rename_fun in H5.
unfold not;intro.
rewrite <-H6 in H5.
inversion H;intuition.
destruct y.
assert (In (rename_vert_inv__aux (rename_fun l) (S x)) l).
apply in_rename_in_inv__aux.
intuition.
intuition.
rewrite (rename_fun_fst l 2 1).
unfold rename_fun in H5.
unfold not;intro.
rewrite H6 in H5.
inversion H;intuition.
rewrite (rename_fun_fst l 2 1).
rewrite (rename_fun_fst l 2 1).
unfold rename_fun in IHl.
apply IHl.
inversion H;assumption.
intuition.
intuition.
intuition.
intuition.
intuition.
Qed.
Lemma rename_vert_inv_in :
forall (l l' : list nat) (y : nat),
In y l'
-> In (rename_vert_inv__aux (rename_fun l) y)
(rename_vert_inv_aux l' (rename_fun l)).
Proof.
induction l';intros.
inversion H.
simpl.
simpl in H;decompose [or]H.
left;subst;reflexivity.
right;apply IHl'.
assumption.
Qed.
Lemma in_rename_edg_le_lth :
forall (edg : list (nat*nat)) (l : list nat) (x y : nat),
In (x,y) (rename_edg edg l)
-> (forall (a b : nat),
In (a,b) edg
-> In a l /\ In b l)
-> x <= length l /\ y<= length l.
Proof.
induction edg;intros.
inversion H.
destruct a;simpl in H;decompose [or]H.
inversion H1;subst.
assert (In n l /\In n0 l).
apply H0;intuition.
split;apply rank_le_lth;intuition.
apply IHedg;intuition.
assert (In a l /\ In b l).
apply H0;intuition.
intuition.
assert (In a l /\ In b l).
apply H0;intuition.
intuition.
assert (In a l /\ In b l).
apply H0;intuition.
intuition.
assert (In a l /\ In b l).
apply H0;intuition.
intuition.
Qed.
Lemma sv_rename :
forall (l rl : list nat) (edg : list (nat*nat)) (x : nat),
sv (rename_vert_inv__aux (rename_fun l) x)
((rename_vert_inv__aux (rename_fun l) x) :: rename_vert_inv_aux rl (rename_fun l))
edg
-> NoDup l
-> (forall a : nat,
In a (x :: rl)
-> a <> 0)
-> (forall (a b : nat),
In (a,b) edg
-> In a l /\ In b l)
-> sv x (x :: rl) (rename_edg edg l).
Proof.
intros.
constructor.
intuition.
intros.
inversion H.
assert (x <= length l).
decompose [or] H8.
apply (proj1 ((in_rename_edg_le_lth edg l x y) H15 H2)).
apply (proj2 ((in_rename_edg_le_lth edg l y x) H15 H2)).
assert (y <= length l).
decompose [or] H8.
apply (proj2 ((in_rename_edg_le_lth edg l x y) H16 H2)).
apply (proj1 ((in_rename_edg_le_lth edg l y x) H16 H2)).
assert (z <= length l).
decompose [or] H9.
apply (proj2 ((in_rename_edg_le_lth edg l x z) H17 H2)).
apply (proj1 ((in_rename_edg_le_lth edg l z x) H17 H2)).
assert (In (rename_vert_inv__aux (rename_fun l) y,rename_vert_inv__aux (rename_fun l) z) edg \/
In (rename_vert_inv__aux (rename_fun l) z,rename_vert_inv__aux (rename_fun l) y) edg).
apply H11.
apply rename_vert_diff.
assumption.
assumption.
assumption.
apply H1;intuition.
apply H1;assumption.
assumption.
apply rename_vert_diff.
assumption.
assumption.
assumption.
apply H1;intuition.
apply H1;assumption.
assumption.
apply rename_vert_diff.
assumption.
assumption.
assumption.
apply H1;intuition.
apply H1;assumption.
clear H9;clear H10.
simpl in H7;decompose [or]H7.
assumption.
assumption.
simpl in H6;decompose [or]H6.
subst;intuition.
simpl;right;apply rename_vert_inv_in;assumption.
simpl in H7;decompose [or]H7.
subst;intuition.
simpl;right;apply rename_vert_inv_in;assumption.
decompose [or]H8;[left |right];apply in_rename_in;assumption.
decompose [or]H9;[left |right];apply in_rename_in;assumption.
decompose [or]H18;[left | right];apply in_rename_in_inv.
assumption.
assumption.
apply H1;intuition.
apply H1;assumption.
assumption.
assumption.
assumption.
assumption.
apply H1;assumption.
apply H1;assumption.
assumption.
assumption.
Qed.
Lemma rank_lth :
forall (l l' : list nat) (x : nat),
~In x l
-> length l < rank (l ++ x :: l') 1 x.
Proof.
induction l;intros;simpl.
destruct (eq_nat_dec x x);intuition.
destruct (eq_nat_dec x a).
subst;apply False_ind;intuition.
rewrite rank_S.
apply lt_n_S.
apply IHl.
intuition.
Qed.
Lemma rank_next_aux :
forall (l l' : list nat) (x y z : nat),
NoDup (x :: y :: z :: l)
-> rank (l ++ y :: z :: l') 1 z = S (rank (l ++ y :: z :: l') 1 y)
-> rank (l ++ x :: y :: z :: l') 1 z = S (rank (l ++ x :: y :: z :: l') 1 y).
Proof.
induction l;intros;simpl.
destruct (eq_nat_dec z x).
subst;apply False_ind;inversion H;intuition.
destruct (eq_nat_dec z y).
subst;apply False_ind;inversion H;inversion H4;intuition.
destruct (eq_nat_dec y x).
subst;apply False_ind;inversion H;inversion H4;intuition.
destruct (eq_nat_dec z z).
destruct (eq_nat_dec y y).
reflexivity.
intuition.
intuition.
intuition.
simpl in H0.
destruct (eq_nat_dec z a).
subst;apply False_ind;inversion H;inversion H4;inversion H8;intuition.
destruct (eq_nat_dec y a).
subst;apply False_ind;inversion H;inversion H4;intuition.
rewrite rank_S.
rewrite (rank_S (l ++ x :: y :: z :: l') 1).
apply eq_S.
apply IHl.
constructor.
unfold not;intro.
simpl in H1;decompose [or] H1;
subst;apply False_ind;inversion H;intuition.
constructor.
unfold not;intro.
simpl in H1;decompose [or] H1;
subst;apply False_ind;inversion H.
inversion H5;intuition.
inversion H6;intuition.
constructor.
inversion H;inversion H4;inversion H8;intuition.
inversion H;inversion H4;inversion H8;inversion H12;assumption.
simpl in H0.
rewrite rank_S in H0;apply eq_add_S in H0;
rewrite (rank_S (l ++ y :: z :: l') 1) in H0.
assumption.
Qed.
Lemma rank_next :
forall (l l' : list nat) (x y : nat),
NoDup (x :: y :: l)
-> rank (rev l ++ x :: y :: l') 1 y
=
S (rank (rev l ++ x :: y :: l') 1 x).
Proof.
induction l;intros;simpl.
destruct (eq_nat_dec y x).
subst;apply False_ind;inversion H;intuition.
destruct (eq_nat_dec y y).
destruct (eq_nat_dec x x).
reflexivity.
intuition.
intuition.
assert ((rev l ++ a :: nil) ++ x :: y :: l' = rev l ++ a :: x :: y :: l').
rewrite <-ass_app;intuition.
rewrite H0.
apply rank_next_aux.
constructor.
unfold not;intro.
simpl in H1;decompose [or]H1.
subst;apply False_ind;inversion H;intuition.
subst;apply False_ind;inversion H;inversion H5;intuition.
assert (In a l).
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
assumption.
inversion H;inversion H7;inversion H11;intuition.
constructor.
unfold not;intro.
simpl in H1;decompose [or] H1.
subst;apply False_ind;inversion H;intuition.
assert (In x l).
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
assumption.
inversion H;intuition.
constructor.
unfold not;intro.
assert (In y l).
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
assumption.
inversion H;inversion H6;intuition.
eapply NoDup_perm.
apply Permutation_rev.
inversion H;inversion H4;inversion H8;assumption.
apply IHl.
constructor.
unfold not;intro.
simpl in H1;decompose [or] H1.
subst;inversion H;intuition.
inversion H;intuition.
constructor.
inversion H;inversion H4;intuition.
inversion H;inversion H4;inversion H8;assumption.
Qed.
Lemma rank_le :
forall (l l' : list nat) (x : nat),
NoDup (x :: l)
-> rank (rev l ++ x :: l') 1 x = S (length l).
Proof.
induction l;intros;simpl.
destruct (eq_nat_dec x x);intuition.
assert ((rev l ++ a :: nil) ++ x :: l' = rev l ++ a :: x :: l').
rewrite <-ass_app;intuition.
rewrite H0.
assert (rank (rev l ++ a :: x :: l') 1 a = S (length l)).
apply IHl.
inversion H;assumption.
rewrite rank_next.
apply eq_S.
assumption.
constructor.
unfold not;intro.
simpl in H2;decompose [or] H2.
subst;inversion H;intuition.
inversion H;inversion H7;intuition.
constructor.
inversion H;intuition.
inversion H;inversion H5;intuition.
Qed.
Lemma rename_rev_dec_aux :
forall (l l' : list nat) (a x : nat),
NoDup l
-> In x (rename_vert_aux l (rev l ++ a :: l'))
-> x <= length l.
Proof.
induction l;intros.
inversion H0.
assert ((rev l ++ a :: nil) ++ a0 :: l' = rev l ++ a :: a0 :: l').
rewrite <-ass_app;intuition.
simpl in H0;decompose [or] H0.
rewrite H1 in H2.
rewrite <-H2.
rewrite rank_le;intuition.
assert (x <= length l).
eapply IHl.
inversion H;assumption.
rewrite H1 in H2.
eassumption.
simpl;intuition.
Qed.
Lemma rename_rev_dec_ext :
forall (l l' : list nat),
NoDup l
-> is_strict_dec (rename_vert_aux l (rev l ++ l')).
Proof.
induction l;intros;simpl.
constructor.
assert ((rev l ++ a :: nil) ++ l' = rev l ++ a :: l').
rewrite <-ass_app;intuition.
apply strict_dec.
intros.
assert (length l < rank ((rev l ++ a :: nil) ++ l') 1 a).
rewrite H0.
rewrite rank_le.
intuition.
assumption.
assert (x <= length l).
rewrite H0 in H1.
eapply rename_rev_dec_aux.
inversion H;assumption.
eassumption.
intuition.
rewrite H0.
apply IHl.
inversion H;assumption.
Qed.
Lemma rename_rev_dec :
forall (l : list nat),
NoDup l
-> is_strict_dec (rename_vert_aux l (rev l)).
Proof.
intros;assert (rev l = rev l ++ nil);intuition.
rewrite H0;apply rename_rev_dec_ext;assumption.
Qed.
Lemma lth_rename_vert_eq_aux :
forall (l l' l0 l'0 : list nat),
NoDup l
-> NoDup l'
-> length l = length l'
-> rename_vert_aux l (rev l ++ l0) = rename_vert_aux l' (rev l' ++ l'0).
Proof.
induction l;intros.
destruct l';simpl.
reflexivity.
inversion H1.
induction l'.
inversion H1.
simpl.
assert ((rev l ++ a :: nil) ++ l0 = (rev l ++ a :: l0)).
rewrite <-ass_app;intuition.
rewrite H2.
rewrite rank_le.
assert ((rev l'++ a0 :: nil) ++ l'0 = rev l'++a0 :: l'0).
rewrite <-ass_app;intuition.
rewrite H3.
rewrite rank_le.
simpl in H1;rewrite H1.
rewrite (IHl l' (a :: l0) (a0 :: l'0)).
reflexivity.
inversion H;assumption.
inversion H0;assumption.
intuition.
assumption.
assumption.
Qed.
Lemma strict_inc_rename_aux :
forall (l l' : list nat),
NoDup l
-> NoDup l'
-> (forall (y : nat),
In y l'
-> ~In y l)
-> (forall (x : nat),
In x (rename_vert_aux l (l' ++ l))
-> length l' < x).
Proof.
induction l;intros.
simpl in H2;intuition.
simpl in H2.
decompose [or] H2.
rewrite <-H3;apply rank_lth.
unfold not;intro.
assert (~In a (a :: l)).
apply H1;assumption.
intuition.
assert (l' ++ a :: l = (l' ++ a :: nil) ++ l).
rewrite <-ass_app;intuition.
assert (length (l' ++a :: nil) < x).
apply IHl.
inversion H;assumption.
assert (NoDup (a :: l')).
constructor.
unfold not;intro.
assert (~In a (a :: l)).
apply H1;assumption.
intuition.
assumption.
apply (NoDup_perm nat (a :: l')).
apply Permutation_cons_app.
assert (l' ++ nil = l').
intuition.
rewrite H6;apply Permutation_refl.
assumption.
intros.
apply in_app_or in H5.
decompose [or] H5.
assert (~In y (a :: l)).
apply H1;intuition.
intuition.
simpl in H6;decompose [or]H6.
subst;inversion H;assumption.
intuition.
rewrite <-H4;assumption.
assert (length (l'++ a :: nil) = length (a :: l')).
apply Permutation_length.
apply Permutation_sym;apply Permutation_cons_app.
assert (l' ++ nil = l').
intuition.
rewrite H6;apply Permutation_refl.
rewrite H6 in H5;simpl in H6;intuition.
Qed.
Lemma rank_app_eq :
forall (l l' : list nat) (x : nat),
~In x l
-> rank (l ++ x :: l') 1 x = length (l ++ x :: nil).
Proof.
induction l;intros;simpl.
destruct (eq_nat_dec x x).
reflexivity.
intuition.
destruct (eq_nat_dec x a).
subst;apply False_ind;intuition.
rewrite rank_S.
apply eq_S.
apply IHl;intuition.
Qed.
Lemma strict_inc_rename :
forall (l l' : list nat),
NoDup l
-> NoDup l'
-> (forall (y : nat),
In y l'
-> ~In y l)
-> is_strict_inc (rename_vert_aux l (l' ++ l)).
Proof.
induction l;intros;simpl.
constructor.
apply strict_inc_add_hd.
assert (l' ++ a :: l = (l' ++ a :: nil) ++ l).
rewrite <-ass_app;intuition.
rewrite H2;apply IHl.
inversion H;assumption.
apply (NoDup_perm nat (a :: l')).
apply Permutation_cons_app.
assert (l' ++ nil = l').
intuition.
rewrite H3;apply Permutation_refl.
constructor.
unfold not;intro.
assert (~In a (a :: l)).
apply H1;assumption.
intuition.
assumption.
intros.
apply in_app_or in H3.
decompose [or] H3.
assert (~In y (a :: l)).
apply H1;assumption.
intuition.
simpl in H4;decompose [or] H4.
subst;inversion H;assumption.
intuition.
intros.
assert (l' ++ a :: l = (l' ++ a ::nil) ++ l).
rewrite <-ass_app;intuition.
rewrite H3 in H2.
assert (length (l' ++ a :: nil) < y).
apply (strict_inc_rename_aux l (l' ++ a :: nil)).
inversion H;assumption.
apply (NoDup_perm nat (a :: l')).
apply Permutation_cons_app.
assert (l' ++ nil = l').
intuition.
rewrite H4;apply Permutation_refl.
constructor.
unfold not;intro.
assert (~In a (a :: l)).
apply H1;assumption.
intuition.
assumption.
intros.
apply in_app_or in H4.
decompose [or] H4.
assert (~In y0 (a :: l)).
apply H1;assumption.
intuition.
simpl in H5;decompose [or] H5.
subst;inversion H;assumption.
intuition.
assumption.
rewrite rank_app_eq.
assumption.
unfold not;intro.
assert (~In a (a :: l)).
apply H1;assumption.
intuition.
Qed.
Lemma rename_lth_eq :
forall (l l' l0 l'0 : list nat),
length l = length l'
-> length l0 = length l'0
-> (forall (y : nat),
In y l0 -> ~In y l)
-> (forall (y : nat),
In y l'0 -> ~In y l')
-> NoDup l
-> NoDup l'
-> rename_vert_aux l (l0 ++ l) = rename_vert_aux l' (l'0 ++ l').
Proof.
induction l;intros.
destruct l'.
simpl;reflexivity.
inversion H.
induction l'.
inversion H.
simpl.
rewrite rank_app_eq.
rewrite rank_app_eq.
assert (l0 ++ a :: l = (l0 ++ (a :: nil)) ++ l).
rewrite <-ass_app;intuition.
assert (l'0 ++ a0 :: l' = (l'0 ++ a0 :: nil) ++ l').
rewrite <-ass_app;intuition.
rewrite H5;rewrite H6.
assert (length (l0 ++ a :: nil) = length (l'0 ++ a0 :: nil)).
assert (length (l0 ++ a :: nil) = length (a :: l0)).
apply Permutation_length.
apply Permutation_sym;apply Permutation_cons_app.
assert (l0 ++ nil = l0).
intuition.
rewrite H7;apply Permutation_refl.
rewrite H7.
assert (length (l'0 ++ a0 :: nil) = length (a0 :: l'0)).
apply Permutation_length.
apply Permutation_sym;apply Permutation_cons_app.
assert (l'0 ++ nil = l'0).
intuition.
rewrite H8;apply Permutation_refl.
rewrite H8.
simpl.
apply eq_S;assumption.
rewrite H7.
assert (rename_vert_aux l ((l0 ++ a :: nil) ++ l) = rename_vert_aux l' ((l'0 ++ a0 :: nil) ++ l')).
apply IHl.
intuition.
assumption.
unfold not;intros.
apply in_app_or in H8;decompose [or] H8.
assert (~In y (a :: l)).
apply H1;assumption.
intuition.
simpl in H10;decompose [or] H10.
subst;inversion H3;intuition.
assumption.
unfold not;intros.
apply in_app_or in H8;decompose [or] H8.
assert (~In y (a0 :: l')).
apply H2;assumption.
intuition.
simpl in H10;decompose [or] H10.
subst;inversion H4;intuition.
assumption.
inversion H3;assumption.
inversion H4;assumption.
rewrite H8;reflexivity.
unfold not;intro.
assert (~In a0 (a0 :: l')).
apply H2;assumption.
intuition.
unfold not;intro.
assert (~In a (a :: l)).
apply H1;assumption.
intuition.
Qed.
Lemma lth_rename_eq :
forall (l l' : list nat),
NoDup l
-> NoDup l'
-> length l = length l'
-> rename_vert_aux l l = rename_vert_aux l' l'.
Proof.
intros.
assert (rename_vert_aux l (nil ++ l) = rename_vert_aux l' (nil ++ l')).
apply rename_lth_eq.
assumption.
reflexivity.
intuition.
intuition.
assumption.
assumption.
simpl in H2;assumption.
Qed.
Lemma rename_rev_rev_eq :
forall (l : list nat),
NoDup l
-> rename_vert_aux l l = rename_vert_aux (rev l) (rev l).
Proof.
intros;apply lth_rename_eq.
assumption.
eapply NoDup_perm.
apply Permutation_rev.
assumption.
symmetry;apply rev_length.
Qed.
Fixpoint intervalle_dec (n : nat) {struct n} : list nat :=
match n with
| 1 => 1 :: nil
| S m => S m :: intervalle_dec m
| 0 => nil
end.
Fixpoint intervalle_inc_aux (n : nat) (acc : list nat) {struct n}: list nat :=
match n with
| 0 => acc
| S m => intervalle_inc_aux m (S m :: acc)
end.
Definition intervalle_inc (n : nat) : list nat :=
intervalle_inc_aux n nil.
Lemma intervalle_lth :
forall (n : nat),
length (intervalle_dec n) = n.
Proof.
induction n;intros;simpl.
reflexivity.
assert ({n = 0}+{n <> 0}).
apply eq_nat_dec.
destruct H.
rewrite e.
reflexivity.
assert (exists x : nat, n = S x).
destruct n;[ | exists n];intuition.
inversion H;rewrite H0.
rewrite <-H0.
simpl;intuition.
Qed.
Lemma in_interv_le :
forall (x n : nat),
In x (intervalle_dec n)
-> x <= n.
Proof.
induction n;simpl;intros.
intuition.
assert ({n = 0} + {n <> 0}).
apply eq_nat_dec.
destruct H0.
rewrite e in H.
simpl in H;decompose [or] H;intuition.
assert (exists y : nat, n = S y).
destruct n;[|exists n];intuition.
inversion H0;rewrite H1 in H.
rewrite <-H1 in H.
simpl in H;decompose [or] H.
intuition.
apply le_S;apply IHn;assumption.
Qed.
Lemma only_in_interv_le :
forall (n x : nat),
0 < x
-> x <= n
-> In x (intervalle_dec n).
Proof.
induction n;intros.
apply False_ind;intuition.
simpl.
destruct n.
assert (x = 1);subst;intuition.
destruct (le_gt_dec x (S n)).
simpl;right;apply IHn;assumption.
assert (x = S (S n));subst;intuition.
Qed.
Lemma strict_dec_interv :
forall (n : nat),
is_strict_dec (intervalle_dec n).
Proof.
induction n;intros;simpl.
constructor.
assert ({n = 0} + {n <> 0}).
apply eq_nat_dec.
destruct H.
rewrite e.
constructor.
assert (exists y : nat, n = S y).
destruct n;[|exists n];intuition.
inversion H;rewrite H0.
rewrite <-H0.
apply strict_dec.
intros.
apply le_lt_n_Sm;apply in_interv_le;assumption.
assumption.
Qed.
Lemma rename_semi_rev_aux :
forall (l : list nat),
NoDup l
-> rename_vert_aux l (rev l) = intervalle_dec (length l).
Proof.
induction l;intros;simpl.
reflexivity.
assert ({length l = 0}+{length l <> 0}).
apply eq_nat_dec.
destruct H0.
assert (l = nil).
apply lth_0_nil;assumption.
subst;simpl.
destruct (eq_nat_dec a a).
reflexivity.
intuition.
assert (exists y : nat, length l = S y).
destruct (length l).
intuition.
exists n0;intuition.
inversion H0;rewrite H1.
rewrite <-H1.
rewrite rank_app_eq.
assert (length (rev l ++ a :: nil) = length (a :: rev l)).
apply Permutation_length.
apply Permutation_sym;apply Permutation_cons_app.
rewrite <-app_nil_end;apply Permutation_refl.
rewrite H2.
simpl.
assert (length (rev l) = length l).
apply rev_length.
rewrite H3.
rewrite (lth_rename_vert_eq_aux l l (a :: nil) nil).
rewrite <-app_nil_end.
rewrite IHl.
reflexivity.
inversion H;assumption.
inversion H;assumption.
inversion H;assumption.
reflexivity.
unfold not;intro.
assert (In a l).
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
assumption.
inversion H;intuition.
Qed.
Lemma in_rename_vert_le_lth_aux :
forall (l l' : list nat) (x : nat),
In x (rename_vert_aux l l')
-> (forall (y : nat),
In y l
-> In y l')
-> x <= length l'.
Proof.
induction l;intros;simpl.
inversion H.
simpl in H;decompose [or] H.
rewrite <-H1.
apply rank_le_lth.
apply H0;intuition.
apply IHl.
assumption.
intuition.
Qed.
Lemma in_rename_vert_le_lth :
forall (l : list nat) (x : nat),
In x (rename_vert_aux l l)
-> x <= length l.
Proof.
intros;apply (in_rename_vert_le_lth_aux l l);intuition.
Qed.
Lemma list_decompose_inv :
forall (l : list nat),
l <> nil
-> exists y : nat, exists l' : list nat,
l = l' ++ y :: nil.
Proof.
intros;induction l.
intuition.
induction l.
exists a.
exists (@nil nat).
simpl;reflexivity.
assert (exists y : nat, exists l' : list nat, a0 :: l = l' ++ y :: nil).
apply IHl.
discriminate.
inversion H0.
inversion H1.
destruct x0.
inversion H2;subst.
exists x.
exists (a :: nil).
intuition.
inversion H2.
exists x.
exists (a :: n :: x0).
intuition.
Qed.
Lemma inc_dec_perm :
forall (l l' : list nat),
is_strict_inc l
-> is_strict_dec l'
-> Permutation l l'
-> rev l' = l.
Proof.
induction l;intros.
assert (l' = nil).
apply Permutation_nil;assumption.
subst;intuition.
destruct l'.
assert (a :: l = nil).
apply Permutation_nil.
apply Permutation_sym;assumption.
discriminate.
assert (exists y : nat, exists l'' : list nat, n :: l' = l'' ++ y :: nil).
apply list_decompose_inv;discriminate.
inversion H2;inversion H3.
rewrite H4.
assert (rev (x0 ++ x :: nil) = x :: rev x0).
apply rev_unit.
rewrite H5.
assert (is_strict_inc (x :: rev x0)).
rewrite <-H4 in H5.
rewrite <-H5;apply rev_dec_inc.
assumption.
assert (a = x).
assert (In x (a :: l)).
eapply Permutation_in.
apply Permutation_sym;eassumption.
rewrite H4;intuition.
destruct (eq_nat_dec x a).
subst;reflexivity.
assert (In x l).
simpl in H7;decompose [or]H7;subst;intuition.
assert (a < x).
eapply in_strict_sort.
eassumption.
assumption.
assert (In a (n :: l')).
eapply Permutation_in.
eassumption.
intuition.
assert (In a (x :: rev x0)).
rewrite <-H4 in H5.
rewrite <-H5.
eapply Permutation_in.
apply Permutation_rev.
assumption.
assert (x < a).
eapply in_strict_sort.
eassumption.
simpl in H11;decompose [or] H11.
apply False_ind;intuition.
assumption.
apply False_ind;intuition.
rewrite H7.
rewrite (IHl x0).
reflexivity.
eapply is_strict_inc_tail;eassumption.
assert (is_strict_dec (rev (rev x0))).
apply rev_inc_dec.
eapply is_strict_inc_tail;eassumption.
rewrite rev_involutive in H8;assumption.
assert (Permutation (a :: l) (x :: rev x0)).
rewrite <-H4 in H5;rewrite <-H5.
apply Permutation_trans with (l' := n :: l').
assumption.
apply Permutation_rev.
rewrite H7 in H8.
assert (Permutation (x :: l) (x :: x0)).
apply Permutation_trans with (l' := x :: rev x0).
assumption.
constructor.
apply Permutation_sym;apply Permutation_rev.
eapply Permutation_cons_inv;eassumption.
Qed.
Lemma rename_semi_rev_l :
forall (l : list nat),
NoDup l
-> rename_vert_aux (rev l) l = rev (rename_vert_aux l l).
Proof.
intros;assert (rev (rev (rename_vert_aux l l)) = rev (rename_vert_aux (rev l) l)).
apply inc_dec_perm.
apply rev_dec_inc.
assert (is_strict_dec (rename_vert_aux (rev l) (rev (rev l)))).
rewrite rename_semi_rev_aux.
apply strict_dec_interv.
eapply NoDup_perm.
apply Permutation_rev.
assumption.
rewrite rev_involutive in H0.
assumption.
apply rev_inc_dec.
assert (is_strict_inc (rename_vert_aux l (nil ++ l))).
apply strict_inc_rename.
assumption.
constructor.
intuition.
simpl in H0;assumption.
assert (Permutation (rename_vert_aux (rev l) l) (rename_vert_aux l l)).
assert (Permutation (rename_vert_aux (rev l) (rev (rev l))) (rename_vert_aux l l)).
rewrite rev_involutive.
apply renaming_perm.
apply Permutation_sym;apply Permutation_rev.
rewrite rev_involutive in H0;assumption.
apply Permutation_trans with (l' := rename_vert_aux (rev l) l).
apply Permutation_sym;apply Permutation_rev.
apply Permutation_trans with (l' := rename_vert_aux l l).
assumption.
apply Permutation_rev.
assert (rev (rev (rev (rename_vert_aux l l))) = rev (rev (rename_vert_aux (rev l) l))).
rewrite H0;reflexivity.
rewrite rev_involutive in H1;rewrite rev_involutive in H1.
symmetry;assumption.
Qed.
Lemma rename_semi_rev :
forall (l : list nat),
NoDup l
-> rename_vert_aux l (rev l) = rev (rename_vert_aux l l).
Proof.
intros;assert (rename_vert_aux (rev (rev l)) (rev l) = rev (rename_vert_aux (rev l) (rev l))).
apply rename_semi_rev_l.
eapply NoDup_perm.
apply Permutation_rev.
assumption.
rewrite (lth_rename_eq (rev l) l) in H0.
rewrite rev_involutive in H0;assumption.
eapply NoDup_perm.
apply Permutation_rev.
assumption.
assumption.
apply rev_length.
Qed.
Lemma rename_inv_rev_aux :
forall (l rl ll : list nat),
rename_vert_inv_aux (rev rl ++ ll) (rename_fun l)
= rev (rename_vert_inv_aux rl (rename_fun l)) ++ (rename_vert_inv_aux ll (rename_fun l)).
Proof.
induction rl;intros.
simpl;reflexivity.
simpl.
assert ((rev rl ++ a :: nil) ++ ll = rev rl ++ a :: ll).
rewrite <-ass_app;intuition.
rewrite H.
rewrite IHrl.
simpl.
assert ((rename_vert_inv__aux (rename_fun l) a :: nil) ++ rename_vert_inv_aux ll (rename_fun l) =
rename_vert_inv__aux (rename_fun l) a :: rename_vert_inv_aux ll (rename_fun l)).
intuition.
rewrite app_ass.
rewrite H0.
reflexivity.
Qed.
Lemma rename_inv_rev :
forall (l rl : list nat),
NoDup l
-> rev (rename_vert_inv_aux (rev rl) (rename_fun l))
= rename_vert_inv_aux rl (rename_fun l).
Proof.
intros.
assert (rev rl = rev rl ++ nil).
intuition.
rewrite H0.
rewrite rename_inv_rev_aux.
simpl.
rewrite <-app_nil_end.
apply rev_involutive.
Qed.
Lemma peo_renaming2 :
forall (l vert : list nat) (edg : list (nat*nat)),
_peo l vert edg
-> NoDup vert
-> (forall (a b : nat),
In (a,b) edg
-> In a vert /\ In b vert)
-> _peo (rename_vert_aux l (rev l)) (rename_vert_aux vert (rev l)) (rename_edg edg (rev l)).
Proof.
induction 1;intros.
constructor;intros.
apply renaming_perm;assumption.
rewrite rename_semi_rev in H3.
assert (rev (rev (rename_vert_aux l l)) = rev rl ++ x :: rev ll).
apply rev_app;assumption.
rewrite rev_involutive in H4.
assert (rev l = rename_vert_inv (rev rl ++ x :: rev ll) (rev l)).
apply rename_inv.
eapply NoDup_perm.
apply Permutation_rev.
eapply NoDup_perm;eassumption.
unfold rename_vert;rewrite <-rename_rev_rev_eq.
assumption.
eapply NoDup_perm;eassumption.
rewrite rename_inv_app in H5.
unfold rename_vert_inv in H5;simpl in H5.
assert (0 < x).
apply (positive_in_rename l l);intuition.
rewrite H4;intuition.
assert (exists y : nat, x = S y).
destruct x.
apply False_ind;intuition.
exists x;reflexivity.
inversion H7.
assert (sv (rename_vert_inv__aux (rename_fun (rev l)) x)
((rename_vert_inv__aux (rename_fun (rev l)) x) :: rev (rename_vert_inv_aux (rev rl) (rename_fun (rev l))))
edg).
eapply H0.
assert (rev (rev l) = rev (rename_vert_inv_aux (rev ll) (rename_fun (rev l))) ++ rename_vert_inv__aux (rename_fun (rev l)) x :: rev (rename_vert_inv_aux (rev rl) (rename_fun (rev l)))).
apply rev_app;assumption.
rewrite rev_involutive in H9.
eassumption.
apply sv_rename.
rewrite <-rename_inv_rev.
assumption.
eapply NoDup_perm.
apply Permutation_rev.
eapply NoDup_perm;eassumption.
eapply NoDup_perm.
apply Permutation_rev.
eapply NoDup_perm;eassumption.
intros;assert (0 < a).
apply (positive_in_rename l l);intuition.
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
rewrite H3;intuition.
intuition.
intros.
assert (In a vert /\ In b vert).
apply H2;assumption.
split;eapply Permutation_in.
apply Permutation_rev.
eapply Permutation_in.
eassumption.
intuition.
apply Permutation_rev.
eapply Permutation_in.
eassumption.
intuition.
unfold not;intro.
simpl.
assert (0 < 0).
apply (positive_in_rename l l 0).
intuition.
rewrite H4;intuition.
intuition.
eapply NoDup_perm;eassumption.
Qed.
Lemma peo_clique :
forall (g : graph),
peo (rev (vertices g)) g
-> (forall (x : nat),
In x (vertices g)
-> is_clique g (x :: get_nghbs g x)
(length (get_nghbs g x) + 1)).
Proof.
intros.
constructor.
constructor.
apply not_in_x_nghbsx.
apply NoDup_get_nghbs.
simpl;intuition.
intros.
inversion H.
clear H4;clear H6;clear H7;clear H8.
assert (exists ll : list nat, exists rl : list nat, vertices g = ll ++ x :: rl).
apply in_ex_app;assumption.
inversion H4;inversion H6;clear H4;clear H6.
assert (sv x (x :: rev x1) (edges g)).
apply (H5 x (rev x2) (rev x1)).
apply rev_app;assumption.
simpl in H1;decompose [or] H1.
subst.
simpl in H2;decompose [or] H2.
apply False_ind;intuition.
right;apply edges_nghbs;assumption.
simpl in H2;decompose [or] H2.
subst.
left;apply edges_nghbs;assumption.
inversion H4.
apply H10.
assert (~In x (get_nghbs g x)).
apply not_in_x_nghbsx.
unfold not in *;intro;subst;apply (H14 H6).
assert (~In x (get_nghbs g x)).
apply not_in_x_nghbsx.
unfold not in *;intro;subst;apply (H14 H8).
assumption.
simpl;right.
eapply in_rev_sv;eassumption.
simpl;right.
eapply in_rev_sv;eassumption.
right;apply edges_nghbs;assumption.
right;apply edges_nghbs;assumption.
intros.
simpl in H1;decompose [or] H1.
subst;assumption.
rewrite vertices_edges.
assert (In (x0,x) (edges g)).
apply edges_nghbs;assumption.
apply (proj1 ((in_vertices (edges g) x0 x) H3)).
Qed.
Definition my_peo : list nat := peo_search my_graph.
Lemma my_peo_eq : my_peo = peo_search my_graph.
Proof.
unfold my_peo;reflexivity.
Qed.
Lemma inc_perm_eq :
forall (l l' : list nat),
is_strict_inc l
-> is_strict_inc l'
-> Permutation l l'
-> l' = l.
Proof.
intros;assert (is_strict_dec (rev l')).
apply rev_inc_dec;assumption.
assert (rev (rev l') = l).
apply inc_dec_perm.
assumption.
assumption.
apply Permutation_trans with (l' := l').
assumption.
apply Permutation_rev.
rewrite rev_involutive in H3;assumption.
Qed.
Lemma in_rename_edg_l :
forall (edg : list (nat*nat)) (l : list nat) (x y : nat),
In (x,y) (rename_edg edg l)
-> (forall (a b : nat),
In (a,b) edg
-> In a l /\ In b l)
-> 0 < x /\ x <= length l.
Proof.
split;induction edg;intros.
inversion H.
destruct a;simpl in H.
decompose [or]H.
inversion H1;subst.
assert (1 <= rank l 1 n).
assert ({In n l}+{~In n l}).
apply In_dec;apply eq_nat_dec.
destruct H2.
apply acc_le_rank_in;assumption.
rewrite not_in_rank;intuition.
intuition.
apply IHedg;intuition.
assert (In a l /\ In b l);[apply H0|];intuition.
assert (In a l /\ In b l);[apply H0|];intuition.
assert (In a l /\ In b l);[apply H0|];intuition.
assert (In a l /\ In b l);[apply H0|];intuition.
inversion H.
destruct a;simpl in H.
decompose [or]H.
inversion H1.
apply rank_le_lth.
assert(In n l /\ In n0 l);[apply H0|];intuition.
apply IHedg.
assumption.
intros;assert (In a l /\ In b l);[apply H0|];intuition.
Qed.
Lemma in_rename_edg_r :
forall (edg : list (nat*nat)) (l : list nat) (x y : nat),
In (x,y) (rename_edg edg l)
-> (forall (a b : nat),
In (a,b) edg
-> In a l /\ In b l)
-> 0 < y /\ y <= length l.
Proof.
split;induction edg;intros.
inversion H.
destruct a;simpl in H.
decompose [or]H.
inversion H1;subst.
assert (1 <= rank l 1 n0).
assert ({In n0 l}+{~In n0 l}).
apply In_dec;apply eq_nat_dec.
destruct H2.
apply acc_le_rank_in;assumption.
rewrite not_in_rank;intuition.
intuition.
apply IHedg;intuition.
assert (In a l /\ In b l);[apply H0|];intuition.
assert (In a l /\ In b l);[apply H0|];intuition.
assert (In a l /\ In b l);[apply H0|];intuition.
assert (In a l /\ In b l);[apply H0|];intuition.
inversion H.
destruct a;simpl in H.
decompose [or]H.
inversion H1.
apply rank_le_lth.
assert(In n l /\ In n0 l);[apply H0|];intuition.
apply IHedg.
assumption.
intros;assert (In a l /\ In b l);[apply H0|];intuition.
Qed.
Lemma rename_interv :
forall (l : list nat),
NoDup l
-> rev (rename_vert_aux l l) = intervalle_dec (length l).
Proof.
intros;rewrite <-rename_semi_rev.
apply rename_semi_rev_aux;assumption.
assumption.
Qed.
Lemma rename_hd :
forall (l : list nat) (a : nat),
NoDup (a :: l)
-> rename_vert_aux (a :: l) (a :: l) = 1 :: rename_vert_aux l (a :: l).
Proof.
induction l;intros;simpl.
destruct (eq_nat_dec a a).
reflexivity.
intuition.
destruct (eq_nat_dec a a0).
subst;apply False_ind;inversion H;intuition.
destruct (eq_nat_dec a a).
destruct (eq_nat_dec a0 a0).
reflexivity.
intuition.
intuition.
Qed.
Lemma eq_vert_aux_aux :
forall (l : list nat) (x a : nat),
In (S x) (rename_vert_aux l (a :: l))
-> 0 < x
-> NoDup (a :: l)
-> In x (rename_vert_aux l l).
Proof.
intros.
assert (In (S x) (rename_vert_aux (a :: l) (a :: l))).
rewrite rename_hd;intuition.
assert (x <= length l).
apply le_S_n.
assert (length (a :: l) = S (length l)).
simpl;reflexivity.
rewrite <-H3;apply in_rename_vert_le_lth;assumption.
assert (In x (intervalle_dec (length l))).
apply only_in_interv_le;assumption.
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
rewrite rename_interv.
assumption.
inversion H1;assumption.
Qed.
Lemma eq_vert_aux :
forall (l : list nat) (edg : list (nat*nat)) (x : nat),
In x (rename_vert_aux l l)
-> NoDup l
-> (forall (z : nat),
In z l
-> exists a: nat, In (z,a) edg \/ In (a,z) edg)
-> exists y : nat, In (rename_vert_inv__aux (rename_fun l) x,y) edg
\/ In (y,rename_vert_inv__aux (rename_fun l) x) edg.
Proof.
induction l;intros;simpl.
inversion H.
assert (0 < x).
apply (positive_in_rename (a :: l) (a :: l));intuition.
destruct x.
apply False_ind;intuition.
simpl in H;destruct (eq_nat_dec a a).
destruct x.
apply H1;intuition.
rewrite (rename_fun_fst l 2 1).
unfold rename_fun in IHl.
apply IHl.
decompose [or]H.
inversion H3.
eapply eq_vert_aux_aux.
eassumption.
intuition.
assumption.
inversion H0;assumption.
intuition.
intuition.
Qed.
Lemma eq_vert_aux2_l :
forall (edg : list (nat*nat)) (l : list nat) (x y : nat),
In (rename_vert_inv__aux (rename_fun l) x,y) edg
-> 0 < x
-> x <= length l
-> NoDup l
-> (forall (y z : nat),
In (y,z) edg
-> In y l /\ In z l)
-> In (x,rank l 1 y) (rename_edg edg l).
Proof.
induction edg;intros.
inversion H.
destruct a;simpl.
destruct (eq_nat_dec y n0).
subst.
destruct (eq_nat_dec x (rank l 1 n)).
subst;left;reflexivity.
right;apply IHedg.
simpl in H;decompose [or] H.
inversion H4.
assert (x = rank l 1 n).
rewrite H6.
rewrite in_rename_in_inv_aux.
reflexivity.
assumption.
intuition.
assumption.
apply False_ind;intuition.
assumption.
assumption.
assumption.
assumption.
intros;apply H3;intuition.
right;apply IHedg.
simpl in H;decompose [or] H.
inversion H4;apply False_ind;intuition.
assumption.
assumption.
assumption.
assumption.
intros;apply H3;intuition.
Qed.
Lemma eq_vert_aux2_r :
forall (edg : list (nat*nat)) (l : list nat) (x y : nat),
In (y,rename_vert_inv__aux (rename_fun l) x) edg
-> 0 < x
-> x <= length l
-> NoDup l
-> (forall (y z : nat),
In (y,z) edg
-> In y l /\ In z l)
-> In (rank l 1 y,x) (rename_edg edg l).
Proof.
induction edg;intros.
inversion H.
destruct a;simpl.
destruct (eq_nat_dec y n).
subst.
destruct (eq_nat_dec x (rank l 1 n0)).
subst;left;reflexivity.
right;apply IHedg.
simpl in H;decompose [or] H.
inversion H4.
assert (x = rank l 1 n0).
rewrite H6.
rewrite in_rename_in_inv_aux.
reflexivity.
assumption.
intuition.
assumption.
apply False_ind;intuition.
assumption.
assumption.
assumption.
assumption.
intros;apply H3;intuition.
right;apply IHedg.
simpl in H;decompose [or] H.
inversion H4;apply False_ind;intuition.
assumption.
assumption.
assumption.
assumption.
intros;apply H3;intuition.
Qed.
Lemma eq_vert_aux3 :
forall (edg : list (nat*nat)) (l : list nat) (x : nat),
NoDup l
-> (forall (y z : nat),
In (y,z) edg
-> In y l /\ In z l)
-> (forall (y : nat),
In y l
-> exists z : nat, In (y,z) edg \/ In (z,y) edg)
-> is_strict_inc (rename_vert_aux l l)
-> is_strict_ord edg
-> (In x (rename_vert l) <->
In x (edges_to_vertices (lto_edges (rename_edg edg l)))).
Proof.
split;intros.
assert (exists y : nat, In (rename_vert_inv__aux (rename_fun l) x,y) edg \/ In (y,rename_vert_inv__aux (rename_fun l) x) edg).
apply (eq_vert_aux l edg x).
unfold rename_vert in H3;assumption.
assumption.
assumption.
assert (0 < x).
apply (positive_in_rename l l).
intuition.
unfold rename_vert in H3;assumption.
assert (x <= length l).
apply in_rename_vert_le_lth.
unfold rename_vert in H3;assumption.
assert (exists y : nat, In (x,y) (rename_edg edg l) \/ In (y,x) (rename_edg edg l)).
inversion H5.
decompose [or] H8;exists (rank l 1 x0);
[left;apply eq_vert_aux2_l | right;apply eq_vert_aux2_r];assumption.
inversion H8.
assert (In (x,x0) (lto_edges (rename_edg edg l))
\/ In (x0,x) (lto_edges (rename_edg edg l))).
decompose [or]H9.
apply correct_lto_edges_aux2.
assumption.
assert (In (rename_vert_inv__aux (rename_fun l) x,rename_vert_inv__aux (rename_fun l) x0) edg).
apply in_rename_in;assumption.
unfold not;intro.
subst.
assert (rename_vert_inv__aux (rename_fun l) x0 < rename_vert_inv__aux (rename_fun l) x0).
eapply strict_in;eassumption.
intuition.
assert (In (x0,x) (lto_edges (rename_edg edg l))
\/ In (x,x0) (lto_edges (rename_edg edg l))).
apply correct_lto_edges_aux2.
assumption.
assert (In (rename_vert_inv__aux (rename_fun l) x0,rename_vert_inv__aux (rename_fun l) x) edg).
apply in_rename_in;assumption.
unfold not;intro.
subst.
assert (rename_vert_inv__aux (rename_fun l) x < rename_vert_inv__aux (rename_fun l) x).
eapply strict_in;eassumption.
intuition.
intuition.
decompose [or]H10.
apply (proj1 (in_vertices ((lto_edges (rename_edg edg l))) x x0 H11)).
apply (proj2 (in_vertices ((lto_edges (rename_edg edg l))) x0 x H11)).
assert (exists y : nat, In (x,y) (lto_edges (rename_edg edg l)) \/ In (y,x) (lto_edges (rename_edg edg l))).
apply in_edges_only;assumption.
assert (exists y : nat, In (x,y) (rename_edg edg l) \/ In (y,x) (rename_edg edg l)).
inversion H5;exists x0.
decompose [or] H6.
apply correct_lto_edges1;assumption.
assert (In (x0,x) (rename_edg edg l) \/ In (x,x0) (rename_edg edg l)).
apply correct_lto_edges1;assumption.
decompose [or] H7;intuition.
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
unfold rename_vert;rewrite rename_interv.
inversion H6;clear H5;clear H6.
decompose [or] H7;assert (0 < x /\x <= length l).
eapply in_rename_edg_l;eassumption.
apply only_in_interv_le;intuition.
eapply in_rename_edg_r;eassumption.
apply only_in_interv_le;intuition.
assumption.
Qed.
Lemma in_vert_in_rev_mypeo :
forall (x : nat),
In x (vertices my_graph)
-> In x (rev my_peo).
Proof.
intros.
eapply Permutation_in.
apply Permutation_rev.
assert (peo my_peo my_graph).
unfold my_peo;apply peo_peo_search;apply ax1.
inversion H0.
eapply Permutation_in.
eassumption.
assumption.
Qed.
Lemma peo_my_peo :
peo my_peo my_graph.
Proof.
unfold my_peo;apply peo_peo_search;apply ax1.
Qed.
Lemma NoDup_rev_mypeo :
NoDup (rev my_peo).
Proof.
assert (peo my_peo my_graph).
apply peo_my_peo.
apply (NoDup_perm nat my_peo (rev my_peo)).
apply Permutation_rev.
inversion H;apply (NoDup_perm nat (vertices my_graph) my_peo).
assumption.
apply strict_inc_NoDup;rewrite vertices_edges;apply is_strict_inc_vertices.
Qed.
Lemma strict_inc_rename_rev_my_peo_aux:
is_strict_inc (rename_vert_aux (nil ++ rev my_peo) (nil ++ rev my_peo)).
Proof.
apply strict_inc_rename.
apply NoDup_rev_mypeo.
constructor.
intros.
inversion H.
Qed.
Lemma strict_inc_rename_rev_my_peo :
is_strict_inc (rename_vert (rev my_peo)).
Proof.
unfold rename_vert.
replace (rev my_peo) with (nil ++ (rev my_peo)).
apply strict_inc_rename_rev_my_peo_aux.
intuition.
Qed.
Lemma eq_vert : my_chordal_gph_vert = rename_vert (rev my_peo).
Proof.
unfold my_chordal_gph_vert.
unfold my_chordal_gph_edg.
unfold new_edg.
rewrite <-my_peo_eq.
apply inc_perm_eq.
apply strict_inc_rename_rev_my_peo.
apply is_strict_inc_vertices.
apply NoDup_Permutation.
apply strict_inc_NoDup.
apply strict_inc_rename_rev_my_peo.
apply strict_inc_NoDup.
apply is_strict_inc_vertices.
intro;apply eq_vert_aux3.
apply NoDup_rev_mypeo.
intros.
split; apply in_vert_in_rev_mypeo;
rewrite vertices_edges;
destruct (in_vertices (edges my_graph) y z); assumption.
intros.
apply in_edges_only.
assert (peo my_peo my_graph).
apply peo_my_peo.
inversion H0.
rewrite vertices_edges in H1.
apply Permutation_sym in H1.
eapply Permutation_in. eassumption.
rewrite <- rev_involutive.
apply (proj1(In_rev(rev my_peo) y));assumption.
2: apply is_strict_ord_edges.
replace (rename_vert_aux (rev my_peo) (rev my_peo)) with
( (rename_vert (rev my_peo))).
apply strict_inc_rename_rev_my_peo.
unfold rename_vert.
reflexivity.
Qed.
Lemma peo_perm :
forall (l vert vert': list nat) (edg : list (nat*nat)),
_peo l vert edg
-> Permutation vert vert'
-> _peo l vert' edg.
Proof.
induction 1;intro.
constructor.
apply Permutation_trans with (l' := vert).
apply Permutation_sym;assumption.
assumption.
assumption.
Qed.
Lemma peo_to_peo_aux :
peo my_peo my_graph
-> _peo (rev my_chordal_gph_vert) my_chordal_gph_vert (new_edg).
Proof.
assert (peo my_peo my_graph).
unfold my_peo;apply peo_peo_search.
apply ax1.
unfold peo;unfold new_edg;rewrite eq_vert;
rewrite <-my_peo_eq;unfold rename_vert;intros.
rewrite <-rename_semi_rev_l.
rewrite rev_involutive.
apply peo_renaming2.
eapply peo_perm.
unfold peo in H.
eexact H.
inversion H.
apply Permutation_trans with (l' := my_peo).
assumption.
apply Permutation_rev.
apply (NoDup_perm nat (rev (vertices my_graph))).
inversion H.
apply Permutation_trans with (l' := my_peo).
apply Permutation_trans with (l' := vertices my_graph).
apply Permutation_sym;apply Permutation_rev.
assumption.
apply Permutation_rev.
eapply NoDup_perm.
apply Permutation_rev.
apply strict_inc_NoDup.
rewrite vertices_edges;apply is_strict_inc_vertices.
intros.
assert (In a (vertices my_graph) /\ In b (vertices my_graph)).
rewrite vertices_edges;apply in_vertices;assumption.
split;eapply Permutation_in.
apply Permutation_rev.
eapply Permutation_in.
inversion H.
eassumption.
intuition.
apply Permutation_rev.
eapply Permutation_in.
inversion H.
eassumption.
intuition.
eapply NoDup_perm.
apply Permutation_rev.
eapply NoDup_perm.
inversion H;eassumption.
apply strict_inc_NoDup;rewrite vertices_edges;apply is_strict_inc_vertices.
Qed.
Lemma peo_lto_edges :
forall (l vert : list nat) (edg : list (nat*nat)),
_peo l vert edg
-> _peo l vert (lto_edges edg).
Proof.
induction 1.
constructor.
assumption.
intros.
constructor.
intuition.
intros.
assert (sv x (x :: rl) edg).
eapply H0;eassumption.
inversion H9.
assert (In (y,z) edg \/ In (z,y) edg).
apply H11.
assumption.
assumption.
assumption.
assumption.
assumption.
decompose [or] H7.
apply correct_lto_edges1;assumption.
assert (In (y,x) edg \/ In (x,y) edg).
apply correct_lto_edges1;assumption.
intuition.
decompose [or] H8.
apply correct_lto_edges1;assumption.
assert (In (z,x) edg \/ In (x,z) edg).
apply correct_lto_edges1;assumption.
intuition.
decompose [or] H15.
apply correct_lto_edges_aux2;assumption.
assert (In (z,y) (lto_edges edg) \/ In (y,z) (lto_edges edg)).
apply correct_lto_edges_aux2;intuition.
intuition.
Qed.
Lemma peo_to_peo :
peo (my_peo) my_graph
-> peo (rev (rename_vert (rev my_peo))) my_chordal_gph.
Proof.
rewrite <-eq_vert.
unfold peo;intros.
assert (_peo (rev my_chordal_gph_vert) (rev (vertices my_chordal_gph))
(edges my_chordal_gph)).
assert (edges my_chordal_gph = my_chordal_gph_edg).
intuition.
rewrite H0.
unfold my_chordal_gph_edg.
apply peo_lto_edges.
assert (vertices my_chordal_gph = my_chordal_gph_vert).
intuition.
rewrite H1.
eapply peo_perm.
apply peo_to_peo_aux.
unfold peo;assumption.
apply Permutation_rev.
eapply peo_perm.
eassumption.
apply Permutation_sym;apply Permutation_rev.
Qed.
Lemma peo_vertices :
forall (x : nat),
In x (my_chordal_gph_vert)
-> is_clique
my_chordal_gph
(x :: get_nghbs my_chordal_gph x)
(length (get_nghbs my_chordal_gph x) + 1).
Proof.
intros;apply peo_clique.
assert (vertices my_chordal_gph = my_chordal_gph_vert).
intuition.
rewrite H0.
rewrite eq_vert in *.
apply peo_to_peo.
unfold my_peo;apply peo_peo_search.
apply ax1.
assumption.
Qed.
Definition my_chordal_graph : chordal_graph :=
Chordal_graph
my_chordal_gph
peo_vertices.