Skip to content

Instantly share code, notes, and snippets.

@chdoc
Created August 19, 2020 13:10
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save chdoc/7aa7b1ce0a2adcb23fef654c5f42d7b3 to your computer and use it in GitHub Desktop.
Save chdoc/7aa7b1ce0a2adcb23fef654c5f42d7b3 to your computer and use it in GitHub Desktop.
Lemmas on subseq, next, arc, findex etc.
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