Library peo_search
Require Import List.
Require Import ZArith.
Require Import lex_sort.
Require Import strict_ord.
Require Import strict_inc_and_dec.
Require Import graph_construction.
Require Import Recdef.
Require Import quicksort.
Require Import nat_quicksort.
Fixpoint sv_nghbs_aux (l : list (nat*nat)) (x : nat) {struct l} : list nat :=
match l with
| nil => nil
| (a,b) :: l' => match (eq_nat_dec x a) with
| left _ => b :: sv_nghbs_aux l' x
| right _ => match (eq_nat_dec x b) with
| left _ => a :: sv_nghbs_aux l' x
| right _ => sv_nghbs_aux l' x
end
end
end.
Definition sv_nghbs (g : graph) (x : nat) : list nat :=
sv_nghbs_aux (edges g) x.
Fixpoint is_clique_b_aux (x : nat) (l : list nat) (l' : list (nat*nat)) {struct l'}: (bool*(list (nat*nat))) :=
match l with
| nil => (true,l')
| a :: l0 => match l' with
| nil => (false,nil)
| (y,z) :: l'' => match (gt_eq_gt_dec x y) with
| inleft (left _) => (false,nil)
| inleft (right _) => match (gt_eq_gt_dec a z) with
| inleft (left _) => (false,nil)
| inleft (right _) => is_clique_b_aux x l0 l''
| inright _ => is_clique_b_aux x l l''
end
| inright _ => is_clique_b_aux x l l''
end
end
end.
Fixpoint is_clique_b (l : list nat) (l' : list (nat*nat)) {struct l}: bool :=
match l with
| nil => true
| x :: l'' => match fst (is_clique_b_aux x l'' l') with
| true => is_clique_b l'' (snd (is_clique_b_aux x l'' l'))
| false => false
end
end.
Definition is_sv (x : nat) (l' : list (nat*nat)) : bool :=
is_clique_b (sv_nghbs_aux l' x) l'.
Fixpoint sv_search_aux (l : list nat) (l' : list (nat*nat)) {struct l}: nat :=
match l with
| nil => 0
| x :: l'' => match l'' with
| nil => x
| _ :: l''' => match (is_sv x l') with
| true => x
| false => sv_search_aux l'' l'
end
end
end.
Definition sv_search (g : graph) :=
sv_search_aux (vertices g) (edges g).
Fixpoint rm (x : nat) (l : list (nat*nat)) {struct l} : list (nat*nat) :=
match l with
| nil => nil
| (y,z) :: l' => match (eq_nat_dec x y) with
| left _ => rm x l'
| right _ => match (eq_nat_dec x z) with
| left _ => rm x l'
| right _ => (y,z) :: rm x l'
end
end
end.
Lemma in_sv_nghbs_tail:
forall (edg : list (nat*nat)) (x y z : nat),
NoDup ((x,y) :: edg)
-> is_strict_ord ((x,y) :: edg)
-> is_lex_sorted ((x,y) :: edg)
-> In z (sv_nghbs_aux edg x)
-> y < z.
Proof.
induction edg;intros.
simpl in H2;intuition.
destruct a;simpl in H2.
destruct (eq_nat_dec x n).
subst.
simpl in H2;decompose [or]H2.
subst.
assert (n < n \/ (n = n /\ (y <= z))).
eapply strict_sort_in.
eassumption.
intuition.
decompose [or]H3.
intuition.
assert (y <> z).
unfold not;intro;subst.
inversion H;intuition.
intuition.
apply (IHedg n y z).
constructor.
inversion H;intuition.
inversion H;inversion H7;assumption.
constructor.
inversion H0;assumption.
inversion H0;inversion H8;assumption.
eapply is_lex_sorted_rmsnd;eassumption.
assumption.
destruct (eq_nat_dec x n0).
subst;inversion H1.
subst;inversion H5.
simpl in H4;inversion H0;inversion H12;
apply False_ind;subst;intuition.
simpl in H3;inversion H0;inversion H11;
subst;apply False_ind;intuition.
intuition.
apply (IHedg x y z).
constructor.
inversion H;intuition.
inversion H;inversion H6;assumption.
constructor.
inversion H0;assumption.
inversion H0;inversion H7;assumption.
eapply is_lex_sorted_rmsnd;eassumption.
assumption.
Qed.
Lemma in_sv_nghbs_le :
forall (edg : list (nat*nat)) (x y z : nat),
is_lex_sorted ((x,y) :: edg)
-> NoDup ((x,y) :: edg)
-> is_strict_ord ((x,y) :: edg)
-> In z (sv_nghbs_aux edg y)
-> x < z.
Proof.
induction edg;intros.
simpl in H2;inversion H2.
destruct a;simpl in H2.
destruct (eq_nat_dec y n).
subst.
simpl in H2;decompose [or] H2.
subst.
inversion H1;inversion H7;intuition.
apply (IHedg x n z).
eapply is_lex_sorted_rmsnd;eassumption.
constructor.
inversion H0;intuition.
inversion H0;inversion H7;assumption.
constructor.
inversion H1;assumption.
inversion H1;inversion H8;assumption.
assumption.
destruct (eq_nat_dec y n0).
subst.
simpl in H2;decompose [or]H2.
subst.
assert (x < z \/ (x = z /\ n0 <= n0)).
eapply strict_sort_in.
eassumption.
intuition.
decompose [or] H3.
assumption.
decompose [and]H4.
subst.
apply False_ind;inversion H0;intuition.
apply (IHedg x n0 z).
eapply is_lex_sorted_rmsnd;eassumption.
constructor.
inversion H0;intuition.
inversion H0;inversion H7;assumption.
constructor.
inversion H1;assumption.
inversion H1;inversion H8;assumption.
assumption.
apply (IHedg x y z).
eapply is_lex_sorted_rmsnd;eassumption.
constructor.
inversion H0;intuition.
inversion H0;inversion H6;assumption.
constructor.
inversion H1;assumption.
inversion H1;inversion H7;assumption.
assumption.
Qed.
Lemma strict_inc_sv_nghbs :
forall (edg : list (nat*nat)) (x : nat),
is_lex_sorted edg
-> is_strict_ord edg
-> NoDup edg
-> is_strict_inc (sv_nghbs_aux edg x).
Proof.
induction edg;intros.
simpl.
constructor.
destruct a;simpl.
destruct (eq_nat_dec x n).
subst.
apply strict_inc_add_hd.
apply IHedg.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
inversion H1;assumption.
intros;eapply in_sv_nghbs_tail;eassumption.
destruct (eq_nat_dec x n0).
subst.
apply strict_inc_add_hd.
apply IHedg.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
inversion H1;assumption.
intros.
apply (in_sv_nghbs_le edg n n0 y);assumption.
apply IHedg.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
inversion H1;assumption.
Qed.
Lemma in_sv_search_aux :
forall (l : list nat) (l' : list (nat*nat)),
l <> nil
-> In (sv_search_aux l l') l.
Proof.
induction l;intros.
intuition.
simpl.
destruct l.
intuition.
destruct (is_sv a).
intuition.
right;apply IHl.
discriminate.
Qed.
Lemma remove_lth :
forall (l : list nat) (x : nat),
length (remove eq_nat_dec x l) <= length l.
Proof.
induction l;simpl;intros.
intuition.
destruct (eq_nat_dec x a).
apply le_S.
apply IHl.
simpl.
apply le_n_S.
apply IHl.
Qed.
Lemma in_remove_lth :
forall (l : list nat) (x : nat),
In x l
-> length (remove eq_nat_dec x l) < length l.
Proof.
induction l;simpl;intros.
inversion H.
destruct (eq_nat_dec x a).
apply le_lt_n_Sm.
apply remove_lth.
decompose [or] H.
intuition.
simpl;apply lt_n_S;apply IHl;assumption.
Qed.
Function peo_search_aux (l : list nat) (l' : list (nat*nat)) {measure length l}: list nat :=
match l with
| nil => nil
| _ => (sv_search_aux l l') :: peo_search_aux (remove eq_nat_dec (sv_search_aux l l') l)
(rm (sv_search_aux l l') l')
end.
Proof.
intros;apply in_remove_lth;apply in_sv_search_aux;discriminate.
Qed.
Fixpoint is_peo (l : list nat) (edg : list (nat*nat)) {struct l} : bool :=
match l with
nil => true
|x :: l' => match (is_sv x edg) with
| true => is_peo l' (rm x edg)
| false => false
end
end.
Definition peo_search (g : graph) : list nat :=
peo_search_aux (vertices g) (edges g).
Lemma remove_not_in :
forall (l : list nat) (x : nat),
~In x l
-> remove eq_nat_dec x l = l.
Proof.
induction l;simpl;intros.
reflexivity.
destruct (eq_nat_dec x a).
apply False_ind;intuition.
rewrite IHl.
reflexivity.
intuition.
Qed.
Lemma in_sv_nghbs_aux :
forall (edg : list (nat*nat)) (x y : nat),
In x (sv_nghbs_aux edg y)
-> In (x,y) edg \/ In (y,x) edg.
Proof.
induction edg;intros.
inversion H.
destruct a;simpl in H.
destruct (eq_nat_dec y n).
simpl in H;decompose [or] H.
subst.
right;intuition.
assert (In (x,y) edg \/ In (y,x) edg).
apply IHedg;assumption.
intuition.
destruct (eq_nat_dec y n0).
subst.
simpl in H;decompose [or] H.
subst.
left;intuition.
assert (In (x,n0) edg \/ In (n0,x) edg).
apply IHedg;assumption.
intuition.
assert (In (x,y) edg \/ In (y,x) edg).
apply IHedg;assumption.
intuition.
Qed.
Lemma sv_nghbs_add :
forall (edg : list (nat*nat)) (x y : nat),
sv_nghbs_aux ((x,y) :: edg) x = y :: sv_nghbs_aux edg x.
Proof.
induction edg;intros.
simpl.
destruct (eq_nat_dec x x).
reflexivity.
intuition.
simpl.
destruct (eq_nat_dec x x).
destruct a.
destruct (eq_nat_dec x n).
reflexivity.
destruct (eq_nat_dec x n0).
reflexivity.
reflexivity.
intuition.
Qed.
Lemma clique_true :
forall (l : list nat) (edg : list (nat*nat)) (x : nat),
fst(is_clique_b_aux x l edg) = true
-> (forall (y : nat),
In y l
-> In (x,y) edg).
Proof.
induction l;intros.
inversion H0.
induction edg;simpl in H.
inversion H;apply False_ind;intuition.
destruct a0.
destruct (gt_eq_gt_dec x n).
destruct s.
apply False_ind;simpl in H;intuition.
destruct (gt_eq_gt_dec a n0).
destruct s.
simpl in H;apply False_ind;intuition.
subst.
simpl in H0;decompose [or]H0.
subst;intuition.
simpl;right;apply (IHl edg n);assumption.
simpl;right;apply IHedg;assumption.
simpl;right;apply IHedg;assumption.
Qed.
Lemma clique_snd_in :
forall (l : list nat) (edg : list (nat*nat)) (y z x : nat),
In (y,z) (snd (is_clique_b_aux x l edg))
-> In (y,z) edg.
Proof.
induction l;intros.
destruct edg;assumption.
induction edg.
assumption.
simpl in H.
destruct a0.
destruct (gt_eq_gt_dec x n).
destruct s.
apply False_ind;simpl in H;intuition.
destruct (gt_eq_gt_dec a n0).
destruct s.
simpl in H;intuition.
subst.
simpl;right;eapply IHl;eassumption.
subst.
simpl;right;apply IHedg;assumption.
right;intuition.
Qed.
Lemma clique_in :
forall (l : list nat) (edg : list (nat*nat)) (x y : nat),
In x l
-> In y l
-> x <> y
-> is_clique_b l edg = true
-> In (x,y) edg \/ In (y,x) edg.
Proof.
induction l;intros.
inversion H.
simpl in H;decompose [or]H.
subst.
simpl in H2.
assert (fst (is_clique_b_aux x l edg) = true \/ fst (is_clique_b_aux x l edg) = false).
destruct (fst (is_clique_b_aux x l edg));intuition.
decompose [or]H3.
assert (exists l' : list (nat*nat), is_clique_b_aux x l edg = (true,l')).
destruct (is_clique_b_aux x l edg).
simpl in H4.
exists l0;rewrite H4;reflexivity.
inversion H5.
left;apply (clique_true l edg x).
assumption.
simpl in H0;decompose [or]H0;intuition.
rewrite H4 in H2.
inversion H2.
simpl in H0;decompose [or]H0.
subst.
simpl in H2.
assert (fst (is_clique_b_aux y l edg) = true \/ fst (is_clique_b_aux y l edg) = false).
destruct (fst (is_clique_b_aux y l edg));intuition.
decompose [or]H4.
assert (exists l' : list (nat*nat), is_clique_b_aux y l edg = (true,l')).
destruct (is_clique_b_aux y l edg).
simpl in H5.
exists l0;rewrite H5;reflexivity.
inversion H6.
right;apply (clique_true l edg y);assumption.
rewrite H5 in H2.
inversion H2.
simpl in H2.
assert (fst (is_clique_b_aux a l edg) = true \/ fst (is_clique_b_aux a l edg) = false).
destruct (fst (is_clique_b_aux a l edg));intuition.
decompose [or]H5.
rewrite H6 in H2.
assert (In (x,y) (snd (is_clique_b_aux a l edg)) \/ In (y,x) (snd (is_clique_b_aux a l edg))).
apply IHl;assumption.
decompose [or]H7;[left|right];eapply clique_snd_in;eassumption.
rewrite H6 in H2.
inversion H2.
Qed.
Lemma in_sv_nghbs :
forall (edg : list (nat*nat)) (x y : nat),
In (x,y) edg \/ In (y,x) edg
-> In y (sv_nghbs_aux edg x).
Proof.
induction edg;[|destruct a];simpl;intros.
intuition.
destruct (eq_nat_dec x n).
subst.
decompose [or] H.
inversion H1;intuition.
simpl;right;apply IHedg;intuition.
inversion H1;intuition.
simpl;right;apply IHedg;intuition.
destruct (eq_nat_dec x n0).
decompose [or] H.
inversion H1;apply False_ind;intuition.
simpl;right;apply IHedg;intuition.
inversion H1;intuition.
simpl;right;apply IHedg;intuition.
decompose [or] H.
inversion H1;apply False_ind;intuition.
apply IHedg;intuition.
inversion H1;apply False_ind;intuition.
apply IHedg;intuition.
Qed.
Lemma sv_nghbs_swap :
forall (edg : list (nat*nat)) (x y z : nat),
sv_nghbs_aux ((x,y) :: edg) z
=
sv_nghbs_aux ((y,x) :: edg) z.
Proof.
intros;simpl.
destruct (eq_nat_dec z x).
subst.
destruct (eq_nat_dec x y);subst;reflexivity.
reflexivity.
Qed.
Lemma sv_clique :
forall (edg : list (nat*nat)) (x : nat),
is_sv x edg = true
-> (forall (y z : nat),
x <> y
-> x <> z
-> y <> z
-> In (x,y) edg \/ In (y,x) edg
-> In (x,z) edg \/ In (z,x) edg
-> In (y,z) edg \/ In (z,y) edg).
Proof.
unfold is_sv;destruct edg;intros.
inversion H3;inversion H5.
simpl in H.
destruct p.
destruct (eq_nat_dec x n).
subst.
rewrite <-sv_nghbs_add in H.
apply (clique_in (sv_nghbs_aux ((n,n0) :: edg) n) ((n,n0) :: edg) y z).
apply in_sv_nghbs;assumption.
apply in_sv_nghbs;assumption.
assumption.
assumption.
destruct (eq_nat_dec x n0).
subst.
rewrite <- sv_nghbs_add in H.
rewrite <- sv_nghbs_swap in H.
apply (clique_in (sv_nghbs_aux ((n,n0) :: edg) n0) ((n,n0) :: edg)).
apply in_sv_nghbs;assumption.
apply in_sv_nghbs;assumption.
assumption.
assumption.
apply (clique_in (sv_nghbs_aux edg x) ((n,n0) :: edg)).
apply in_sv_nghbs.
decompose [or] H3.
simpl in H5;decompose [or]H5.
inversion H6;apply False_ind;intuition.
intuition.
simpl in H5;decompose [or]H5.
inversion H6;apply False_ind;intuition.
intuition.
apply in_sv_nghbs.
decompose [or] H4.
simpl in H5;decompose [or]H5.
inversion H6;apply False_ind;intuition.
intuition.
simpl in H5;decompose [or]H5.
inversion H6;apply False_ind;intuition.
intuition.
assumption.
assumption.
Qed.
Lemma is_clique_b_aux_true :
forall (edg : list (nat*nat)) (l : list nat) (x : nat),
is_lex_sorted edg
-> is_strict_ord edg
-> is_strict_inc l
->
(forall (y : nat),
In y l
-> In (x,y) edg)
-> fst(is_clique_b_aux x l edg) = true.
Proof.
induction edg;intros.
destruct l.
simpl;reflexivity.
assert (In (x,n) nil).
apply H2;intuition.
inversion H3.
simpl.
destruct l.
reflexivity.
destruct a.
destruct (gt_eq_gt_dec x n0).
destruct s.
assert (n0 < x \/ (n0 = x /\ n1 <= n)).
eapply strict_sort_in.
eassumption.
assert (In (x,n) ((n0,n1) :: edg)).
apply H2;intuition.
simpl in H3;decompose [or] H3.
inversion H4;apply False_ind;intuition.
assumption.
decompose [or] H3;apply False_ind;intuition.
subst.
destruct (gt_eq_gt_dec n n1).
destruct s.
assert (n0 < n0 \/ (n0 = n0 /\ n1 <= n)).
eapply strict_sort_in.
eassumption.
assert (In (n0,n) ((n0,n1) :: edg)).
apply H2;intuition.
simpl in H3;decompose [or] H3.
inversion H4;apply False_ind;intuition.
assumption.
intuition.
subst.
apply IHedg.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
eapply is_strict_inc_tail;eassumption.
intros.
assert (In (n0,y) ((n0,n1) :: edg)).
apply H2;intuition.
simpl in H4;decompose [or] H4.
inversion H5.
assert (n1 < y).
eapply in_strict_sort;eassumption.
apply False_ind;intuition.
assumption.
apply IHedg.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
assumption.
intros.
assert (In (n0,y) ((n0,n1) :: edg)).
apply H2;assumption.
simpl in H4;decompose [or] H4.
assert (n <= y).
simpl in H3;decompose [or] H3.
intuition.
assert (n < y).
eapply in_strict_sort;eassumption.
intuition.
inversion H5;apply False_ind;intuition.
assumption.
apply IHedg.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
assumption.
intros.
assert (In (x,y) ((n0,n1) :: edg)).
apply H2;assumption.
simpl in H4;decompose [or] H4.
inversion H5;apply False_ind;intuition.
assumption.
Qed.
Lemma lex_sort_clique_b_aux :
forall (edg : list (nat*nat)) (l : list nat) (x : nat),
is_lex_sorted edg
-> is_lex_sorted (snd (is_clique_b_aux x l edg)).
Proof.
induction edg;intros;simpl;destruct l;try assumption.
destruct a.
destruct (gt_eq_gt_dec x n0).
destruct s.
simpl;unfold is_lex_sorted;constructor.
destruct (gt_eq_gt_dec n n1).
destruct s.
simpl;unfold is_lex_sorted;constructor.
apply IHedg;eapply is_lex_sorted_tail;eassumption.
apply IHedg;eapply is_lex_sorted_tail;eassumption.
apply IHedg;eapply is_lex_sorted_tail;eassumption.
Qed.
Lemma strict_ord_clique_b_aux :
forall (edg : list (nat*nat)) (l : list nat) (x : nat),
is_strict_ord edg
-> is_strict_ord (snd (is_clique_b_aux x l edg)).
Proof.
induction edg;intros.
simpl;destruct l;assumption.
simpl.
destruct l;destruct a.
assumption.
destruct (gt_eq_gt_dec x n0).
destruct s.
constructor.
destruct (gt_eq_gt_dec n n1).
destruct s.
constructor.
apply IHedg;inversion H;assumption.
apply IHedg;inversion H;assumption.
apply IHedg;inversion H;assumption.
Qed.
Lemma snd_is_clique_b_aux_prop :
forall (edg : list (nat*nat)) (l : list nat) (x : nat),
exists l' : list (nat*nat),
l' ++ snd (is_clique_b_aux x l edg) = edg
/\
(fst (is_clique_b_aux x l edg) = true
->
(forall (y z : nat),
In (y,z) l'
-> y <= x)).
Proof.
induction edg;intros.
exists (@nil (nat*nat)).
destruct l;simpl;intuition.
simpl.
destruct l.
exists (@nil (nat*nat)).
split.
reflexivity.
intros.
inversion H0.
destruct a.
destruct (gt_eq_gt_dec x n0).
destruct s.
exists ((n0,n1) :: edg).
split.
simpl.
rewrite app_nil_end;reflexivity.
intro;inversion H.
destruct (gt_eq_gt_dec n n1).
destruct s.
exists ((n0,n1) :: edg).
split.
rewrite app_nil_end;reflexivity.
intro;inversion H.
assert (exists l'' : list (nat*nat),l''++ snd (is_clique_b_aux x l edg) = edg
/\ (fst (is_clique_b_aux x l edg) = true
-> forall y z : nat, In (y,z) l'' -> y <= x)).
apply IHedg.
inversion H.
exists ((n0,n1) :: x0).
simpl.
split.
rewrite (proj1 H0);reflexivity.
intros.
decompose [or] H2.
inversion H3.
intuition.
eapply ((proj2 (H0)) H1);eassumption.
assert (exists l'' : list (nat*nat),l''++ snd (is_clique_b_aux x (n :: l) edg) = edg
/\ (fst (is_clique_b_aux x (n :: l) edg) = true
-> forall y z : nat, In (y,z) l'' -> y <= x)).
apply IHedg.
inversion H.
exists ((n0,n1) :: x0).
simpl.
split.
rewrite (proj1 H0);reflexivity.
intros.
decompose [or] H2.
inversion H3.
intuition.
eapply ((proj2 (H0)) H1);eassumption.
assert (exists l'' : list (nat*nat),l''++ snd (is_clique_b_aux x (n :: l) edg) = edg
/\ (fst (is_clique_b_aux x (n :: l) edg) = true
-> forall y z : nat, In (y,z) l'' -> y <= x)).
apply IHedg.
inversion H.
exists ((n0,n1) :: x0).
simpl.
split.
rewrite (proj1 H0);reflexivity.
intros.
decompose [or] H2.
inversion H3.
intuition.
eapply ((proj2 (H0)) H1);eassumption.
Qed.
Lemma in_snd_is_clique_b_aux :
forall (edg : list (nat*nat)) (l : list nat) (a x y : nat),
is_strict_inc (a :: l)
-> is_lex_sorted edg
-> is_strict_ord edg
-> In x l
-> In y l
-> x < y
-> In (x,y) edg
-> fst (is_clique_b_aux a l edg) = true
-> In (x,y) (snd (is_clique_b_aux a l edg)).
Proof.
induction edg;intros.
inversion H5.
simpl in *.
destruct l.
inversion H2.
destruct a.
destruct (gt_eq_gt_dec a0 n0).
destruct s.
inversion H6.
destruct (gt_eq_gt_dec n n1).
destruct s.
inversion H6.
subst.
assert (exists l' : list (nat*nat),
l' ++ snd (is_clique_b_aux n0 l edg) = edg
/\ (fst (is_clique_b_aux n0 l edg) = true
-> forall y z : nat,
In (y,z) l'
-> y <= n0)).
apply snd_is_clique_b_aux_prop.
destruct H7.
decompose [and] H7.
assert (In (x,y) x0 \/ In (x,y) (snd (is_clique_b_aux n0 l edg))).
apply in_app_or;rewrite H8.
decompose [or] H5.
assert (n1 <= x).
simpl in H2;decompose [or] H2.
intuition.
assert (n1 < x).
eapply in_strict_sort;inversion H;eassumption.
intuition.
apply False_ind;inversion H10;inversion H1;intuition.
assumption.
decompose [or] H10.
assert (x <= n0).
eapply H9;eassumption.
assert (n1 <= x).
simpl in H2;decompose [or] H2.
intuition.
assert (n1 < x).
eapply in_strict_sort.
inversion H;eassumption.
assumption.
intuition.
apply False_ind;inversion H;intuition.
assumption.
apply IHedg.
assumption.
eapply is_lex_sorted_tail;eassumption.
inversion H1;assumption.
assumption.
assumption.
assumption.
decompose [or] H5.
inversion H7;subst.
assert (n <= y).
simpl in H3;decompose [or] H3.
intuition.
assert (n < y).
eapply in_strict_sort.
inversion H;eassumption.
assumption.
intuition.
apply False_ind;intuition.
assumption.
assumption.
apply IHedg.
assumption.
eapply is_lex_sorted_tail;eassumption.
inversion H1;assumption.
assumption.
assumption.
assumption.
decompose [or] H5.
inversion H7;subst.
assert (n <= x).
simpl in H2;decompose [or] H2.
intuition.
assert (n < x).
eapply in_strict_sort.
inversion H;eassumption.
assumption.
intuition.
apply False_ind;inversion H;intuition.
assumption.
assumption.
Qed.
Lemma clique_in_inv :
forall (l : list nat) (edg : list (nat*nat)),
is_lex_sorted edg
-> is_strict_ord edg
-> is_strict_inc l
-> (forall (x y : nat),
In x l
-> In y l
-> x < y
-> In (x,y) edg)
-> is_clique_b l edg = true.
Proof.
induction l;intros.
reflexivity.
simpl.
assert (fst (is_clique_b_aux a l edg) = true).
apply is_clique_b_aux_true.
assumption.
assumption.
eapply is_strict_inc_tail;eassumption.
intros;apply H2;intuition.
eapply in_strict_sort;eassumption.
rewrite H3.
apply IHl.
apply lex_sort_clique_b_aux;assumption.
apply strict_ord_clique_b_aux;assumption.
eapply is_strict_inc_tail;eassumption.
intros;apply in_snd_is_clique_b_aux.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
apply H2;intuition.
assumption.
Qed.
Lemma clique_construct :
forall (edg : list (nat*nat)) (l : list nat) (x : nat),
is_strict_ord edg
-> is_lex_sorted edg
-> is_strict_inc (x :: l)
-> is_clique_b l edg = true
-> fst (is_clique_b_aux x l edg) = true
-> is_clique_b (x :: l) edg = true.
Proof.
intros.
simpl;rewrite H3.
apply clique_in_inv.
apply lex_sort_clique_b_aux;assumption.
apply strict_ord_clique_b_aux;assumption.
eapply is_strict_inc_tail;eassumption.
intros;apply in_snd_is_clique_b_aux.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
assert (In (x0,y) edg \/ In (y,x0) edg).
eapply clique_in.
eassumption.
eassumption.
intuition.
assumption.
decompose [or] H7.
assumption.
assert (y < x0).
eapply strict_in;eassumption.
apply False_ind;intuition.
assumption.
Qed.
Lemma clique_aux :
forall (edg : list (nat*nat)) (l : list nat) (x : nat),
is_lex_sorted edg
-> is_strict_ord edg
-> is_strict_inc (x :: l)
-> (forall (y z : nat),
In y (x :: l)
-> In z (x :: l)
-> y <> z
-> In (y,z) edg \/ In (z,y) edg)
-> fst (is_clique_b_aux x l edg) = true.
Proof.
induction edg;intros.
simpl.
destruct l.
reflexivity.
assert (In (x,n) nil \/ In (n,x) nil).
apply H2.
intuition.
intuition.
inversion H1;intuition.
inversion H3;inversion H4.
simpl.
destruct l.
simpl;reflexivity.
destruct a.
destruct (gt_eq_gt_dec x n0).
destruct s.
assert (In (x,n) ((n0,n1) :: edg) \/ In (n,x) ((n0,n1) :: edg)).
apply H2.
intuition.
intuition.
inversion H1;intuition.
decompose [or]H3.
assert (n0 < x \/ (n0 = x /\ n1 <= n)).
apply (strict_sort_in edg x n n0 n1).
assumption.
simpl in H4;decompose [or]H4.
inversion H5;apply False_ind;intuition.
assumption.
decompose [or] H5;apply False_ind;intuition.
assert (n < x).
eapply strict_in;eassumption.
inversion H1;apply False_ind;intuition.
subst.
destruct (gt_eq_gt_dec n n1).
destruct s.
assert (In (n0,n) ((n0,n1) :: edg)).
assert (In (n0,n) ((n0,n1) :: edg) \/ In (n,n0) ((n0,n1) :: edg)).
apply H2.
intuition.
intuition.
inversion H1;intuition.
decompose [or]H3.
assumption.
assert (n < n0).
eapply strict_in;eassumption.
inversion H1;apply False_ind;intuition.
assert (n0 < n0 \/ (n0 = n0 /\ n1 <= n)).
apply (strict_sort_in edg n0 n n0 n1).
assumption.
simpl in H3;decompose [or]H3.
inversion H4;apply False_ind;intuition.
assumption.
decompose [or]H4;intuition.
subst.
apply IHedg.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
eapply is_strict_inc_rmsnd;eassumption.
intros.
assert (~In n1 (n0 :: l)).
unfold not;intro.
assert (NoDup (n0 :: n1 :: l)).
apply strict_inc_NoDup;assumption.
inversion H7.
destruct (eq_nat_dec n0 n1).
inversion H1;intuition.
inversion H11.
simpl in H6;decompose [or]H6.
intuition.
intuition.
assert (In (y,z) ((n0,n1) :: edg) \/ In (z,y) ((n0,n1) :: edg)).
apply H2.
simpl in H3;decompose [or]H3.
subst;intuition.
intuition.
simpl in H4;decompose [or]H4.
subst;intuition.
intuition.
assumption.
decompose [or]H7.
left.
simpl in H8;decompose [or]H8.
inversion H9;subst.
apply False_ind;intuition.
assumption.
right.
simpl in H8;decompose [or]H8.
inversion H9;subst.
apply False_ind;intuition.
assumption.
apply IHedg.
eapply is_lex_sorted_tail;eassumption.
inversion H0;assumption.
assumption.
intros.
assert (~In n1 (n0 :: n :: l)).
unfold not;intro.
simpl in H6;decompose [or]H6.
inversion H0;intuition.
intuition.
assert (n < n1).
eapply in_strict_sort.
inversion H1;eassumption.
assumption.
intuition.
assert (In (y,z) ((n0,n1) :: edg) \/ In (z,y) ((n0,n1) :: edg)).
apply H2;assumption.
decompose [or]H7.
left.
simpl in H8;decompose [or]H8.
inversion H9.
subst.
apply False_ind;intuition.
assumption.
simpl in H8;decompose [or]H8.
inversion H9.
subst.
apply False_ind;intuition.
intuition.
apply IHedg.
eapply is_lex_sorted_tail;eassumption.
inversion H0;intuition.
assumption.
intros.
assert (In (y,z) ((n0,n1) :: edg) \/ In (z,y) ((n0,n1) :: edg)).
apply H2;assumption.
decompose [or] H6.
left.
simpl in H7;decompose [or]H7.
inversion H8.
subst.
assert (x < y).
eapply in_strict_sort.
eassumption.
simpl in H3;decompose [or]H3.
subst.
apply False_ind;intuition.
subst;intuition.
intuition.
apply False_ind;intuition.
assumption.
simpl in H7;decompose [or]H7.
inversion H8;subst.
assert (x < z).
eapply in_strict_sort.
eassumption.
simpl in H4;decompose [or]H4.
subst.
apply False_ind;intuition.
subst;intuition.
intuition.
apply False_ind;intuition.
intuition.
Qed.
Lemma clique_sv_aux :
forall (edg : list (nat*nat)) (l : list nat),
is_lex_sorted edg
-> is_strict_ord edg
-> is_strict_inc l
-> (forall (y z : nat),
In y l
-> In z l
-> y <> z
-> In (y,z) edg \/ In (z,y) edg)
-> is_clique_b l edg = true.
Proof.
induction l;intros.
simpl;reflexivity.
apply clique_construct.
assumption.
assumption.
assumption.
apply IHl.
assumption.
assumption.
eapply is_strict_inc_tail;eassumption.
intuition.
apply clique_aux;assumption.
Qed.
Lemma clique_sv :
forall (edg : list (nat*nat)) (x : nat),
(forall (y z : nat),
x <> y
-> x <> z
-> y <> z
-> In (x,y) edg \/ In (y,x) edg
-> In (x,z) edg \/ In (z,x) edg
-> In (y,z) edg \/ In (z,y) edg)
-> is_lex_sorted edg
-> is_strict_ord edg
-> NoDup edg
-> is_sv x edg = true.
Proof.
intros;unfold is_sv;apply clique_sv_aux.
assumption.
assumption.
apply strict_inc_sv_nghbs;assumption.
intros.
assert (In (y,x) edg \/ In (x,y) edg).
apply in_sv_nghbs_aux;assumption.
assert (In (z,x) edg \/ In (x,z) edg).
apply in_sv_nghbs_aux;assumption.
apply H.
decompose [or] H6.
assert (y < x).
eapply strict_in;eassumption.
intuition.
assert (x < y).
eapply strict_in;eassumption.
intuition.
decompose [or] H7.
assert (z < x).
eapply strict_in;eassumption.
intuition.
assert (x < z).
eapply strict_in;eassumption.
intuition.
assumption.
intuition.
intuition.
Qed.
Lemma sv_simplicial_vertex_aux :
forall (vert : list nat) (edg : list (nat*nat)) (x : nat),
is_sv x edg = true
-> In x vert
-> sv x vert edg.
Proof.
induction vert;intros.
inversion H0.
constructor.
assumption.
intros.
apply (sv_clique edg x);assumption.
Qed.
Lemma sv_simplicial_vertex_aux2 :
forall (vert : list nat) (edg : list (nat*nat)) (x : nat),
sv x vert edg
-> (forall (x y : nat),
In (x,y) edg
-> In x vert /\ In y vert)
-> is_lex_sorted edg
-> is_strict_ord edg
-> NoDup edg
-> is_sv x edg = true.
Proof.
induction vert;intros.
destruct edg;inversion H;inversion H4.
apply clique_sv.
intros;inversion H.
apply H10.
assumption.
assumption.
assumption.
decompose [or] H7.
apply (proj2 ((H0 x y) H14)).
apply (proj1 ((H0 y x) H14)).
decompose [or] H8.
apply (proj2 ((H0 x z) H14)).
apply (proj1 ((H0 z x) H14)).
assumption.
assumption.
assumption.
assumption.
assumption.
Qed.
Lemma not_sv :
forall (vert : list nat) (edg : list (nat*nat)),
is_sv (sv_search_aux vert edg) edg = false
-> (forall (x : nat),
In x vert
-> is_sv x edg = false).
Proof.
induction vert;intros.
inversion H0.
simpl in H.
destruct vert.
simpl in H0;decompose [or] H0.
subst;assumption.
intuition.
assert (is_sv a edg = true \/ is_sv a edg = false).
destruct (is_sv a edg);intuition.
decompose [or]H1;rewrite H2 in H.
rewrite H2 in H;apply False_ind;intuition.
simpl in H0.
decompose [or] H0;subst.
assumption.
apply IHvert;intuition.
apply IHvert;intuition.
Qed.
Lemma sv_sv_search_aux :
forall (vert : list nat) (edg : list (nat*nat)),
vert <> nil
-> is_lex_sorted edg
-> is_strict_ord edg
-> NoDup edg
-> (forall (x y : nat),
In (x,y) edg
-> In x vert /\ In y vert)
-> (exists x : nat, sv x vert edg)
-> is_sv (sv_search_aux vert edg) edg = true.
Proof.
intros.
assert (is_sv (sv_search_aux vert edg) edg = true \/ is_sv (sv_search_aux vert edg) edg = false).
destruct (is_sv (sv_search_aux vert edg) edg);intuition.
decompose [or] H5.
assumption.
inversion H4.
assert (is_sv x edg = false).
apply (not_sv vert edg).
assumption.
inversion H7;assumption.
assert (is_sv x edg = true).
apply (sv_simplicial_vertex_aux2 vert edg x);assumption.
rewrite H9 in H8;apply False_ind;intuition.
Qed.
Lemma remove_in :
forall (l : list nat) (x y : nat),
In x (remove eq_nat_dec y l)
-> In x l.
Proof.
induction l;simpl;intros.
assumption.
destruct (eq_nat_dec y a).
right;eapply IHl;eassumption.
simpl in H;decompose [or]H.
intuition.
right;eapply IHl;eassumption.
Qed.
Lemma NoDup_remove :
forall (l : list nat) (x : nat),
NoDup l
-> NoDup (remove eq_nat_dec x l).
Proof.
induction l;intros;simpl.
assumption.
destruct (eq_nat_dec x a).
apply IHl;inversion H;assumption.
constructor.
unfold not;intro.
assert (In a l).
eapply remove_in;eassumption.
inversion H;intuition.
apply IHl;inversion H;assumption.
Qed.
Lemma rm_perm :
forall (l l' : list nat) (x : nat),
Permutation l l'
-> NoDup l
-> NoDup l'
-> Permutation (remove eq_nat_dec x l) (remove eq_nat_dec x l').
Proof.
induction 1;intros.
apply Permutation_refl.
simpl.
destruct (eq_nat_dec x x0).
subst.
apply IHPermutation.
inversion H0;assumption.
inversion H1;assumption.
constructor.
apply IHPermutation.
inversion H0;assumption.
inversion H1;assumption.
simpl.
destruct (eq_nat_dec x y);destruct (eq_nat_dec x x0);subst.
apply Permutation_refl.
apply Permutation_refl.
apply Permutation_refl.
constructor;apply Permutation_refl.
apply Permutation_trans with (l' := remove eq_nat_dec x l').
apply IHPermutation1.
assumption.
eapply NoDup_perm;eassumption.
apply IHPermutation2.
eapply NoDup_perm;eassumption.
assumption.
Qed.
Lemma in_NoDup_remove :
forall (l : list nat) (x : nat),
NoDup l
-> In x l
-> Permutation (x :: remove eq_nat_dec x l) l.
Proof.
induction l;intros.
inversion H0.
simpl.
destruct (eq_nat_dec x a).
subst.
constructor.
rewrite remove_not_in.
apply Permutation_refl.
inversion H;assumption.
apply Permutation_trans with (l' := a :: x :: remove eq_nat_dec x l).
constructor;apply Permutation_refl.
constructor.
apply IHl.
inversion H;assumption.
simpl in H0;decompose [or]H0.
apply False_ind;intuition.
assumption.
Qed.
Lemma rm_NoDup :
forall (vert l : list nat) (x : nat),
NoDup vert
-> Permutation (remove eq_nat_dec x vert) l
-> In x vert
-> Permutation vert (x :: l).
Proof.
induction vert;intros.
inversion H1.
simpl in H1;decompose [or]H1.
subst.
constructor.
simpl in H0;decompose [or]H0.
destruct (eq_nat_dec x x).
rewrite remove_not_in in H0.
assumption.
inversion H;assumption.
intuition.
simpl in H0.
destruct (eq_nat_dec x a).
subst.
inversion H;intuition.
assert (Permutation vert (x :: remove eq_nat_dec a l)).
apply (IHvert (remove eq_nat_dec a l) x).
inversion H;assumption.
assert (Permutation (remove eq_nat_dec a (remove eq_nat_dec x (a :: vert)))
(remove eq_nat_dec a (remove eq_nat_dec x (x :: l)))).
simpl.
destruct (eq_nat_dec x a);destruct (eq_nat_dec x x).
subst.
intuition.
intuition.
apply rm_perm.
assert (l = remove eq_nat_dec x l).
rewrite (remove_not_in l x).
reflexivity.
unfold not;intro.
assert (In x (a :: remove eq_nat_dec x vert)).
apply Permutation_sym in H0.
eapply Permutation_in;eassumption.
simpl in H4;decompose [or]H4.
intuition.
assert (~In x (remove eq_nat_dec x vert)).
apply remove_In.
intuition.
rewrite H3 in H0.
assumption.
assert (a :: remove eq_nat_dec x vert = remove eq_nat_dec x (a :: vert)).
simpl;destruct (eq_nat_dec x a).
subst;intuition.
reflexivity.
rewrite H3.
apply NoDup_remove;assumption.
apply NoDup_remove.
eapply NoDup_perm.
eassumption.
assert (a :: remove eq_nat_dec x vert = remove eq_nat_dec x (a :: vert)).
simpl;destruct (eq_nat_dec x a).
subst;intuition.
reflexivity.
rewrite H3.
apply NoDup_remove;assumption.
intuition.
simpl in H3.
destruct (eq_nat_dec x a).
intuition.
destruct (eq_nat_dec x x).
simpl in H3.
destruct (eq_nat_dec a a).
rewrite remove_not_in in H3.
rewrite (remove_not_in l x) in H3.
assumption.
unfold not;intro.
assert (In x (a :: remove eq_nat_dec x vert)).
apply Permutation_sym in H0.
eapply Permutation_in;eassumption.
simpl in H5;decompose [or]H5.
intuition.
assert (~In x (remove eq_nat_dec x vert)).
apply remove_In.
intuition.
unfold not;intro.
assert (In a vert).
eapply remove_in;eassumption.
inversion H;intuition.
intuition.
intuition.
assumption.
apply Permutation_trans with (l' := a :: x :: remove eq_nat_dec a l).
constructor;assumption.
apply Permutation_trans with (l' := x :: a :: remove eq_nat_dec a l).
constructor;apply Permutation_refl.
constructor.
apply in_NoDup_remove.
eapply NoDup_perm.
eassumption.
assert (a :: remove eq_nat_dec x vert = remove eq_nat_dec x (a :: vert)).
simpl.
destruct (eq_nat_dec x a).
intuition.
reflexivity.
rewrite H4.
apply NoDup_remove;assumption.
eapply Permutation_in.
eassumption.
intuition.
Qed.
Lemma sv_perm :
forall (vert pvert : list nat) (edg : list (nat*nat)) (x : nat),
Permutation vert pvert
-> sv x vert edg
-> sv x pvert edg.
Proof.
intros;constructor.
eapply Permutation_in;inversion H0;eassumption.
inversion H0.
intros;apply H2.
assumption.
assumption.
assumption.
apply Permutation_sym in H.
eapply Permutation_in;eassumption.
apply Permutation_sym in H.
eapply Permutation_in;eassumption.
assumption.
assumption.
Qed.
Lemma rm_diff :
forall (edg : list (nat*nat)) (x y z : nat),
x <> y
-> x <> z
-> In (y,z) edg
-> In (y,z) (rm x edg).
Proof.
induction edg;intros.
inversion H1.
destruct a;simpl.
destruct (eq_nat_dec x n).
subst.
simpl in H1;decompose [or] H1.
inversion H2;apply False_ind;intuition.
apply IHedg;assumption.
destruct (eq_nat_dec x n0).
subst.
simpl in H1;decompose [or] H1.
inversion H2;apply False_ind;intuition.
apply IHedg;assumption.
simpl in H1;decompose [or] H1.
rewrite H2;intuition.
simpl;right;apply IHedg;assumption.
Qed.
Lemma rm_only_diff :
forall (l : list (nat*nat)) (x y z : nat),
In (x,y) (rm z l)
-> x <> z /\ y <> z.
Proof.
induction l;intros.
inversion H.
destruct a;simpl in H.
destruct (eq_nat_dec z n).
apply IHl;assumption.
destruct (eq_nat_dec z n0).
apply IHl;assumption.
simpl in H;decompose [or] H.
inversion H0;intuition.
apply IHl;assumption.
Qed.
Lemma rm_in :
forall (edg : list (nat*nat)) (x y z :nat),
In (x,y) (rm z edg)
-> In (x,y) edg.
Proof.
induction edg;intros.
assumption.
destruct a;simpl in H.
destruct (eq_nat_dec z n).
subst.
simpl;right;eapply IHedg;eassumption.
destruct (eq_nat_dec z n0).
simpl;right;eapply IHedg;eassumption.
simpl in H;decompose [or] H.
rewrite H0;intuition.
simpl;right;eapply IHedg;eassumption.
Qed.
Lemma lex_rm_aux :
forall (l : list (nat*nat)) (x y z : nat),
is_lex_sorted ((y,z) :: l)
-> is_lex_sorted ((y,z) :: rm x l).
Proof.
induction l;intros.
assumption.
destruct a;simpl.
destruct (eq_nat_dec x n).
apply IHl;eapply is_lex_sorted_rmsnd;eassumption.
destruct (eq_nat_dec x n0).
apply IHl;eapply is_lex_sorted_rmsnd;eassumption.
subst;constructor.
inversion H;assumption.
apply IHl;eapply is_lex_sorted_tail;eassumption.
Qed.
Lemma lex_rm :
forall (l : list (nat*nat)) (x : nat),
is_lex_sorted l
-> is_lex_sorted (rm x l).
Proof.
induction l;intros.
assumption.
destruct a;simpl.
destruct (eq_nat_dec x n).
apply IHl;eapply is_lex_sorted_tail;eassumption.
destruct (eq_nat_dec x n0).
apply IHl;eapply is_lex_sorted_tail;eassumption.
apply lex_rm_aux;assumption.
Qed.
Lemma strict_ord_rm :
forall (l : list (nat*nat)) (x : nat),
is_strict_ord l
-> is_strict_ord (rm x l).
Proof.
induction l;intros.
assumption.
destruct a;simpl.
destruct (eq_nat_dec x n).
apply IHl;inversion H;assumption.
destruct (eq_nat_dec x n0).
apply IHl;inversion H;assumption.
constructor;[ | apply IHl];inversion H;assumption.
Qed.
Lemma NoDup_rm :
forall (edg : list (nat*nat)) (x : nat),
NoDup edg
-> NoDup (rm x edg).
Proof.
induction 1.
simpl;constructor.
destruct x0;simpl.
destruct (eq_nat_dec x n).
assumption.
destruct (eq_nat_dec x n0).
assumption.
constructor.
unfold not;intro.
assert (In (n,n0) l).
eapply rm_in;eassumption.
intuition.
assumption.
Qed.
Lemma _peo_construction :
forall (l vert : list nat) (edg : list (nat*nat)) (x : nat),
_peo l (remove eq_nat_dec x vert) (rm x edg)
-> NoDup vert
-> sv x vert edg
-> _peo (x :: l) vert edg.
Proof.
intros.
constructor.
inversion H.
inversion H1.
apply rm_NoDup.
assumption.
assumption.
inversion H1;assumption.
intros.
inversion H.
destruct ll.
assert (x = x0).
simpl in H2;inversion H2;intuition.
subst.
simpl in H2.
apply (sv_perm vert (x0 :: rl) edg).
inversion H2.
rewrite H6 in H3.
apply rm_NoDup.
assumption.
assumption.
inversion H1;assumption.
assumption.
simpl in H2.
inversion H2.
constructor.
intuition.
assert (sv x0 (x0 :: rl) (rm x edg)).
apply (H4 x0 ll rl);assumption.
inversion H8.
intros.
assert (~In x l).
unfold not;intro.
assert (In x (remove eq_nat_dec x vert)).
eapply Permutation_in.
apply Permutation_sym;eassumption.
assumption.
assert (~In x (remove eq_nat_dec x vert)).
apply remove_In.
intuition.
clear H;clear H0;clear H1;clear H2;clear H4;clear H5;
clear H6;clear H7;clear H13;clear H14;clear H15.
assert (In y l).
rewrite H10.
intuition.
assert (In z l).
rewrite H10;intuition.
assert (In x0 l).
rewrite H10;intuition.
assert (In (y,z) (rm x edg) \/ In (z,y) (rm x edg)).
apply H12.
assumption.
assumption.
assumption.
assumption.
assumption.
decompose [or] H21;[left|right];apply rm_diff.
unfold not;intro.
rewrite <-H4 in H1;intuition.
unfold not;intro.
rewrite <-H4 in H;intuition.
assumption.
unfold not;intro.
rewrite <-H4 in H;intuition.
unfold not;intro.
rewrite <-H4 in H1;intuition.
assumption.
decompose [or] H22;[left|right];apply rm_diff.
unfold not;intro.
rewrite <-H4 in H1;intuition.
unfold not;intro.
rewrite <-H4 in H0;intuition.
assumption.
unfold not;intro.
rewrite <-H4 in H0;intuition.
unfold not;intro.
rewrite <-H4 in H1;intuition.
assumption.
decompose [or] H2;[left|right];eapply rm_in;eassumption.
Qed.
Lemma ex_peo_ex_sv :
forall (l vert : list nat) (edg : list (nat*nat)) (x : nat),
_peo (x :: l) vert edg
-> sv x vert edg.
Proof.
intros.
inversion H.
assert (sv x (x :: l) edg).
apply (H1 x nil l);intuition.
eapply sv_perm.
apply Permutation_sym;eassumption.
assumption.
Qed.
Lemma in_rm_aux :
forall (vert : list nat) (x y : nat),
In x vert
-> x <> y
-> In x (remove eq_nat_dec y vert).
Proof.
induction vert;intros.
inversion H.
simpl.
destruct (eq_nat_dec y a).
subst.
simpl in H;decompose [or] H.
apply False_ind;intuition.
apply IHvert;assumption.
simpl in H;decompose [or] H.
subst;intuition.
simpl;right;apply IHvert;assumption.
Qed.
Lemma in_rm:
forall (edg : list (nat*nat)) (vert : list nat) (x y z : nat),
In x vert
-> In y vert
-> In (x,y) (rm z edg)
-> In x (remove eq_nat_dec z vert)
/\ In y (remove eq_nat_dec z vert).
Proof.
induction edg;intros.
inversion H1.
destruct a;simpl in H1.
destruct (eq_nat_dec z n).
subst.
apply IHedg;assumption.
destruct (eq_nat_dec z n0).
subst.
apply IHedg;assumption.
simpl in H1;decompose [or] H1.
inversion H2.
subst.
split;apply in_rm_aux;intuition.
apply IHedg;assumption.
Qed.
Lemma rm_nodup_lth :
forall (l : list nat) (x k : nat),
In x l
-> NoDup l
-> length l = S k
-> length (remove eq_nat_dec x l) = k.
Proof.
induction l;intros.
inversion H.
simpl.
destruct (eq_nat_dec x a).
subst.
rewrite remove_not_in.
intuition.
inversion H0;assumption.
simpl.
destruct k.
assert (l = nil).
apply lth_0_nil.
intuition.
subst.
simpl in H;decompose [or] H;apply False_ind;intuition.
apply eq_S.
apply IHl.
simpl in H;decompose [or] H.
apply False_ind;intuition.
assumption.
inversion H0;assumption.
intuition.
Qed.
Lemma sv_rm :
forall (edg : list (nat*nat)) (l : list nat) (x y : nat),
sv x l edg
-> sv x l (rm y edg).
Proof.
induction 1.
constructor.
assumption.
intros.
assert (x <> y).
decompose [or] H6.
apply (proj1 ((rm_only_diff edg x y0 y) H8)).
apply (proj2 ((rm_only_diff edg y0 x y) H8)).
assert (z <> y).
decompose [or] H7.
apply (proj2 ((rm_only_diff edg x z y) H9)).
apply (proj1 ((rm_only_diff edg z x y) H9)).
assert (y0 <> y).
decompose [or] H6.
apply (proj2 ((rm_only_diff edg x y0 y) H10)).
apply (proj1 ((rm_only_diff edg y0 x y) H10)).
assert (In (y0,z) edg \/ In (z,y0) edg).
apply H0.
assumption.
assumption.
assumption.
assumption.
assumption.
decompose [or] H6;[left | right];eapply rm_in;eassumption.
decompose [or] H7;[left | right];eapply rm_in;eassumption.
decompose [or] H11;[left | right];apply rm_diff;intuition.
Qed.
Lemma in_ex_app :
forall (l : list nat) (x : nat),
In x l
-> exists ll : list nat,
exists rl : list nat,
l = ll ++ x :: rl.
Proof.
induction l;intros.
inversion H.
simpl in H;decompose [or] H.
subst.
exists (@nil nat).
exists l.
reflexivity.
assert (exists ll : list nat,
exists rl : list nat,
l = ll ++ x :: rl).
apply IHl;assumption.
inversion H1.
exists (a :: x0).
inversion H2.
exists x1.
simpl.
rewrite H3;reflexivity.
Qed.
Lemma rm_app :
forall (l rl ll : list nat) (x y : nat),
x <> y
-> l = ll ++ x :: rl
-> remove eq_nat_dec y l = (remove eq_nat_dec y ll) ++ x :: (remove eq_nat_dec y rl).
Proof.
induction l;intros.
assert (In x nil).
rewrite H0;intuition.
inversion H1.
simpl.
destruct (eq_nat_dec y a).
subst.
destruct ll.
simpl in H0.
inversion H0;apply False_ind;intuition.
simpl in H0;inversion H0.
rewrite <-H3.
simpl.
destruct (eq_nat_dec n n).
apply IHl;intuition.
intuition.
destruct ll.
simpl in H0;inversion H0.
simpl;reflexivity.
simpl in H0;inversion H0.
rewrite <-H3.
simpl.
destruct (eq_nat_dec y n0).
inversion H0;apply False_ind;intuition.
simpl.
assert (remove eq_nat_dec y l = remove eq_nat_dec y ll ++ x :: remove eq_nat_dec y rl).
apply IHl;assumption.
rewrite H1;reflexivity.
Qed.
Lemma app_nodup_eq :
forall (ll1 ll2 rl1 rl2 : list nat) (x : nat),
~In x ll1
-> ~In x ll2
-> ~In x rl1
-> ~In x rl2
-> ll1 ++ x :: rl1 = ll2 ++ x :: rl2
-> rl1 = rl2.
Proof.
induction ll1;intros.
simpl in H3.
destruct ll2.
simpl in H3.
inversion H3.
reflexivity.
inversion H3.
subst;apply False_ind;intuition.
destruct ll2.
simpl in H3.
inversion H3.
subst;apply False_ind;intuition.
inversion H3.
subst.
apply (IHll1 ll2 rl1 rl2 x);intuition.
Qed.
Lemma nodup_in_app :
forall (l ll rl : list nat) (x : nat),
NoDup l
-> l = ll ++ x :: rl
-> ~In x ll /\ ~In x rl.
Proof.
induction l;intros.
assert (In x nil).
rewrite H0;intuition.
inversion H1.
destruct ll.
inversion H0.
subst.
split.
intuition.
inversion H;assumption.
assert (~In x ll /\ ~In x rl).
apply IHl.
inversion H;assumption.
inversion H0;intuition.
split.
unfold not;intro.
simpl in H2;decompose [or] H2.
subst.
inversion H0.
rewrite H4 in *.
inversion H.
rewrite H5 in H7.
apply False_ind;intuition.
intuition.
intuition.
Qed.
Lemma NoDup_rm_app_l :
forall (l ll rl : list nat) (x y : nat),
NoDup l
-> l = ll ++ x :: rl
-> NoDup (remove eq_nat_dec y ll ++ x :: rl).
Proof.
induction l;intros.
assert (In x nil).
rewrite H0;intuition.
inversion H1.
destruct ll.
inversion H0.
subst.
simpl;assumption.
inversion H0.
subst.
simpl.
destruct (eq_nat_dec y n).
subst.
apply IHl.
inversion H;assumption.
reflexivity.
simpl.
constructor.
unfold not;intro.
assert (In n (ll ++ x :: rl)).
assert (In n (remove eq_nat_dec y ll) \/ In n (x :: rl)).
apply in_app_or;assumption.
decompose [or] H2.
assert (In n ll).
eapply remove_in;eassumption.
intuition.
intuition.
inversion H;intuition.
apply IHl.
inversion H;assumption.
reflexivity.
Qed.
Lemma nodup_app_in_l :
forall (l ll rl : list nat) (x y : nat),
NoDup l
-> l = ll ++ y :: rl
-> In x ll
-> ~In x rl.
Proof.
induction l;intros.
assert (In x nil).
rewrite H0;intuition.
inversion H2.
destruct ll.
inversion H1.
simpl in H1;decompose [or] H1.
subst.
inversion H0.
subst.
inversion H.
unfold not;intro;intuition.
apply (IHl ll rl x y).
inversion H;assumption.
inversion H0;intuition.
assumption.
Qed.
Lemma nodup_app_in_r :
forall (l ll rl : list nat) (x y : nat),
NoDup l
-> l = ll ++ y :: rl
-> In x rl
-> ~In x ll.
Proof.
induction l;intros.
assert (In x nil).
rewrite H0;intuition.
inversion H2.
destruct ll.
intuition.
unfold not;intro.
simpl in H2;decompose [or] H2.
subst.
rewrite H0 in H.
inversion H;intuition.
inversion H0.
subst.
unfold not in IHl;apply (IHl ll rl x y).
inversion H;assumption.
intuition.
assumption.
assumption.
Qed.
Lemma sv_remove :
forall (l : list nat) (edg : list (nat*nat)) (x y : nat),
sv x (x :: l) edg
-> sv x (x :: remove eq_nat_dec y l) edg.
Proof.
intros.
inversion H;constructor.
intuition.
intros.
apply H1.
assumption.
assumption.
assumption.
simpl in H8;decompose [or] H8.
intuition.
simpl;right;eapply remove_in;eassumption.
simpl in H9;decompose [or] H9.
intuition.
simpl;right;eapply remove_in;eassumption.
assumption.
assumption.
Qed.
Lemma remove_peo :
forall (edg : list (nat*nat)) (l vert : list nat) (x : nat),
_peo l vert edg
-> NoDup vert
-> In x l
-> _peo (remove eq_nat_dec x l)
(remove eq_nat_dec x vert)
(rm x edg).
Proof.
induction 1;intro.
constructor.
apply rm_perm.
assumption.
assumption.
eapply NoDup_perm;eassumption.
intros.
destruct (eq_nat_dec x x0).
subst.
constructor.
intuition.
intros.
assert (x0 <> x0).
decompose [or] H9.
apply (proj1 ((rm_only_diff edg x0 y x0) H11)).
apply (proj2 ((rm_only_diff edg y x0 x0) H11)).
intuition.
assert (exists ll : list nat,
exists rl : list nat,
l = ll ++ x0 :: rl).
apply in_ex_app.
apply (remove_in l x0 x).
rewrite H3;intuition.
inversion H4;inversion H5.
assert (NoDup l).
eapply NoDup_perm;eassumption.
assert (remove eq_nat_dec x l = (remove eq_nat_dec x x1) ++ x0 :: (remove eq_nat_dec x x2)).
apply rm_app;intuition.
rewrite H3 in H8.
assert ({In x x1}+{In x x2}).
assert ({In x x1}+{~In x x1}).
apply In_dec;apply eq_nat_dec.
destruct H9.
left;assumption.
right.
assert (In x (x1 ++ x0 :: x2)).
rewrite <-H6;assumption.
assert (In x x1 \/ In x (x0 :: x2)).
apply in_app_or;assumption.
simpl in H10;decompose [or] H10.
apply False_ind;intuition.
apply False_ind;intuition.
assumption.
destruct H9.
rewrite (remove_not_in x2 x) in H8.
assert (NoDup (remove eq_nat_dec x l)).
apply NoDup_remove;assumption.
assert (rl = x2).
apply (app_nodup_eq ll (remove eq_nat_dec x x1) rl x2 x0).
unfold not;intro.
apply False_ind.
assert (~In x0 ll).
apply ((proj1 ((nodup_in_app (remove eq_nat_dec x l) ll rl x0) H9 H3))).
intuition.
assert (NoDup (remove eq_nat_dec x x1 ++ x0 :: x2)).
apply (NoDup_rm_app_l l x1 x2 x0 x);assumption.
rewrite H8 in H3.
apply ((proj1 ((nodup_in_app (remove eq_nat_dec x l) (remove eq_nat_dec x x1) x2 x0) H9 H3))).
apply (proj2 ((nodup_in_app (remove eq_nat_dec x l) ll rl x0) H9 H3)).
rewrite <-H3 in H8.
apply (proj2 ((nodup_in_app (remove eq_nat_dec x l) (remove eq_nat_dec x x1) x2 x0) H9 H8)).
assumption.
assert (sv x0 (x0 :: rl) edg).
eapply H0.
rewrite <-H10 in H6;eassumption.
eapply sv_rm;eassumption.
eapply nodup_app_in_l;eassumption.
rewrite (remove_not_in) in H8.
assert (sv x0 (x0 :: x2) (rm x edg)).
assert (sv x0 (x0 :: x2) edg).
eapply H0;eassumption.
eapply sv_rm;eassumption.
assert (NoDup (remove eq_nat_dec x l)).
apply NoDup_remove;assumption.
assert (rl = remove eq_nat_dec x x2).
apply (app_nodup_eq ll x1 rl (remove eq_nat_dec x x2) x0).
apply (proj1 ((nodup_in_app (remove eq_nat_dec x l) ll rl x0) H10 H3)).
rewrite H8 in H3.
apply (proj1 ((nodup_in_app (remove eq_nat_dec x l) x1 (remove eq_nat_dec x x2) x0) H10 H3)).
apply (proj2 ((nodup_in_app (remove eq_nat_dec x l) ll rl x0) H10 H3)).
rewrite H8 in H3.
apply (proj2 ((nodup_in_app (remove eq_nat_dec x l) x1 (remove eq_nat_dec x x2) x0) H10 H3)).
assumption.
rewrite H11.
apply sv_remove;assumption.
apply (nodup_app_in_r l x1 x2 x x0);assumption.
Qed.
Lemma peo_peo_search_aux :
forall (k : nat) (vert l : list nat) (edg : list (nat*nat)),
_peo l vert edg
-> is_lex_sorted edg
-> is_strict_ord edg
-> NoDup edg
-> (forall (x y : nat),
In (x,y) edg
-> In x vert /\ In y vert)
-> NoDup vert
-> length vert = k
-> _peo (peo_search_aux vert edg) vert edg.
Proof.
induction k;intros.
induction vert.
rewrite peo_search_aux_equation.
constructor.
apply Permutation_refl.
intros.
assert (In x nil).
rewrite H6;intuition.
inversion H7.
inversion H5.
induction vert.
inversion H5.
rewrite peo_search_aux_equation.
apply _peo_construction.
apply (IHk (remove eq_nat_dec (sv_search_aux (a :: vert) edg) (a :: vert))
(remove eq_nat_dec (sv_search_aux (a :: vert) edg) l)
(rm (sv_search_aux (a :: vert) edg) edg)).
apply remove_peo.
assumption.
assumption.
assert (In (sv_search_aux (a :: vert) edg) (a :: vert)).
apply in_sv_search_aux.
discriminate.
inversion H.
eapply Permutation_in;eassumption.
apply lex_rm;assumption.
apply strict_ord_rm;assumption.
apply NoDup_rm;assumption.
intros;eapply in_rm.
apply ((proj1 ((H3 x y) ((rm_in edg x y (sv_search_aux (a :: vert) edg) H6))))).
apply ((proj2 ((H3 x y) ((rm_in edg x y (sv_search_aux (a :: vert) edg) H6))))).
eassumption.
apply NoDup_remove;assumption.
apply rm_nodup_lth.
apply in_sv_search_aux;discriminate.
assumption.
assumption.
assumption.
apply sv_simplicial_vertex_aux.
apply sv_sv_search_aux.
discriminate.
assumption.
assumption.
assumption.
assumption.
destruct l.
inversion H.
assert (a :: vert = nil).
apply Permutation_nil;apply Permutation_sym;assumption.
discriminate.
exists n.
eapply ex_peo_ex_sv.
eassumption.
apply in_sv_search_aux.
discriminate.
Qed.
Lemma peo_peo_search :
forall (g : graph),
(exists l : list nat,
peo l g)
->
peo (peo_search g) g.
Proof.
intros.
unfold peo;unfold peo_search.
inversion H.
apply (peo_peo_search_aux (length (vertices g)) (vertices g) x (edges g)).
unfold peo in H0;assumption.
apply is_lex_sorted_edges.
apply is_strict_ord_edges.
apply NoDup_edges.
rewrite vertices_edges.
apply in_vertices;assumption.
apply strict_inc_NoDup.
rewrite vertices_edges.
apply is_strict_inc_vertices.
reflexivity.
Qed.
Lemma sv_add_hd : forall (l : list nat) (x y : nat) (edg : list (nat*nat)),
sv x (y :: l) edg ->
NoDup (y :: l) ->
In x l ->
sv x l edg.
Proof.
constructor;inversion H.
simpl in H2;decompose [or] H2.
subst;apply False_ind.
inversion H0;intuition.
assumption.
intuition.
Qed.
Lemma sv_equiv : forall (vert : list nat) (x : nat) (edg : list (nat*nat)),
(forall (x y : nat),
In (x,y) edg
-> In x vert /\ In y vert)
-> is_lex_sorted edg
-> is_strict_ord edg
-> NoDup edg
-> In x vert
-> (sv x vert edg <-> is_sv x edg = true).
Proof.
split;intros.
eapply sv_simplicial_vertex_aux2;eassumption.
apply sv_simplicial_vertex_aux;assumption.
Qed.
Lemma sv_dec : forall (vert : list nat) (x : nat) (edg : list (nat*nat)),
(forall (x y : nat),
In (x,y) edg
-> In x vert /\ In y vert)
-> is_lex_sorted edg
-> is_strict_ord edg
-> NoDup edg
-> In x vert
-> NoDup vert
-> {sv x vert edg}+{~sv x vert edg}.
Proof.
intros.
assert ({is_sv x edg = true}+{is_sv x edg = false}).
intuition.
destruct H5.
left;apply (proj2 (sv_equiv vert x edg H H0 H1 H2 H3));
assumption.
right;unfold not;intro.
assert (is_sv x edg = true).
apply (proj1 (sv_equiv vert x edg H H0 H1 H2 H3));assumption.
rewrite e in H6;intuition.
Qed.
Lemma _peo_dec : forall (l vert : list nat) (edg : list (nat*nat)),
(forall (x y : nat),
In (x,y) edg
-> In x vert /\ In y vert)
-> is_lex_sorted edg
-> is_strict_ord edg
-> NoDup edg
-> NoDup vert
->{_peo l vert edg}+{~_peo l vert edg}.
Proof.
induction l;intros.
destruct vert.
left.
constructor.
apply Permutation_refl.
intros.
assert (In x nil).
rewrite H4;intuition.
inversion H5.
right.
unfold not;intro.
inversion H4.
assert (In n nil).
eapply Permutation_in.
eassumption.
intuition.
inversion H10.
generalize (IHl (remove eq_nat_dec a vert) (rm a edg));intro.
destruct H4.
intros;eapply in_rm.
apply (proj1 (H x y (rm_in edg x y a H4))).
apply (proj2 (H x y (rm_in edg x y a H4))).
eassumption.
apply lex_rm;assumption.
apply strict_ord_rm;assumption.
apply NoDup_rm;assumption.
apply NoDup_remove;assumption.
destruct (In_dec eq_nat_dec a vert).
destruct (sv_dec vert a edg);try assumption.
left;apply _peo_construction;assumption.
right;unfold not in *;intro.
apply n;inversion H4.
assert (sv a (a :: l) edg).
apply (H6 a nil l);intuition.
eapply sv_perm.
apply Permutation_sym;eassumption.
assumption.
right;unfold not in *;intro.
inversion H4.
apply n.
eapply Permutation_in.
apply Permutation_sym;eassumption.
intuition.
right;unfold not in *;intro.
apply n.
replace l with (remove eq_nat_dec a (a :: l)).
apply remove_peo;intuition.
simpl;destruct (eq_nat_dec a a).
apply remove_not_in.
inversion H4.
assert (NoDup (a :: l)).
eapply NoDup_perm.
eassumption.
assumption.
inversion H10;assumption.
intuition.
Qed.
Lemma peo_dec : forall (l : list nat) (g : graph),
{peo l g}+{~peo l g}.
Proof.
unfold peo;intros;apply _peo_dec.
intros;rewrite vertices_edges;apply in_vertices;assumption.
apply is_lex_sorted_edges.
apply is_strict_ord_edges.
apply NoDup_edges.
apply strict_inc_NoDup; rewrite vertices_edges;
apply is_strict_inc_vertices.
Qed.
Lemma ex_peo_dec : forall (g : graph),
{exists l : list nat, peo l g}+{~exists l :list nat, peo l g}.
Proof.
intro.
destruct (peo_dec (peo_search g) g).
left;exists (peo_search g);assumption.
right;unfold not in *;intro;apply n;
apply peo_peo_search;assumption.
Qed.