Created
August 19, 2020 13:10
-
-
Save chdoc/7aa7b1ce0a2adcb23fef654c5f42d7b3 to your computer and use it in GitHub Desktop.
Lemmas on subseq, next, arc, findex etc.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Setoid Morphisms. | |
From mathcomp Require Import all_ssreflect. | |
Set Implicit Arguments. | |
Unset Strict Implicit. | |
Unset Printing Implicit Defensive. | |
Lemma iter_id (T : Type) n : @iter T n id =1 id. | |
Proof. by elim: n. Qed. | |
(** ** Lemmas on [index], [mask], and [subseq] *) | |
(** could go to seq.v *) | |
Lemma rev_mask (T : Type) (m : bitseq) (s : seq T) : | |
size m = size s -> rev (mask m s) = mask (rev m) (rev s). | |
Proof. | |
elim: m s => [|b m IHm] [|x s] //= /eqP m_s. | |
have ? : size m = size s by exact/eqP. | |
rewrite fun_if !rev_cons -!cats1 IHm // mask_cat ?size_rev //. | |
by case: b => //=; rewrite cats0. | |
Qed. | |
Lemma eqseq_pivot (T : eqType) (s1 s2 s3 s4 : seq T) (x : T) : | |
uniq (s1 ++ x :: s2) -> uniq (s3 ++ x :: s4) -> | |
s1 ++ x :: s2 == s3 ++ x :: s4 = (s1 == s3) && (s2 == s4). | |
Proof. | |
move=> uniq12 uniq34; apply/idP/idP => [E|/andP [/eqP-> /eqP->] //]. | |
suff S : size s1 = size s3 by rewrite eqseq_cat // eqseq_cons eqxx in E. | |
gen have I,I1 : s1 s2 uniq12 {E} / size s1 = index x (s1 ++ x :: s2). | |
rewrite index_cat index_head addn0 ifN //. | |
by apply: contraTN uniq12 => x_s1; rewrite cat_uniq /= x_s1 /= andbF. | |
by rewrite I1 (eqP E) -I. | |
Qed. | |
Lemma subseq_cat2l (T : eqType) (l s1 s2 : seq T) : | |
subseq (l ++ s1) (l ++ s2) = subseq s1 s2. | |
Proof. elim: l => // x l IHl. by rewrite !cat_cons /= eqxx. Qed. | |
Lemma subseq_rev (T : eqType) (s1 s2 : seq T) : | |
subseq (rev s1) (rev s2) = subseq s1 s2. | |
Proof. | |
apply/subseqP/subseqP => -[m] size_m mask_m; exists (rev m). | |
all: rewrite ?size_rev // in size_m *. | |
- by rewrite -[s1]revK mask_m rev_mask ?size_rev // revK. | |
- by rewrite -rev_mask // mask_m. | |
Qed. | |
Lemma subseq_cat2r (T : eqType) (l s1 s2 : seq T) : | |
subseq (s1 ++ l) (s2 ++ l) = subseq s1 s2. | |
Proof. by rewrite -subseq_rev !rev_cat subseq_cat2l subseq_rev. Qed. | |
Lemma subseqLR (T : eqType) (s1 s2 s3 s4 : seq T) x : | |
uniq (s3 ++ [:: x] ++ s4) -> | |
subseq (s1 ++ [:: x] ++ s2) (s3 ++ [:: x] ++ s4) -> subseq s1 s3 /\ subseq s2 s4. | |
Proof. | |
move => uniq_s' sub_s_s'; have uniq_s := subseq_uniq sub_s_s' uniq_s'. | |
have/eqP {sub_s_s' uniq_s'} := subseq_uniqP uniq_s' sub_s_s'. | |
rewrite !filter_cat /= mem_cat inE eqxx orbT /= => E. | |
move: (E); rewrite eqseq_pivot -?(eqP E) // => /andP [/eqP -> /eqP ->]. | |
by rewrite !filter_subseq. | |
Qed. | |
(* TOTHINK: the proof seems more complicated than necessary *) | |
Lemma index_subseq (T : eqType) x y (s1 s2 : seq T) : | |
y \in s1 -> subseq s1 s2 -> uniq s2 -> | |
index x s1 <= index y s1 -> index x s2 <= index y s2. | |
Proof. | |
move=> y_s1 sub_s1_s2 uniq_s2 x_before_y. | |
have x_s1 : x \in s1. | |
{ by rewrite -index_mem; apply: leq_ltn_trans x_before_y _; rewrite index_mem. } | |
have x_s2 := mem_subseq sub_s1_s2 x_s1. | |
have uniq_s1 := subseq_uniq sub_s1_s2 uniq_s2. | |
case: (splitPr x_s2) uniq_s2 sub_s1_s2 => p1 p2 uniq_p. | |
case: (splitPr x_s1) uniq_s1 x_before_y y_s1 => u1 u2 uniq_s1 x_before_y y_s1. | |
move/subseqLR => /(_ uniq_p) => -[/mem_subseq sub1 /mem_subseq sub2]. | |
have xNp1 : x \notin p1. | |
{ by apply: contraTN uniq_p => x_p1; rewrite cat_uniq /= x_p1 andbF. } | |
suff yNp1 : y \notin p1. | |
{ rewrite index_cat (negbTE xNp1) index_head addn0. | |
by rewrite index_cat (negbTE yNp1) leq_addr. } | |
have yNu1 : y \notin u1. | |
{ apply: contraTN x_before_y => y_u1. | |
rewrite -ltnNge !index_cat y_u1 ifF ?index_head ?addn0 ?index_mem //. | |
apply: contraNF xNp1. exact: sub1. } | |
rewrite mem_cat (negbTE yNu1) /= in y_s1. | |
apply: contraTN uniq_p => y_p1. rewrite cat_uniq. | |
rewrite [has _ _](_ : is_true _) ?andbF //. | |
apply/hasP; exists y => //=. move: y_s1; rewrite !inE. | |
case: (_ == _) => //=. exact: sub2. | |
Qed. | |
Lemma subseq_rot (T : eqType) (p s : seq T) n : | |
subseq p s -> exists2 k, k <= n & subseq (rot k p) (rot n s). | |
Proof. | |
move => /subseqP [m size_m ->]. | |
exists (count id (take n m)); last by rewrite -mask_rot // mask_subseq. | |
apply: leq_trans (count_size _ _) _; rewrite size_take. | |
by case: (ltnP n (size m)). | |
Qed. | |
(** ** Lemmas on [next] and [rot] *) | |
(** could go to path.v *) | |
Section Path. | |
Lemma eq_traject (T : Type) (f g : T -> T) : f =1 g -> traject f =2 traject g. | |
Proof. move=> fg x n; elim: n x => //= n IHn x. by rewrite IHn fg. Qed. | |
Variable (T : eqType). | |
Implicit Types (s p : seq T) (x y : T). | |
Lemma head_rot s x0 n : n < size s -> head x0 (rot n s) = nth x0 s n. | |
Proof. | |
move=> n_lt_s; rewrite /rot -nth0 nth_cat size_drop subn_gt0 n_lt_s. | |
by rewrite -{2}[s](cat_take_drop n) nth_cat size_take n_lt_s ltnn subnn. | |
Qed. | |
Lemma next_cons x0 x s : next (x::s) x = head x0 (rcons s x). | |
Proof. by case: s => [|y s] /=; rewrite eqxx. Qed. | |
Lemma next_neq x p : x \in p -> uniq p -> 1 < size p -> x != next p x. | |
Proof. | |
move => x_p; have [i p' rot_p uniq_p] := rot_to x_p. | |
move: (uniq_p); rewrite -(next_rot i) // -(size_rot i) -(rot_uniq i) {}rot_p. | |
case: p' => //= y p'. rewrite inE eqxx. by case: (x == y). | |
Qed. | |
Lemma iter_next_rot x0 s n : | |
n < size s -> uniq s -> iter n (next s) (head x0 s) = head x0 (rot n s). | |
Proof. | |
elim: n s => [|n IHn] s; first by move => *; rewrite rot0. | |
case: s => [_ /= |x s]; first by rewrite (@eq_iter _ _ id) ?iter_id. | |
move => n_lt_s uniq_s. rewrite iterSr rotS 1?ltnW // rot_rot rot1_cons. | |
rewrite (next_cons x0). | |
under eq_iter => z do rewrite -(next_rot 1) ?rot1_cons //. | |
by rewrite IHn // ?size_rcons ?rcons_uniq // ltnW. | |
Qed. | |
Lemma iter_next x0 s n : | |
uniq s -> n < size s -> iter n (next s) (head x0 s) = nth x0 s n. | |
Proof. by move => *; rewrite iter_next_rot // head_rot. Qed. | |
Lemma traject_next x0 s : | |
uniq s -> traject (next s) (head x0 s) (size s) = s. | |
Proof. | |
move=> uniq_s. | |
apply: (@eq_from_nth _ x0); rewrite size_traject // => i i_lt_s. | |
rewrite (set_nth_default (head x0 s)) ?size_traject //. | |
by rewrite nth_traject // iter_next. | |
Qed. | |
End Path. | |
Lemma eq_findex (T : finType) (f g : T -> T) : | |
f =1 g -> findex f =2 findex g. | |
Proof. | |
move=> fg x y; rewrite /findex /index /orbit /order (eq_traject fg). | |
congr (_ _ (traject _ _ _)); exact/eq_card/eq_fconnect. | |
Qed. | |
Lemma findex_head (T : finType) (x y : T) (s : seq T) (uniq_xs : uniq (x::s)) : | |
findex (next (x :: s)) x y = index y (x :: s). | |
Proof. | |
rewrite /findex (_ : orbit (next (x::s)) x = x::s) // /orbit. | |
rewrite (@order_cycle _ _ (x::s)) ?mem_head ?cycle_next //. | |
exact: (@traject_next _ x). | |
Qed. | |
(* Require Import preliminaries. *) | |
(* already on mathcomp master *) | |
Axiom card_gt1P : | |
forall {T : finType} {A : pred T}, reflect (exists x y : T, [/\ x \in A, y \in A & x != y]) (1 < #|A|). | |
(* not yet in mathcomp *) | |
Axiom disjointP : | |
forall (T : finType) (A B : pred T), reflect (forall x : T, x \in A -> x \in B -> False) [disjoint A & B]. | |
Section UcycleArc. | |
Definition path0 (T : Type) (e : rel T) (s : seq T) := | |
if s is x::s then path e x s else true. | |
Variables (T : finType) (e : rel T) (s : seq T). | |
Hypothesis ucycle_s : ucycle e s. | |
Let cycle_s := ucycle_cycle ucycle_s. | |
Let uniq_s := ucycle_uniq ucycle_s. | |
Lemma arc_path x y (xDy : x != y) : | |
x \in s -> y \in s -> path0 e (arc s x y). | |
Proof. | |
move=> x_s y_s. | |
case: (rot_to_arc uniq_s x_s y_s xDy) => i s1 s2 <- _ E /=. | |
move: cycle_s. rewrite -(rot_cycle i) E /= rcons_path cat_path. | |
by case: (path e x s1). | |
Qed. | |
Lemma head_arc x y (xDy : x != y) : x \in s -> y \in s -> x \in arc s x y. | |
Proof. | |
move=> x_s y_s. | |
case: (rot_to_arc uniq_s x_s y_s xDy) => i s1 s2 <- _ _. | |
exact: mem_head. | |
Qed. | |
Lemma mem_arc x y z (xDy : x != y) : | |
x \in s -> y \in s -> | |
(z \in arc s x y) = (findex (next s) x z < findex (next s) x y). | |
Proof. | |
move=> x_s y_s; have [i s1 s2 A1 A2 R] := rot_to_arc uniq_s x_s y_s xDy. | |
under eq_findex => u do rewrite -(next_rot i) //. | |
under (@eq_findex _ (next s)) => u do rewrite -(next_rot i) //. | |
have uniq_xy : uniq (x :: s1 ++ y :: s2) by rewrite -R rot_uniq. | |
rewrite R !findex_head // -cat_cons !index_cat index_head. | |
rewrite -A1 [X in _ < X]ifN. | |
by case: ifP => [Hz|_]; rewrite ?ltn_add2l // addn0 index_mem Hz. | |
by apply: contraTN uniq_xy => C; rewrite -cat_cons cat_uniq /= C /= andbF. | |
Qed. | |
Lemma arc_disjoint2 x1 x2 : | |
x1 \in s -> x2 \in s -> x1 != x2 -> [disjoint arc s x1 x2 & arc s x2 x1]. | |
Proof. | |
move => x1_s x2_s x1Dx2. | |
have [n s1 s2 <- <- rot_s] := rot_to_arc uniq_s x1_s x2_s x1Dx2. | |
move: uniq_s. rewrite -(rot_uniq n) rot_s -cat_cons cat_uniq. | |
by rewrite disjoint_sym disjoint_has => /and3P [_ -> _]. | |
Qed. | |
Lemma arc_disjoint x1 x2 y1 y2 : | |
x1 \in s -> x2 \in s -> y1 \in s -> y2 \in s -> x1 != x2 -> y1 != y2 -> | |
findex (next s) x1 x2 <= findex (next s) x1 y1 -> | |
findex (next s) y1 y2 <= findex (next s) y1 x1 -> | |
[disjoint arc s x1 x2 & arc s y1 y2]. | |
Proof. | |
move=> x1_s x2_s y1_s y2_s x1Dx2 y1Dy2 index_x index_y. | |
have x1Dy1 : x1 != y1. | |
{ apply: contraNneq x1Dx2 => ?; subst y1. | |
by move: index_x; rewrite findex0 leqn0 findex_eq0. } | |
apply/pred0Pn => -[x] /=; rewrite !mem_arc // => /andP [A1 A2]. | |
have {A1 index_x} := leq_trans A1 index_x. | |
have {A2 index_y} := leq_trans A2 index_y. | |
rewrite -!mem_arc //= 1?eq_sym //. | |
by apply/disjointP/arc_disjoint2; rewrite // eq_sym. | |
Qed. | |
Variable p : seq T. | |
Hypothesis p_sub_s : subseq p s. | |
Let p_in_s := mem_subseq p_sub_s. | |
Let uniq_p := subseq_uniq p_sub_s uniq_s. | |
Lemma findex_next_other (x y : T) : | |
x \in p -> y \in p -> x != y -> findex (next s) x (next p x) <= findex (next s) x y. | |
Proof. | |
move=> x_p y_p xDy. | |
have x_s : x \in s by apply p_in_s. | |
have [n s' E] := (rot_to x_s). | |
under eq_findex => z do rewrite -(next_rot n) //. | |
under [X in _ <= X]eq_findex => z do rewrite -(next_rot n) //. | |
have uniq_xs : uniq (x :: s') by rewrite -E rot_uniq. | |
have [m _ sub] := subseq_rot n p_sub_s. | |
rewrite E !findex_head // -(next_rot m) //. rewrite E in sub. | |
have [p' P] : exists p', rot m p = x :: p'. | |
{ rewrite -(mem_rot m) in x_p. | |
case: (splitPr x_p) sub => p1 p2. rewrite -[x::s']cat0s. | |
move/subseqLR => /(_ uniq_xs). | |
by rewrite subseq0 => -[/eqP -> _]; exists p2. } | |
rewrite P. rewrite next_nth mem_head index_head. | |
destruct p' as [|y' p']. by rewrite /= eqxx leq0n. | |
rewrite [nth _ _ _]/= P in sub *. | |
apply: index_subseq sub _ _ => //. | |
by rewrite -P mem_rot. | |
by rewrite /= eqxx (negbTE xDy); case: (x == y'). | |
Qed. | |
Lemma arc_next_disjoint x y : | |
x \in p -> y \in p -> x != y -> | |
[disjoint arc s x (next p x) & arc s y (next p y)]. | |
Proof. | |
move=> x_p y_p xDy. | |
have x_s : x \in s by apply p_in_s. | |
have ? : 1 < size p. | |
{ apply: leq_trans (card_size _). by apply/card_gt1P; exists x,y. } | |
apply: arc_disjoint; try apply: p_in_s; rewrite ?mem_next //. | |
1-2: exact: next_neq. | |
all: by apply: findex_next_other; rewrite // eq_sym. | |
Qed. | |
End UcycleArc. | |
Print Assumptions arc_next_disjoint. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment