Top

Module mathcomp.boot.path

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

   The basic theory of paths over an eqType; this file is essentially a
complement to seq.v. Paths are non-empty sequences that obey a progression
relation. They are passed around in three parts: the head and tail of the
sequence, and a proof of a (boolean) predicate asserting the progression.
This "exploded" view is rarely embarrassing, as the first two parameters
are usually inferred from the type of the third; on the contrary, it saves
the hassle of constantly constructing and destructing a dependent record.
   We define similarly cycles, for which we allow the empty sequence,
which represents a non-rooted empty cycle; by contrast, the "empty" path
from a point x is the one-item sequence containing only x.
  We allow duplicates; uniqueness, if desired (as is the case for several
geometric constructions), must be asserted separately. We do provide
shorthand, but only for cycles, because the equational properties of
"path" and "uniq" are unfortunately incompatible (esp. wrt "cat").
   We define notations for the common cases of function paths, where the
progress relation is actually a function. In detail:
  path e x p == x :: p is an e-path [:: x_0; x_1; ... ; x_n], i.e., we
                have e x_i x_{i+1} for all i < n. The path x :: p starts
                at x and ends at last x p.
 fpath f x p == x :: p is an f-path, where f is a function, i.e., p is of
                the form [:: f x; f (f x); ...]. This is just a notation
                for path (frel f) x p.
  sorted e s == s is an e-sorted sequence: either s = [::], or s = x :: p
                is an e-path (this is often used with e = leq or ltn).
   cycle e c == c is an e-cycle: either c = [::], or c = x :: p with
                x :: (rcons p x) an e-path.
  fcycle f c == c is an f-cycle, for a function f.
traject f x n == the f-path of size n starting at x
             := [:: x; f x; ...; iter n.-1 f x]
looping f x n == the f-paths of size greater than n starting at x loop
                back, or, equivalently, traject f x n contains all
                iterates of f at x.
merge e s1 s2 == the e-sorted merge of sequences s1 and s2: this is always
                a permutation of s1 ++ s2, and is e-sorted when s1 and s2
                are and e is total.
    sort e s == a permutation of the sequence s, that is e-sorted when e
                is total (computed by a merge sort with the merge function
                above).  This sort function is also designed to be stable.
  mem2 s x y == x, then y occur in the sequence (path) s; this is
                non-strict: mem2 s x x = (x \in s).
    next c x == the successor of the first occurrence of x in the sequence
                c (viewed as a cycle), or x if x \notin c.
    prev c x == the predecessor of the first occurrence of x in the
                sequence c (viewed as a cycle), or x if x \notin c.
   arc c x y == the sub-arc of the sequence c (viewed as a cycle) starting
                at the first occurrence of x in c, and ending just before
                the next occurrence of y (in cycle order); arc c x y
                returns an unspecified sub-arc of c if x and y do not both
                occur in c.
 ucycle e c <-> ucycleb e c (ucycle e c is a Coercion target of type Prop)
ufcycle f c <-> c is a simple f-cycle, for a function f.
 shorten x p == the tail a duplicate-free subpath of x :: p with the same
                endpoints (x and last x p), obtained by removing all loops
                from x :: p.
rel_base e e' h b <-> the function h is a functor from relation e to
                relation e', EXCEPT at points whose image under h satisfy
                the "base" predicate b:
                   e' (h x) (h y) = e x y UNLESS b (h x) holds
                This is the statement of the side condition of the path
                functorial mapping lemma map_path.
fun_base f f' h b <-> the function h is a functor from function f to f',
                except at the preimage of predicate b under h.
We also provide three segmenting dependently-typed lemmas (splitP, splitPl
and splitPr) whose elimination split a path x0 :: p at an internal point x
as follows:
 - splitP applies when x \in p; it replaces p with (rcons p1 x ++ p2), so
   that x appears explicitly at the end of the left part. The elimination
   of splitP will also simultaneously replace take (index x p) with p1 and
   drop (index x p).+1 p with p2.
 - splitPl applies when x \in x0 :: p; it replaces p with p1 ++ p2 and
   simultaneously generates an equation x = last x0 p1.
 - splitPr applies when x \in p; it replaces p with (p1 ++ x :: p2), so x
   appears explicitly at the start of the right part.
The parts p1 and p2 are computed using index/take/drop in all cases, but
only splitP attempts to substitute the explicit values. The substitution
of p can be deferred using the dependent equation generation feature of
ssreflect, e.g.: case/splitPr def_p: {1}p / x_in_p => [p1 p2] generates
the equation p = p1 ++ p2 instead of performing the substitution outright.
  Similarly, eliminating the loop removal lemma shortenP simultaneously
replaces shorten e x p with a fresh constant p', and last x p with
last x p'.
  Note that although all "path" functions actually operate on the
underlying sequence, we provide a series of lemmas that define their
interaction with the path and cycle predicates, e.g., the cat_path equation
can be used to split the path predicate after splitting the underlying
sequence.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Paths.

Variables (n0 : nat) (T : Type).

Section Path.

Variables (x0_cycle : T) (e : rel T).

Fixpoint path x (p : seq T) :=
  if p is y :: p' then e x y && path y p' else true.

Lemma cat_path x p1 p2 : path x (p1 ++ p2) = path x p1 && path (last x p1) p2.

Proof.

by elim: p1 x => [|y p1 Hrec] x //=; rewrite Hrec -!andbA. Qed.

Lemma rcons_path x p y : path x (rcons p y) = path x p && e (last x p) y.

Proof.

by rewrite -cats1 cat_path /= andbT. Qed.

Lemma take_path x p i : path x p -> path x (take i p).

Proof.

elim: p x i => [//| x p] IHp x' [//| i] /= /andP[-> ?]; exact: IHp. Qed.

Lemma pathP x p x0 :
  reflect (forall i, i < size p -> e (nth x0 (x :: p) i) (nth x0 p i))
          (path x p).

Proof.

elim: p x => [|y p IHp] x /=; first by left.
apply: (iffP andP) => [[e_xy /IHp e_p [] //] | e_p].
by split; [apply: (e_p 0) | apply/(IHp y) => i; apply: e_p i.+1].
Qed.

Definition cycle p := if p is x :: p' then path x (rcons p' x) else true.

Lemma cycle_path p : cycle p = path (last x0_cycle p) p.

Proof.

by case: p => //= x p; rewrite rcons_path andbC. Qed.

Lemma cycle_catC p q : cycle (p ++ q) = cycle (q ++ p).

Proof.

case: p q => [|x p] [|y q]; rewrite /= ?cats0 //=.
by rewrite !rcons_path !cat_path !last_cat /= -!andbA; do !bool_congr.
Qed.

Lemma rot_cycle p : cycle (rot n0 p) = cycle p.

Proof.

by rewrite cycle_catC cat_take_drop. Qed.

Lemma rotr_cycle p : cycle (rotr n0 p) = cycle p.

Proof.

by rewrite -rot_cycle rotrK. Qed.

Definition sorted s := if s is x :: s' then path x s' else true.

Lemma sortedP s x :
  reflect (forall i, i.+1 < size s -> e (nth x s i) (nth x s i.+1)) (sorted s).

Proof.

by case: s => *; [constructor|apply: (iffP (pathP _ _ _)); apply]. Qed.

Lemma path_sorted x s : path x s -> sorted s.

Proof.

by case: s => //= y s /andP[]. Qed.

Lemma path_min_sorted x s : all (e x) s -> path x s = sorted s.

Proof.

by case: s => //= y s /andP [->]. Qed.

Lemma pairwise_sorted s : pairwise e s -> sorted s.

Proof.

by elim: s => //= x s IHs /andP[/path_min_sorted -> /IHs]. Qed.

Lemma sorted_cat_cons s1 x s2 :
  sorted (s1 ++ x :: s2) = sorted (rcons s1 x) && path x s2.

Proof.

by case: s1 => [ | e1 s1] //=; rewrite -cat_rcons cat_path last_rcons.
Qed.

End Path.

Section PathEq.

Variables (e e' : rel T).

Lemma rev_path x p :
  path e (last x p) (rev (belast x p)) = path (fun z => e^~ z) x p.

Proof.

elim: p x => //= y p IHp x; rewrite rev_cons rcons_path -{}IHp andbC.
by rewrite -(last_cons x) -rev_rcons -lastI rev_cons last_rcons.
Qed.

Lemma rev_cycle p : cycle e (rev p) = cycle (fun z => e^~ z) p.

Proof.

case: p => //= x p; rewrite -rev_path last_rcons belast_rcons rev_cons.
by rewrite -[in LHS]cats1 cycle_catC.
Qed.

Lemma rev_sorted p : sorted e (rev p) = sorted (fun z => e^~ z) p.

Proof.

by case: p => //= x p; rewrite -rev_path lastI rev_rcons. Qed.

Lemma path_relI x s :
  path [rel x y | e x y && e' x y] x s = path e x s && path e' x s.

Proof.

by elim: s x => //= y s IHs x; rewrite andbACA IHs. Qed.

Lemma cycle_relI s :
  cycle [rel x y | e x y && e' x y] s = cycle e s && cycle e' s.

Proof.

by case: s => [|? ?]; last apply: path_relI. Qed.

Lemma sorted_relI s :
  sorted [rel x y | e x y && e' x y] s = sorted e s && sorted e' s.

Proof.

by case: s; last apply: path_relI. Qed.

End PathEq.

Section SubPath_in.

Variable (P : {pred T}) (e e' : rel T).
Hypothesis (ee' : {in P &, subrel e e'}).

Lemma sub_in_path x s : all P (x :: s) -> path e x s -> path e' x s.

Proof.

by elim: s x => //= y s ihs x /and3P [? ? ?] /andP [/ee' -> //]; apply/ihs/andP.
Qed.

Lemma sub_in_cycle s : all P s -> cycle e s -> cycle e' s.

Proof.

case: s => //= x s /andP [Px Ps].
by apply: sub_in_path; rewrite /= all_rcons Px.
Qed.

Lemma sub_in_sorted s : all P s -> sorted e s -> sorted e' s.

Proof.

by case: s => //; apply: sub_in_path. Qed.

End SubPath_in.

Section EqPath_in.

Variable (P : {pred T}) (e e' : rel T).
Hypothesis (ee' : {in P &, e =2 e'}).

Let e_e' : {in P &, subrel e e'}

Proof.

by move=> ? ? ? ?; rewrite ee'. Qed.

Let e'_e : {in P &, subrel e' e}

Proof.

by move=> ? ? ? ?; rewrite ee'. Qed.

Lemma eq_in_path x s : all P (x :: s) -> path e x s = path e' x s.

Proof.

by move=> Pxs; apply/idP/idP; apply: sub_in_path Pxs. Qed.

Lemma eq_in_cycle s : all P s -> cycle e s = cycle e' s.

Proof.

by move=> Ps; apply/idP/idP; apply: sub_in_cycle Ps. Qed.

Lemma eq_in_sorted s : all P s -> sorted e s = sorted e' s.

Proof.

by move=> Ps; apply/idP/idP; apply: sub_in_sorted Ps. Qed.

End EqPath_in.

Section SubPath.

Variables e e' : rel T.

Lemma sub_path : subrel e e' -> forall x p, path e x p -> path e' x p.

Proof.

by move=> ? ? ?; apply/sub_in_path/all_predT; apply: in2W. Qed.

Lemma sub_cycle : subrel e e' -> subpred (cycle e) (cycle e').

Proof.

by move=> ee' [] // ? ?; apply: sub_path. Qed.

Lemma sub_sorted : subrel e e' -> subpred (sorted e) (sorted e').

Proof.

by move=> ee' [] //=; apply: sub_path. Qed.

Lemma eq_path : e =2 e' -> path e =2 path e'.

Proof.

by move=> ? ? ?; apply/eq_in_path/all_predT; apply: in2W. Qed.

Lemma eq_cycle : e =2 e' -> cycle e =1 cycle e'.

Proof.

by move=> ee' [] // ? ?; apply: eq_path. Qed.

Lemma eq_sorted : e =2 e' -> sorted e =1 sorted e'.

Proof.

by move=> ee' [] // ? ?; apply: eq_path. Qed.

End SubPath.

Section Transitive_in.

Variables (P : {pred T}) (leT : rel T).

Lemma order_path_min_in x s :
  {in P & &, transitive leT} -> all P (x :: s) -> path leT x s -> all (leT x) s.

Proof.

move=> leT_tr; elim: s => //= y s ihs /and3P [Px Py Ps] /andP [xy ys].
rewrite xy {}ihs ?Px //=; case: s Ps ys => //= z s /andP [Pz Ps] /andP [yz ->].
by rewrite (leT_tr _ _ _ Py Px Pz).
Qed.

Hypothesis leT_tr : {in P & &, transitive leT}.

Lemma path_sorted_inE x s :
  all P (x :: s) -> path leT x s = all (leT x) s && sorted leT s.

Proof.

move=> Pxs; apply/idP/idP => [xs|/andP[/path_min_sorted<-//]].
by rewrite (order_path_min_in leT_tr) //; apply: path_sorted xs.
Qed.

Lemma sorted_pairwise_in s : all P s -> sorted leT s = pairwise leT s.

Proof.

by elim: s => //= x s IHs /andP [Px Ps]; rewrite path_sorted_inE ?IHs //= Px.
Qed.

Lemma path_pairwise_in x s :
  all P (x :: s) -> path leT x s = pairwise leT (x :: s).

Proof.

by move=> Pxs; rewrite -sorted_pairwise_in. Qed.

Lemma cat_sorted2 s s' : sorted leT (s ++ s') -> sorted leT s * sorted leT s'.

Proof.

by case: s => //= x s; rewrite cat_path => /andP[-> /path_sorted]. Qed.

Lemma sorted_mask_in m s : all P s -> sorted leT s -> sorted leT (mask m s).

Proof.

by move=> Ps; rewrite !sorted_pairwise_in ?all_mask //; exact: pairwise_mask.
Qed.

Lemma sorted_filter_in a s : all P s -> sorted leT s -> sorted leT (filter a s).

Proof.

rewrite filter_mask; exact: sorted_mask_in. Qed.

Lemma path_mask_in x m s :
  all P (x :: s) -> path leT x s -> path leT x (mask m s).

Proof.

exact/(sorted_mask_in (true :: m)). Qed.

Lemma path_filter_in x a s :
  all P (x :: s) -> path leT x s -> path leT x (filter a s).

Proof.

by move=> Pxs; rewrite filter_mask; exact: path_mask_in. Qed.

Lemma sorted_ltn_nth_in x0 s : all P s -> sorted leT s ->
  {in [pred n | n < size s] &, {homo nth x0 s : i j / i < j >-> leT i j}}.

Proof.

by move=> Ps; rewrite sorted_pairwise_in //; apply/pairwiseP. Qed.

Hypothesis leT_refl : {in P, reflexive leT}.

Lemma sorted_leq_nth_in x0 s : all P s -> sorted leT s ->
  {in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> leT i j}}.

Proof.

move=> Ps s_sorted x y xs ys; rewrite leq_eqVlt=> /predU1P[->|].
  exact/leT_refl/all_nthP.
exact: sorted_ltn_nth_in.
Qed.

End Transitive_in.

Section Transitive.

Variable (leT : rel T).

Lemma order_path_min x s : transitive leT -> path leT x s -> all (leT x) s.

Proof.

by move=> leT_tr; apply/order_path_min_in/all_predT => //; apply: in3W.
Qed.

Hypothesis leT_tr : transitive leT.

Lemma path_le x x' s : leT x x' -> path leT x' s -> path leT x s.

Proof.

by case: s => [//| x'' s xlex' /= /andP[x'lex'' ->]]; rewrite (leT_tr xlex').
Qed.

Let leT_tr' : {in predT & &, transitive leT}

Proof.

exact: in3W. Qed.

Lemma path_sortedE x s : path leT x s = all (leT x) s && sorted leT s.

Proof.

exact/path_sorted_inE/all_predT. Qed.

Lemma sorted_pairwise s : sorted leT s = pairwise leT s.

Proof.

exact/sorted_pairwise_in/all_predT. Qed.

Lemma path_pairwise x s : path leT x s = pairwise leT (x :: s).

Proof.

exact/path_pairwise_in/all_predT. Qed.

Lemma sorted_mask m s : sorted leT s -> sorted leT (mask m s).

Proof.

exact/sorted_mask_in/all_predT. Qed.

Lemma sorted_filter a s : sorted leT s -> sorted leT (filter a s).

Proof.

exact/sorted_filter_in/all_predT. Qed.

Lemma path_mask x m s : path leT x s -> path leT x (mask m s).

Proof.

exact/path_mask_in/all_predT. Qed.

Lemma path_filter x a s : path leT x s -> path leT x (filter a s).

Proof.

exact/path_filter_in/all_predT. Qed.

Lemma sorted_ltn_nth x0 s : sorted leT s ->
  {in [pred n | n < size s] &, {homo nth x0 s : i j / i < j >-> leT i j}}.

Proof.

exact/sorted_ltn_nth_in/all_predT. Qed.

Hypothesis leT_refl : reflexive leT.

Lemma sorted_leq_nth x0 s : sorted leT s ->
  {in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> leT i j}}.

Proof.

exact/sorted_leq_nth_in/all_predT. Qed.

Lemma take_sorted n s : sorted leT s -> sorted leT (take n s).

Proof.

by rewrite -[s in sorted _ s](cat_take_drop n) => /cat_sorted2[]. Qed.

Lemma drop_sorted n s : sorted leT s -> sorted leT (drop n s).

Proof.

by rewrite -[s in sorted _ s](cat_take_drop n) => /cat_sorted2[]. Qed.

End Transitive.

End Paths.

Arguments pathP {T e x p}.
Arguments sortedP {T e s}.
Arguments path_sorted {T e x s}.
Arguments path_min_sorted {T e x s}.
Arguments order_path_min_in {T P leT x s}.
Arguments path_sorted_inE {T P leT} leT_tr {x s}.
Arguments sorted_pairwise_in {T P leT} leT_tr {s}.
Arguments path_pairwise_in {T P leT} leT_tr {x s}.
Arguments sorted_mask_in {T P leT} leT_tr {m s}.
Arguments sorted_filter_in {T P leT} leT_tr {a s}.
Arguments path_mask_in {T P leT} leT_tr {x m s}.
Arguments path_filter_in {T P leT} leT_tr {x a s}.
Arguments sorted_ltn_nth_in {T P leT} leT_tr x0 {s}.
Arguments sorted_leq_nth_in {T P leT} leT_tr leT_refl x0 {s}.
Arguments order_path_min {T leT x s}.
Arguments path_sortedE {T leT} leT_tr x s.
Arguments sorted_pairwise {T leT} leT_tr s.
Arguments path_pairwise {T leT} leT_tr x s.
Arguments sorted_mask {T leT} leT_tr m {s}.
Arguments sorted_filter {T leT} leT_tr a {s}.
Arguments path_mask {T leT} leT_tr {x} m {s}.
Arguments path_filter {T leT} leT_tr {x} a {s}.
Arguments sorted_ltn_nth {T leT} leT_tr x0 {s}.
Arguments sorted_leq_nth {T leT} leT_tr leT_refl x0 {s}.

Section HomoPath.

Variables (T T' : Type) (P : {pred T}) (f : T -> T') (e : rel T) (e' : rel T').

Lemma path_map x s : path e' (f x) (map f s) = path (relpre f e') x s.

Proof.

by elim: s x => //= y s <-. Qed.

Lemma cycle_map s : cycle e' (map f s) = cycle (relpre f e') s.

Proof.

by case: s => //= ? ?; rewrite -map_rcons path_map. Qed.

Lemma sorted_map s : sorted e' (map f s) = sorted (relpre f e') s.

Proof.

by case: s; last apply: path_map. Qed.

Lemma homo_path_in x s : {in P &, {homo f : x y / e x y >-> e' x y}} ->
  all P (x :: s) -> path e x s -> path e' (f x) (map f s).

Proof.

by move=> f_mono; rewrite path_map; apply: sub_in_path. Qed.

Lemma homo_cycle_in s : {in P &, {homo f : x y / e x y >-> e' x y}} ->
  all P s -> cycle e s -> cycle e' (map f s).

Proof.

by move=> f_mono; rewrite cycle_map; apply: sub_in_cycle. Qed.

Lemma homo_sorted_in s : {in P &, {homo f : x y / e x y >-> e' x y}} ->
  all P s -> sorted e s -> sorted e' (map f s).

Proof.

by move=> f_mono; rewrite sorted_map; apply: sub_in_sorted. Qed.

Lemma mono_path_in x s : {in P &, {mono f : x y / e x y >-> e' x y}} ->
  all P (x :: s) -> path e' (f x) (map f s) = path e x s.

Proof.

by move=> f_mono; rewrite path_map; apply: eq_in_path. Qed.

Lemma mono_cycle_in s : {in P &, {mono f : x y / e x y >-> e' x y}} ->
  all P s -> cycle e' (map f s) = cycle e s.

Proof.

by move=> f_mono; rewrite cycle_map; apply: eq_in_cycle. Qed.

Lemma mono_sorted_in s : {in P &, {mono f : x y / e x y >-> e' x y}} ->
  all P s -> sorted e' (map f s) = sorted e s.

Proof.

by case: s => // x s; apply: mono_path_in. Qed.

Lemma homo_path x s : {homo f : x y / e x y >-> e' x y} ->
  path e x s -> path e' (f x) (map f s).

Proof.

by move=> f_homo; rewrite path_map; apply: sub_path. Qed.

Lemma homo_cycle : {homo f : x y / e x y >-> e' x y} ->
  {homo map f : s / cycle e s >-> cycle e' s}.

Proof.

by move=> f_homo s hs; rewrite cycle_map (sub_cycle _ hs). Qed.

Lemma homo_sorted : {homo f : x y / e x y >-> e' x y} ->
  {homo map f : s / sorted e s >-> sorted e' s}.

Proof.

by move/homo_path => ? []. Qed.

Lemma mono_path x s : {mono f : x y / e x y >-> e' x y} ->
  path e' (f x) (map f s) = path e x s.

Proof.

by move=> f_mon; rewrite path_map; apply: eq_path. Qed.

Lemma mono_cycle : {mono f : x y / e x y >-> e' x y} ->
  {mono map f : s / cycle e s >-> cycle e' s}.

Proof.

by move=> ? ?; rewrite cycle_map; apply: eq_cycle. Qed.

Lemma mono_sorted : {mono f : x y / e x y >-> e' x y} ->
  {mono map f : s / sorted e s >-> sorted e' s}.

Proof.

by move=> f_mon [] //= x s; apply: mono_path. Qed.

End HomoPath.

Arguments path_map {T T' f e'}.
Arguments cycle_map {T T' f e'}.
Arguments sorted_map {T T' f e'}.
Arguments homo_path_in {T T' P f e e' x s}.
Arguments homo_cycle_in {T T' P f e e' s}.
Arguments homo_sorted_in {T T' P f e e' s}.
Arguments mono_path_in {T T' P f e e' x s}.
Arguments mono_cycle_in {T T' P f e e' s}.
Arguments mono_sorted_in {T T' P f e e' s}.
Arguments homo_path {T T' f e e' x s}.
Arguments homo_cycle {T T' f e e'}.
Arguments homo_sorted {T T' f e e'}.
Arguments mono_path {T T' f e e' x s}.
Arguments mono_cycle {T T' f e e'}.
Arguments mono_sorted {T T' f e e'}.

Section CycleAll2Rel.

Lemma cycle_all2rel (T : Type) (leT : rel T) :
  transitive leT -> forall s, cycle leT s = all2rel leT s.

Proof.

move=> leT_tr; elim=> //= x s IHs.
rewrite allrel_cons2 -{}IHs // (path_sortedE leT_tr) /= all_rcons -rev_sorted.
rewrite rev_rcons /= (path_sortedE (rev_trans leT_tr)) all_rev !andbA.
case: (boolP (leT x x && _ && _)) => //=.
case: s => //= y s /and3P[/and3P[_ xy _] yx sx].
rewrite rev_sorted rcons_path /= (leT_tr _ _ _ _ xy) ?andbT //.
by case: (lastP s) sx => //= {}s z; rewrite all_rcons last_rcons => /andP [->].
Qed.

Lemma cycle_all2rel_in (T : Type) (P : {pred T}) (leT : rel T) :
  {in P & &, transitive leT} ->
  forall s, all P s -> cycle leT s = all2rel leT s.

Proof.

move=> /in3_sig leT_tr _ /all_sigP [s ->].
by rewrite cycle_map allrel_mapl allrel_mapr; apply: cycle_all2rel.
Qed.

End CycleAll2Rel.

Section PreInSuffix.

Variables (T : eqType) (e : rel T).
Implicit Type s : seq T.

Local Notation path := (path e).
Local Notation sorted := (sorted e).

Lemma prefix_path x s1 s2 : prefix s1 s2 -> path x s2 -> path x s1.

Proof.

by rewrite prefixE => /eqP <-; exact: take_path. Qed.

Lemma prefix_sorted s1 s2 : prefix s1 s2 -> sorted s2 -> sorted s1.

Proof.

by rewrite prefixE => /eqP <-; exact: take_sorted. Qed.

Lemma infix_sorted s1 s2 : infix s1 s2 -> sorted s2 -> sorted s1.

Proof.

by rewrite infixE => /eqP <- ?; apply/take_sorted/drop_sorted. Qed.

Lemma suffix_sorted s1 s2 : suffix s1 s2 -> sorted s2 -> sorted s1.

Proof.

by rewrite suffixE => /eqP <-; exact: drop_sorted. Qed.

End PreInSuffix.

Section EqSorted.

Variables (T : eqType) (leT : rel T).
Implicit Type s : seq T.

Local Notation path := (path leT).
Local Notation sorted := (sorted leT).

Lemma subseq_path_in x s1 s2 :
  {in x :: s2 & &, transitive leT} -> subseq s1 s2 -> path x s2 -> path x s1.

Proof.

by move=> tr /subseqP [m _ ->]; apply/(path_mask_in tr). Qed.

Lemma subseq_sorted_in s1 s2 :
  {in s2 & &, transitive leT} -> subseq s1 s2 -> sorted s2 -> sorted s1.

Proof.

by move=> tr /subseqP [m _ ->]; apply/(sorted_mask_in tr). Qed.

Lemma sorted_ltn_index_in s : {in s & &, transitive leT} -> sorted s ->
  {in s &, forall x y, index x s < index y s -> leT x y}.

Proof.

case: s => // x0 s' leT_tr s_sorted x y xs ys.
move/(sorted_ltn_nth_in leT_tr x0 (allss (_ :: _)) s_sorted).
by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply.
Qed.

Lemma sorted_leq_index_in s :
  {in s & &, transitive leT} -> {in s, reflexive leT} -> sorted s ->
  {in s &, forall x y, index x s <= index y s -> leT x y}.

Proof.

case: s => // x0 s' leT_tr leT_refl s_sorted x y xs ys.
move/(sorted_leq_nth_in leT_tr leT_refl x0 (allss (_ :: _)) s_sorted).
by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply.
Qed.

Hypothesis leT_tr : transitive leT.

Lemma subseq_path x s1 s2 : subseq s1 s2 -> path x s2 -> path x s1.

Proof.

by apply: subseq_path_in; apply: in3W. Qed.

Lemma subseq_sorted s1 s2 : subseq s1 s2 -> sorted s2 -> sorted s1.

Proof.

by apply: subseq_sorted_in; apply: in3W. Qed.

Lemma sorted_uniq : irreflexive leT -> forall s, sorted s -> uniq s.

Proof.

by move=> irr s; rewrite sorted_pairwise //; apply/pairwise_uniq. Qed.

Lemma sorted_eq : antisymmetric leT ->
  forall s1 s2, sorted s1 -> sorted s2 -> perm_eq s1 s2 -> s1 = s2.

Proof.

by move=> leT_asym s1 s2; rewrite !sorted_pairwise //; apply: pairwise_eq.
Qed.

Lemma irr_sorted_eq : irreflexive leT ->
  forall s1 s2, sorted s1 -> sorted s2 -> s1 =i s2 -> s1 = s2.

Proof.

move=> leT_irr s1 s2 s1_sort s2_sort eq_s12.
have: antisymmetric leT.
  by move=> m n /andP[? ltnm]; case/idP: (leT_irr m); apply: leT_tr ltnm.
by move/sorted_eq; apply=> //; apply: uniq_perm => //; apply: sorted_uniq.
Qed.

Lemma sorted_ltn_index s :
  sorted s -> {in s &, forall x y, index x s < index y s -> leT x y}.

Proof.

case: s => // x0 s' s_sorted x y xs ys /(sorted_ltn_nth leT_tr x0 s_sorted).
by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply.
Qed.

Lemma undup_path x s : path x s -> path x (undup s).

Proof.

exact/subseq_path/undup_subseq. Qed.

Lemma undup_sorted s : sorted s -> sorted (undup s).

Proof.

exact/subseq_sorted/undup_subseq. Qed.

Hypothesis leT_refl : reflexive leT.

Lemma sorted_leq_index s :
  sorted s -> {in s &, forall x y, index x s <= index y s -> leT x y}.

Proof.

case: s => // x0 s' s_sorted x y xs ys.
move/(sorted_leq_nth leT_tr leT_refl x0 s_sorted).
by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply.
Qed.

End EqSorted.

Arguments sorted_ltn_index_in {T leT s} leT_tr s_sorted.
Arguments sorted_leq_index_in {T leT s} leT_tr leT_refl s_sorted.
Arguments sorted_ltn_index {T leT} leT_tr {s}.
Arguments sorted_leq_index {T leT} leT_tr leT_refl {s}.

Section EqSorted_in.

Variables (T : eqType) (leT : rel T).
Implicit Type s : seq T.

Lemma sorted_uniq_in s :
  {in s & &, transitive leT} -> {in s, irreflexive leT} ->
  sorted leT s -> uniq s.

Proof.

move=> /in3_sig leT_tr /in1_sig leT_irr; case/all_sigP: (allss s) => s' ->.
by rewrite sorted_map (map_inj_uniq val_inj); exact: sorted_uniq.
Qed.

Lemma sorted_eq_in s1 s2 :
  {in s1 & &, transitive leT} -> {in s1 &, antisymmetric leT} ->
  sorted leT s1 -> sorted leT s2 -> perm_eq s1 s2 -> s1 = s2.

Proof.

move=> /in3_sig leT_tr /in2_sig/(_ _ _ _)/val_inj leT_anti + + /[dup] s1s2.
have /all_sigP[s1' ->] := allss s1.
have /all_sigP[{s1s2}s2 ->] : all [in s1] s2 by rewrite -(perm_all _ s1s2).
by rewrite !sorted_map => ss1' ss2 /(perm_map_inj val_inj)/(sorted_eq leT_tr)->.
Qed.

Lemma irr_sorted_eq_in s1 s2 :
  {in s1 & &, transitive leT} -> {in s1, irreflexive leT} ->
  sorted leT s1 -> sorted leT s2 -> s1 =i s2 -> s1 = s2.

Proof.

move=> /in3_sig leT_tr /in1_sig leT_irr + + /[dup] s1s2.
have /all_sigP[s1' ->] := allss s1.
have /all_sigP[s2' ->] : all [in s1] s2 by rewrite -(eq_all_r s1s2).
rewrite !sorted_map => ss1' ss2' {}s1s2; congr map.
by apply: (irr_sorted_eq leT_tr) => // x; rewrite -!(mem_map val_inj).
Qed.

End EqSorted_in.

Section EqPath.

Variables (n0 : nat) (T : eqType) (e : rel T).
Implicit Type p : seq T.

Variant split x : seq T -> seq T -> seq T -> Type :=
  Split p1 p2 : split x (rcons p1 x ++ p2) p1 p2.

Lemma splitP p x (i := index x p) :
  x \in p -> split x p (take i p) (drop i.+1 p).

Proof.

by rewrite -has_pred1 => /split_find[? ? ? /eqP->]; constructor. Qed.

Variant splitl x1 x : seq T -> Type :=
  Splitl p1 p2 of last x1 p1 = x : splitl x1 x (p1 ++ p2).

Lemma splitPl x1 p x : x \in x1 :: p -> splitl x1 x p.

Proof.

rewrite inE; case: eqP => [->| _ /splitP[]]; first by rewrite -(cat0s p).
by split; apply: last_rcons.
Qed.

Variant splitr x : seq T -> Type :=
  Splitr p1 p2 : splitr x (p1 ++ x :: p2).

Lemma splitPr p x : x \in p -> splitr x p.

Proof.

by case/splitP=> p1 p2; rewrite cat_rcons. Qed.

Fixpoint next_at x y0 y p :=
  match p with
  | [::] => if x == y then y0 else x
  | y' :: p' => if x == y then y' else next_at x y0 y' p'
  end.

Definition next p x := if p is y :: p' then next_at x y y p' else x.

Fixpoint prev_at x y0 y p :=
  match p with
  | [::] => if x == y0 then y else x
  | y' :: p' => if x == y' then y else prev_at x y0 y' p'
  end.

Definition prev p x := if p is y :: p' then prev_at x y y p' else x.

Lemma next_nth p x :
  next p x = if x \in p then
               if p is y :: p' then nth y p' (index x p) else x
             else x.

Proof.

case: p => //= y0 p.
elim: p {2 3 5}y0 => [|y' p IHp] y /=; rewrite (eq_sym y) inE;
  by case: ifP => // _; apply: IHp.
Qed.

Lemma prev_nth p x :
  prev p x = if x \in p then
               if p is y :: p' then nth y p (index x p') else x
             else x.

Proof.

case: p => //= y0 p; rewrite inE orbC.
elim: p {2 5}y0 => [|y' p IHp] y; rewrite /= ?inE // (eq_sym y').
by case: ifP => // _; apply: IHp.
Qed.

Lemma mem_next p x : (next p x \in p) = (x \in p).

Proof.

rewrite next_nth; case p_x: (x \in p) => //.
case: p (index x p) p_x => [|y0 p'] //= i _; rewrite inE.
have [lt_ip | ge_ip] := ltnP i (size p'); first by rewrite orbC mem_nth.
by rewrite nth_default ?eqxx.
Qed.

Lemma mem_prev p x : (prev p x \in p) = (x \in p).

Proof.

rewrite prev_nth; case p_x: (x \in p) => //; case: p => [|y0 p] // in p_x *.
by apply mem_nth; rewrite /= ltnS index_size.
Qed.

Definition ucycleb p := cycle e p && uniq p.
Definition ucycle p : Prop := cycle e p && uniq p.

Lemma ucycle_cycle p : ucycle p -> cycle e p.

Proof.

by case/andP. Qed.

Lemma ucycle_uniq p : ucycle p -> uniq p.

Proof.

by case/andP. Qed.

Lemma next_cycle p x : cycle e p -> x \in p -> e x (next p x).

Proof.

case: p => //= y0 p; elim: p {1 3 5}y0 => [|z p IHp] y /=; rewrite inE.
  by rewrite andbT; case: (x =P y) => // ->.
by case/andP=> eyz /IHp; case: (x =P y) => // ->.
Qed.

Lemma prev_cycle p x : cycle e p -> x \in p -> e (prev p x) x.

Proof.

case: p => //= y0 p; rewrite inE orbC.
elim: p {1 5}y0 => [|z p IHp] y /=; rewrite ?inE.
  by rewrite andbT; case: (x =P y0) => // ->.
by case/andP=> eyz /IHp; case: (x =P z) => // ->.
Qed.

Lemma rot_ucycle p : ucycle (rot n0 p) = ucycle p.

Proof.

by rewrite /ucycle rot_uniq rot_cycle. Qed.

Lemma rotr_ucycle p : ucycle (rotr n0 p) = ucycle p.

Proof.

by rewrite /ucycle rotr_uniq rotr_cycle. Qed.

Definition mem2 p x y := y \in drop (index x p) p.

Lemma mem2l p x y : mem2 p x y -> x \in p.

Proof.

by rewrite /mem2 -!index_mem size_drop ltn_subRL; apply/leq_ltn_trans/leq_addr.
Qed.

Lemma mem2lf {p x y} : x \notin p -> mem2 p x y = false.

Proof.

exact/contraNF/mem2l. Qed.

Lemma mem2r p x y : mem2 p x y -> y \in p.

Proof.

by rewrite -[in y \in p](cat_take_drop (index x p) p) mem_cat orbC /mem2 => ->.
Qed.

Lemma mem2rf {p x y} : y \notin p -> mem2 p x y = false.

Proof.

exact/contraNF/mem2r. Qed.

Lemma mem2_cat p1 p2 x y :
  mem2 (p1 ++ p2) x y = mem2 p1 x y || mem2 p2 x y || (x \in p1) && (y \in p2).

Proof.

rewrite [LHS]/mem2 index_cat fun_if if_arg !drop_cat addKn.
case: ifPn => [p1x | /mem2lf->]; last by rewrite ltnNge leq_addr orbF.
by rewrite index_mem p1x mem_cat -orbA (orb_idl (@mem2r _ _ _)).
Qed.

Lemma mem2_splice p1 p3 x y p2 :
  mem2 (p1 ++ p3) x y -> mem2 (p1 ++ p2 ++ p3) x y.

Proof.

by rewrite !mem2_cat mem_cat andb_orr orbC => /or3P[]->; rewrite ?orbT.
Qed.

Lemma mem2_splice1 p1 p3 x y z :
  mem2 (p1 ++ p3) x y -> mem2 (p1 ++ z :: p3) x y.

Proof.

exact: mem2_splice [::z]. Qed.

Lemma mem2_cons x p y z :
  mem2 (x :: p) y z = (if x == y then z \in x :: p else mem2 p y z).

Proof.

by rewrite [LHS]/mem2 /=; case: ifP. Qed.

Lemma mem2_seq1 x y z : mem2 [:: x] y z = (y == x) && (z == x).

Proof.

by rewrite mem2_cons eq_sym inE. Qed.

Lemma mem2_last y0 p x : mem2 p x (last y0 p) = (x \in p).

Proof.

apply/idP/idP; first exact: mem2l; rewrite -index_mem /mem2 => p_x.
by rewrite -nth_last -(subnKC p_x) -nth_drop mem_nth // size_drop subnSK.
Qed.

Lemma mem2l_cat {p1 p2 x} : x \notin p1 -> mem2 (p1 ++ p2) x =1 mem2 p2 x.

Proof.

by move=> p1'x y; rewrite mem2_cat (negPf p1'x) mem2lf ?orbF. Qed.

Lemma mem2r_cat {p1 p2 x y} : y \notin p2 -> mem2 (p1 ++ p2) x y = mem2 p1 x y.

Proof.

by move=> p2'y; rewrite mem2_cat (negPf p2'y) -orbA orbC andbF mem2rf.
Qed.

Lemma mem2lr_splice {p1 p2 p3 x y} :
  x \notin p2 -> y \notin p2 -> mem2 (p1 ++ p2 ++ p3) x y = mem2 (p1 ++ p3) x y.

Proof.

move=> p2'x p2'y; rewrite catA !mem2_cat !mem_cat.
by rewrite (negPf p2'x) (negPf p2'y) (mem2lf p2'x) andbF !orbF.
Qed.

Lemma mem2E s x y :
  mem2 s x y = subseq (if x == y then [:: x] else [:: x; y]) s.

Proof.

elim: s => [| h s]; first by case: ifP.
rewrite mem2_cons => ->.
do 2 rewrite inE (fun_if subseq) !if_arg !sub1seq /=.
by have [->|] := eqVneq; case: eqVneq.
Qed.

Variant split2r x y : seq T -> Type :=
  Split2r p1 p2 of y \in x :: p2 : split2r x y (p1 ++ x :: p2).

Lemma splitP2r p x y : mem2 p x y -> split2r x y p.

Proof.

move=> pxy; have px := mem2l pxy.
have:= pxy; rewrite /mem2 (drop_nth x) ?index_mem ?nth_index //.
by case/splitP: px => p1 p2; rewrite cat_rcons.
Qed.

Fixpoint shorten x p :=
  if p is y :: p' then
    if x \in p then shorten x p' else y :: shorten y p'
  else [::].

Variant shorten_spec x p : T -> seq T -> Type :=
   ShortenSpec p' of path e x p' & uniq (x :: p') & {subset p' <= p} :
     shorten_spec x p (last x p') p'.

Lemma shortenP x p : path e x p -> shorten_spec x p (last x p) (shorten x p).

Proof.

move=> e_p; have: x \in x :: p by apply: mem_head.
elim: p x {1 3 5}x e_p => [|y2 p IHp] x y1.
  by rewrite mem_seq1 => _ /eqP->.
rewrite inE orbC /= => /andP[ey12 {}/IHp IHp].
case: ifPn => [y2p_x _ | not_y2p_x /eqP def_x].
  have [p' e_p' Up' p'p] := IHp _ y2p_x.
  by split=> // y /p'p; apply: predU1r.
have [p' e_p' Up' p'p] := IHp y2 (mem_head y2 p).
have{} p'p z: z \in y2 :: p' -> z \in y2 :: p.
  by rewrite !inE; case: (z == y2) => // /p'p.
rewrite -(last_cons y1) def_x; split=> //=; first by rewrite ey12.
by rewrite (contra (p'p y1)) -?def_x.
Qed.

End EqPath.


Section SortSeq.

Variables (T : Type) (leT : rel T).

Fixpoint merge s1 :=
  if s1 is x1 :: s1' then
    let fix merge_s1 s2 :=
      if s2 is x2 :: s2' then
        if leT x1 x2 then x1 :: merge s1' s2 else x2 :: merge_s1 s2'
      else s1 in
    merge_s1
  else id.

Arguments merge !s1 !s2 : rename.

Fixpoint merge_sort_push s1 ss :=
  match ss with
  | [::] :: ss' | [::] as ss' => s1 :: ss'
  | s2 :: ss' => [::] :: merge_sort_push (merge s2 s1) ss'
  end.

Fixpoint merge_sort_pop s1 ss :=
  if ss is s2 :: ss' then merge_sort_pop (merge s2 s1) ss' else s1.

Fixpoint merge_sort_rec ss s :=
  if s is [:: x1, x2 & s'] then
    let s1 := if leT x1 x2 then [:: x1; x2] else [:: x2; x1] in
    merge_sort_rec (merge_sort_push s1 ss) s'
  else merge_sort_pop s ss.

Definition sort := merge_sort_rec [::].

Fixpoint sort_rec1 ss s :=
  if s is x :: s then sort_rec1 (merge_sort_push [:: x] ss) s else
  merge_sort_pop [::] ss.

Lemma sortE s : sort s = sort_rec1 [::] s.

Proof.

transitivity (sort_rec1 [:: nil] s); last by case: s.
rewrite /sort; move: [::] {2}_.+1 (ltnSn (size s)./2) => ss n.
by elim: n => // n IHn in ss s *; case: s => [|x [|y s]] //= /IHn->.
Qed.

Lemma count_merge (p : pred T) s1 s2 :
  count p (merge s1 s2) = count p (s1 ++ s2).

Proof.

rewrite count_cat; elim: s1 s2 => // x s1 IH1.
elim=> //= [|y s2 IH2]; first by rewrite addn0.
by case: leT; rewrite /= ?IH1 ?IH2 !addnA [_ + p y]addnAC [p x + p y]addnC.
Qed.

Lemma size_merge s1 s2 : size (merge s1 s2) = size (s1 ++ s2).

Proof.

exact: (count_merge predT). Qed.

Lemma allrel_merge s1 s2 : allrel leT s1 s2 -> merge s1 s2 = s1 ++ s2.

Proof.

elim: s1 s2 => [|x s1 IHs1] [|y s2]; rewrite ?cats0 //=.
by rewrite allrel_consl /= -andbA => /and3P [-> _ /IHs1->].
Qed.

Lemma count_sort (p : pred T) s : count p (sort s) = count p s.

Proof.

rewrite sortE -[RHS]/(sumn [seq count p x | x <- [::]] + count p s).
elim: s [::] => [|x s ihs] ss.
  rewrite [LHS]/=; elim: ss [::] => //= s ss ihss t.
  by rewrite ihss count_merge count_cat addnCA addnA.
rewrite {}ihs -[in RHS]cat1s count_cat addnA; congr addn; rewrite addnC.
elim: {x s} ss [:: x] => [|[|x s] ss ihss] t //.
by rewrite [LHS]/= add0n ihss count_merge count_cat -addnA addnCA.
Qed.

Lemma pairwise_sort s : pairwise leT s -> sort s = s.

Proof.

pose catss := foldr (fun x => cat ^~ x) (Nil T).
rewrite -{1 3}[s]/(catss [::] ++ s) sortE; elim: s [::] => /= [|x s ihs] ss.
  elim: ss [::] => //= s ss ihss t; rewrite -catA => ssst.
  rewrite -ihss ?allrel_merge //; move: ssst; rewrite !pairwise_cat.
  by case/and4P.
rewrite (catA _ [:: _]) => ssxs.
suff x_ss_E: catss (merge_sort_push [:: x] ss) = catss ([:: x] :: ss).
  by rewrite -[catss _ ++ _]/(catss ([:: x] :: ss)) -x_ss_E ihs // x_ss_E.
move: ssxs; rewrite pairwise_cat => /and3P [_ + _].
elim: ss [:: x] => {x s ihs} //= -[|x s] ss ihss t h_pairwise;
  rewrite /= cats0 // allrel_merge ?ihss ?catA //.
by move: h_pairwise; rewrite -catA !pairwise_cat => /and4P [].
Qed.

Remark size_merge_sort_push s1 :
  let graded ss := forall i, size (nth [::] ss i) \in pred2 0 (2 ^ (i + 1)) in
  size s1 = 2 -> {homo merge_sort_push s1 : ss / graded ss}.

Proof.

set n := {2}1; rewrite -[RHS]/(2 ^ n) => graded sz_s1 ss.
elim: ss => [|s2 ss IHss] in (n) graded s1 sz_s1 * => sz_ss i //=.
  by case: i => [|[]] //; rewrite sz_s1 inE eqxx orbT.
case: s2 i => [|x s2] [|i] //= in sz_ss *; first by rewrite sz_s1 inE eqxx orbT.
  exact: (sz_ss i.+1).
rewrite addSnnS; apply: IHss i => [|i]; last by rewrite -addSnnS (sz_ss i.+1).
by rewrite size_merge size_cat sz_s1 (eqP (sz_ss 0)) addnn expnS mul2n.
Qed.

Section Stability.

Variable leT' : rel T.
Hypothesis (leT_total : total leT) (leT'_tr : transitive leT').

Let leT_lex := [rel x y | leT x y && (leT y x ==> leT' x y)].

Lemma merge_stable_path x s1 s2 :
  allrel leT' s1 s2 -> path leT_lex x s1 -> path leT_lex x s2 ->
  path leT_lex x (merge s1 s2).

Proof.

elim: s1 s2 x => //= x s1 ih1; elim => //= y s2 ih2 h.
rewrite allrel_cons2 => /and4P [xy' xs2 ys1 s1s2] /andP [hx xs1] /andP [hy ys2].
case: ifP => xy /=; rewrite (hx, hy) /=.
- by apply: ih1; rewrite ?allrel_consr ?ys1 //= xy xy' implybT.
- by apply: ih2; have:= leT_total x y; rewrite ?allrel_consl ?xs2 ?xy //= => ->.
Qed.

Lemma merge_stable_sorted s1 s2 :
  allrel leT' s1 s2 -> sorted leT_lex s1 -> sorted leT_lex s2 ->
  sorted leT_lex (merge s1 s2).

Proof.

case: s1 s2 => [|x s1] [|y s2] //=; rewrite allrel_consl allrel_consr /= -andbA.
case/and4P => [xy' xs2 ys1 s1s2] xs1 ys2; rewrite -/(merge (_ :: _)).
by case: ifP (leT_total x y) => /= xy yx; apply/merge_stable_path;
  rewrite /= ?(allrel_consl, allrel_consr, xs2, ys1, xy, yx, xy', implybT).
Qed.

End Stability.

Hypothesis leT_total : total leT.

Let leElex : leT =2 [rel x y | leT x y && (leT y x ==> true)].

Proof.

by move=> ? ? /=; rewrite implybT andbT. Qed.

Lemma merge_path x s1 s2 :
  path leT x s1 -> path leT x s2 -> path leT x (merge s1 s2).

Proof.

by rewrite !(eq_path leElex); apply/merge_stable_path/allrelT. Qed.

Lemma merge_sorted s1 s2 :
  sorted leT s1 -> sorted leT s2 -> sorted leT (merge s1 s2).

Proof.

by rewrite !(eq_sorted leElex); apply/merge_stable_sorted/allrelT. Qed.

Hypothesis leT_tr : transitive leT.

Lemma sorted_merge s t : sorted leT (s ++ t) -> merge s t = s ++ t.

Proof.

by rewrite sorted_pairwise // pairwise_cat => /and3P[/allrel_merge]. Qed.

Lemma sorted_sort s : sorted leT s -> sort s = s.

Proof.

by rewrite sorted_pairwise //; apply/pairwise_sort. Qed.

Lemma mergeA : associative merge.

Proof.

elim=> // x xs IHxs; elim=> // y ys IHys; elim=> [|z zs IHzs] /=.
  by case: ifP.
case: ifP; case: ifP => /= lexy leyz.
- by rewrite lexy (leT_tr lexy leyz) -IHxs /= leyz.
- by rewrite lexy leyz -IHys.
- case: ifP => lexz; first by rewrite -IHxs //= leyz.
  by rewrite -!/(merge (_ :: _)) IHzs /= lexy.
- suff->: leT x z = false by rewrite leyz // -!/(merge (_ :: _)) IHzs /= lexy.
  by apply/contraFF/leT_tr: leyz; have := leT_total x y; rewrite lexy.
Qed.

End SortSeq.

Arguments merge {T} relT !s1 !s2 : rename.
Arguments size_merge {T} leT s1 s2.
Arguments allrel_merge {T leT s1 s2}.
Arguments pairwise_sort {T leT s}.
Arguments merge_path {T leT} leT_total {x s1 s2}.
Arguments merge_sorted {T leT} leT_total {s1 s2}.
Arguments sorted_merge {T leT} leT_tr {s t}.
Arguments sorted_sort {T leT} leT_tr {s}.
Arguments mergeA {T leT} leT_total leT_tr.

Section SortMap.
Variables (T T' : Type) (f : T' -> T).

Section Monotonicity.

Variables (leT' : rel T') (leT : rel T).
Hypothesis f_mono : {mono f : x y / leT' x y >-> leT x y}.

Lemma map_merge : {morph map f : s1 s2 / merge leT' s1 s2 >-> merge leT s1 s2}.

Proof.

elim=> //= x s1 IHs1; elim => [|y s2 IHs2] //=; rewrite f_mono.
by case: leT'; rewrite /= ?IHs1 ?IHs2.
Qed.

Lemma map_sort : {morph map f : s1 / sort leT' s1 >-> sort leT s1}.

Proof.

move=> s; rewrite !sortE -[[::] in RHS]/(map (map f) [::]).
elim: s [::] => /= [|x s ihs] ss; rewrite -/(map f [::]) -/(map f [:: _]);
  first by elim: ss [::] => //= x ss ihss ?; rewrite ihss map_merge.
rewrite ihs -/(map f [:: x]); congr sort_rec1.
by elim: ss [:: x] => {x s ihs} [|[|x s] ss ihss] //= ?; rewrite ihss map_merge.
Qed.

End Monotonicity.

Variable leT : rel T.

Lemma merge_map s1 s2 :
  merge leT (map f s1) (map f s2) = map f (merge (relpre f leT) s1 s2).

Proof.

exact/esym/map_merge. Qed.

Lemma sort_map s : sort leT (map f s) = map f (sort (relpre f leT) s).

Proof.

exact/esym/map_sort. Qed.

End SortMap.

Arguments map_merge {T T' f leT' leT}.
Arguments map_sort {T T' f leT' leT}.
Arguments merge_map {T T' f leT}.
Arguments sort_map {T T' f leT}.

Lemma sorted_sort_in T (P : {pred T}) (leT : rel T) :
  {in P & &, transitive leT} ->
  forall s : seq T, all P s -> sorted leT s -> sort leT s = s.

Proof.

move=> /in3_sig ? _ /all_sigP[s ->].
by rewrite sort_map sorted_map => /sorted_sort->.
Qed.

Arguments sorted_sort_in {T P leT} leT_tr {s}.

Section EqSortSeq.

Variables (T : eqType) (leT : rel T).

Lemma perm_merge s1 s2 : perm_eql (merge leT s1 s2) (s1 ++ s2).

Proof.

by apply/permPl/permP => ?; rewrite count_merge. Qed.

Lemma mem_merge s1 s2 : merge leT s1 s2 =i s1 ++ s2.

Proof.

by apply: perm_mem; rewrite perm_merge. Qed.

Lemma merge_uniq s1 s2 : uniq (merge leT s1 s2) = uniq (s1 ++ s2).

Proof.

by apply: perm_uniq; rewrite perm_merge. Qed.

Lemma perm_sort s : perm_eql (sort leT s) s.

Proof.

by apply/permPl/permP => ?; rewrite count_sort. Qed.

Lemma mem_sort s : sort leT s =i s

Proof.

exact/perm_mem/permPl/perm_sort. Qed.

Lemma sort_uniq s : uniq (sort leT s) = uniq s.

Proof.

exact/perm_uniq/permPl/perm_sort. Qed.

Lemma eq_count_merge (p : pred T) s1 s1' s2 s2' :
  count p s1 = count p s1' -> count p s2 = count p s2' ->
  count p (merge leT s1 s2) = count p (merge leT s1' s2').

Proof.

by rewrite !count_merge !count_cat => -> ->. Qed.

End EqSortSeq.

Lemma perm_iota_sort (T : Type) (leT : rel T) x0 s :
  {i_s : seq nat | perm_eq i_s (iota 0 (size s)) &
                   sort leT s = map (nth x0 s) i_s}.

Proof.

exists (sort (relpre (nth x0 s) leT) (iota 0 (size s))).
  by rewrite perm_sort.
by rewrite -[s in LHS](mkseq_nth x0) sort_map.
Qed.

Lemma all_merge (T : Type) (P : {pred T}) (leT : rel T) s1 s2 :
  all P (merge leT s1 s2) = all P s1 && all P s2.

Proof.

elim: s1 s2 => //= x s1 IHs1; elim=> [|y s2 IHs2]; rewrite ?andbT //=.
by case: ifP => _; rewrite /= ?IHs1 ?IHs2 //=; bool_congr.
Qed.

Lemma all_sort (T : Type) (P : {pred T}) (leT : rel T) s :
  all P (sort leT s) = all P s.

Proof.

case: s => // x s; move: (x :: s) => {}s.
by rewrite -(mkseq_nth x s) sort_map !all_map; apply/perm_all/permPl/perm_sort.
Qed.

Lemma size_sort (T : Type) (leT : rel T) s : size (sort leT s) = size s.

Proof.

exact: (count_sort _ predT). Qed.

Lemma ltn_sorted_uniq_leq s : sorted ltn s = uniq s && sorted leq s.

Proof.

rewrite (sorted_pairwise leq_trans) (sorted_pairwise ltn_trans) uniq_pairwise.
by rewrite -pairwise_relI; apply/eq_pairwise => ? ?; rewrite ltn_neqAle.
Qed.

Lemma gtn_sorted_uniq_geq s : sorted gtn s = uniq s && sorted geq s.

Proof.

by rewrite -rev_sorted ltn_sorted_uniq_leq rev_sorted rev_uniq. Qed.

Lemma iota_sorted i n : sorted leq (iota i n).

Proof.

by elim: n i => // [[|n] //= IHn] i; rewrite IHn leqW. Qed.

Lemma iota_ltn_sorted i n : sorted ltn (iota i n).

Proof.

by rewrite ltn_sorted_uniq_leq iota_sorted iota_uniq. Qed.

Section Stability_iota.

Variables (leN : rel nat) (leN_total : total leN).

Let lt_lex := [rel n m | leN n m && (leN m n ==> (n < m))].

Let Fixpoint push_invariant (ss : seq (seq nat)) :=
  if ss is s :: ss' then
    [&& sorted lt_lex s, allrel gtn s (flatten ss') & push_invariant ss']
  else
    true.

Let push_stable s1 ss :
  push_invariant (s1 :: ss) -> push_invariant (merge_sort_push leN s1 ss).

Proof.

elim: ss s1 => [] // [] //= m s2 ss ihss s1; rewrite -cat_cons allrel_catr.
move=> /and5P[sorted_s1 /andP[s1s2 s1ss] sorted_s2 s2ss hss]; apply: ihss.
rewrite /= hss andbT merge_stable_sorted //=; first by rewrite allrelC.
by apply/allrelP => ? ?; rewrite mem_merge mem_cat => /orP[]; apply/allrelP.
Qed.

Let pop_stable s1 ss :
  push_invariant (s1 :: ss) -> sorted lt_lex (merge_sort_pop leN s1 ss).

Proof.

elim: ss s1 => [s1 /and3P[]|s2 ss ihss s1] //=; rewrite allrel_catr.
move=> /and5P[sorted_s1 /andP[s1s2 s1ss] sorted_s2 s2ss hss]; apply: ihss.
rewrite /= hss andbT merge_stable_sorted //=; first by rewrite allrelC.
by apply/allrelP => ? ?; rewrite mem_merge mem_cat => /orP[]; apply/allrelP.
Qed.

Lemma sort_iota_stable n : sorted lt_lex (sort leN (iota 0 n)).

Proof.

rewrite sortE.
have/andP[]: all (gtn 0) (flatten [::]) && push_invariant [::] by [].
elim: n 0 [::] => [|n ihn] m ss hss1 hss2; first exact: pop_stable.
apply/ihn/push_stable; last by rewrite /= allrel1l hss1.
have: all (gtn m.+1) (flatten ([:: m] :: ss)).
  by rewrite /= leqnn; apply: sub_all hss1 => ? /leqW.
elim: ss [:: _] {hss1 hss2} => [|[|? ?] ? ihss] //= ? ?.
by rewrite ihss //= all_cat all_merge -andbA andbCA -!all_cat.
Qed.

End Stability_iota.

Lemma sort_pairwise_stable T (leT leT' : rel T) :
  total leT -> forall s : seq T, pairwise leT' s ->
  sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s).

Proof.

move=> leT_total s pairwise_s; case Ds: s => // [x s1].
rewrite -{s1}Ds -(mkseq_nth x s) sort_map.
apply/homo_sorted_in/sort_iota_stable/(fun _ _ => leT_total _ _)/allss => y z.
rewrite !mem_sort !mem_iota !leq0n add0n /= => ys zs /andP [->] /=.
by case: (leT _ _); first apply: pairwiseP.
Qed.

Lemma sort_stable T (leT leT' : rel T) :
  total leT -> transitive leT' -> forall s : seq T, sorted leT' s ->
  sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s).

Proof.

move=> leT_total leT'_tr s; rewrite sorted_pairwise //.
exact: sort_pairwise_stable.
Qed.

Lemma sort_stable_in T (P : {pred T}) (leT leT' : rel T) :
  {in P &, total leT} -> {in P & &, transitive leT'} ->
  forall s : seq T, all P s -> sorted leT' s ->
  sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s).

Proof.

move=> /in2_sig leT_total /in3_sig leT_tr _ /all_sigP[s ->].
by rewrite sort_map !sorted_map; apply: sort_stable.
Qed.

Lemma filter_sort T (leT : rel T) :
  total leT -> transitive leT ->
  forall p s, filter p (sort leT s) = sort leT (filter p s).

Proof.

move=> leT_total leT_tr p s; case Ds: s => // [x s1].
pose leN := relpre (nth x s) leT.
pose lt_lex := [rel n m | leN n m && (leN m n ==> (n < m))].
have lt_lex_tr: transitive lt_lex.
  rewrite /lt_lex /leN => ? ? ? /= /andP [xy xy'] /andP [yz yz'].
  rewrite (leT_tr _ _ _ xy yz); apply/implyP => zx; move: xy' yz'.
  by rewrite (leT_tr _ _ _ yz zx) (leT_tr _ _ _ zx xy); apply: ltn_trans.
rewrite -{s1}Ds -(mkseq_nth x s) !(filter_map, sort_map); congr map.
apply/(@irr_sorted_eq _ lt_lex); rewrite /lt_lex /leN //=.
- by move=> ?; rewrite /= ltnn implybF andbN.
- exact/sorted_filter/sort_iota_stable.
- exact/sort_stable/sorted_filter/iota_ltn_sorted/ltn_trans/ltn_trans.
- by move=> ?; rewrite !(mem_filter, mem_sort).
Qed.

Lemma filter_sort_in T (P : {pred T}) (leT : rel T) :
  {in P &, total leT} -> {in P & &, transitive leT} ->
  forall p s, all P s -> filter p (sort leT s) = sort leT (filter p s).

Proof.

move=> /in2_sig leT_total /in3_sig leT_tr p _ /all_sigP[s ->].
by rewrite !(sort_map, filter_map) filter_sort.
Qed.

Section Stability_mask.

Variables (T : Type) (leT : rel T).
Variables (leT_total : total leT) (leT_tr : transitive leT).

Lemma mask_sort s m :
  {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}.

Proof.

case Ds: {-}s => [|x s1]; [by rewrite Ds; case: m; exists [::] | clear s1 Ds].
rewrite -(mkseq_nth x s) -map_mask !sort_map.
exists [seq i \in mask m (iota 0 (size s)) |
            i <- sort (xrelpre (nth x s) leT) (iota 0 (size s))].
rewrite -map_mask -filter_mask [in RHS]mask_filter ?iota_uniq ?filter_sort //.
by move=> ? ? ?; exact: leT_tr.
Qed.

Lemma sorted_mask_sort s m :
  sorted leT (mask m s) -> {m_s | mask m_s (sort leT s) = mask m s}.

Proof.

by move/(sorted_sort leT_tr) <-; exact: mask_sort. Qed.

End Stability_mask.

Section Stability_mask_in.

Variables (T : Type) (P : {pred T}) (leT : rel T).
Hypothesis leT_total : {in P &, total leT}.
Hypothesis leT_tr : {in P & &, transitive leT}.

Let le_sT := relpre (val : sig P -> _) leT.
Let le_sT_total : total le_sT := in2_sig leT_total.
Let le_sT_tr : transitive le_sT := in3_sig leT_tr.

Lemma mask_sort_in s m :
  all P s -> {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}.

Proof.

move=> /all_sigP [{}s ->]; case: (mask_sort (leT := le_sT) _ _ s m) => //.
by move=> m' m'E; exists m'; rewrite -map_mask !sort_map -map_mask m'E.
Qed.

Lemma sorted_mask_sort_in s m :
  all P s -> sorted leT (mask m s) -> {m_s | mask m_s (sort leT s) = mask m s}.

Proof.

move=> ? /(sorted_sort_in leT_tr _) <-; [exact: all_mask | exact: mask_sort_in].
Qed.

End Stability_mask_in.

Section Stability_subseq.

Variables (T : eqType) (leT : rel T).
Variables (leT_total : total leT) (leT_tr : transitive leT).

Lemma subseq_sort : {homo sort leT : t s / subseq t s}.

Proof.

move=> _ s /subseqP [m _ ->]; have [m' <-] := mask_sort leT_total leT_tr s m.
exact: mask_subseq.
Qed.

Lemma sorted_subseq_sort t s :
  subseq t s -> sorted leT t -> subseq t (sort leT s).

Proof.

by move=> subseq_ts /(sorted_sort leT_tr) <-; exact: subseq_sort. Qed.

Lemma mem2_sort s x y : leT x y -> mem2 s x y -> mem2 (sort leT s) x y.

Proof.

move=> lexy /[!mem2E] /subseq_sort.
by case: eqP => // _; rewrite {1}/sort /= lexy /=.
Qed.

End Stability_subseq.

Section Stability_subseq_in.

Variables (T : eqType) (leT : rel T).

Lemma subseq_sort_in t s :
  {in s &, total leT} -> {in s & &, transitive leT} ->
  subseq t s -> subseq (sort leT t) (sort leT s).

Proof.

move=> leT_total leT_tr /subseqP [m _ ->].
have [m' <-] := mask_sort_in leT_total leT_tr m (allss _).
exact: mask_subseq.
Qed.

Lemma sorted_subseq_sort_in t s :
  {in s &, total leT} -> {in s & &, transitive leT} ->
  subseq t s -> sorted leT t -> subseq t (sort leT s).

Proof.

move=> ? leT_tr ? /(sorted_sort_in leT_tr) <-; first exact/allP/mem_subseq.
exact: subseq_sort_in.
Qed.

Lemma mem2_sort_in s :
  {in s &, total leT} -> {in s & &, transitive leT} ->
  forall x y, leT x y -> mem2 s x y -> mem2 (sort leT s) x y.

Proof.

move=> leT_total leT_tr x y lexy; rewrite !mem2E.
by move/subseq_sort_in; case: (_ == _); rewrite /sort /= ?lexy; apply.
Qed.

End Stability_subseq_in.

Lemma sort_sorted T (leT : rel T) :
  total leT -> forall s, sorted leT (sort leT s).

Proof.

move=> leT_total s; apply/sub_sorted/sort_stable => //= [? ? /andP[] //|].
by case: s => // x s; elim: s x => /=.
Qed.

Lemma sort_sorted_in T (P : {pred T}) (leT : rel T) :
  {in P &, total leT} -> forall s : seq T, all P s -> sorted leT (sort leT s).

Proof.

by move=> /in2_sig ? _ /all_sigP[s ->]; rewrite sort_map sorted_map sort_sorted.
Qed.

Arguments sort_sorted {T leT} leT_total s.
Arguments sort_sorted_in {T P leT} leT_total {s}.

Lemma perm_sortP (T : eqType) (leT : rel T) :
  total leT -> transitive leT -> antisymmetric leT ->
  forall s1 s2, reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2).

Proof.

move=> leT_total leT_tr leT_asym s1 s2.
apply: (iffP idP) => eq12; last by rewrite -(perm_sort leT) eq12 perm_sort.
apply: (sorted_eq leT_tr leT_asym); rewrite ?sort_sorted //.
by rewrite perm_sort (permPl eq12) -(perm_sort leT).
Qed.

Lemma perm_sort_inP (T : eqType) (leT : rel T) (s1 s2 : seq T) :
  {in s1 &, total leT} -> {in s1 & &, transitive leT} ->
  {in s1 &, antisymmetric leT} ->
  reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2).

Proof.

move=> /in2_sig leT_total /in3_sig leT_tr /in2_sig/(_ _ _ _)/val_inj leT_asym.
apply: (iffP idP) => s1s2; last by rewrite -(perm_sort leT) s1s2 perm_sort.
move: (s1s2); have /all_sigP[s1' ->] := allss s1.
have /all_sigP[{s1s2}s2 ->] : all [in s1] s2 by rewrite -(perm_all _ s1s2).
by rewrite !sort_map => /(perm_map_inj val_inj) /(perm_sortP leT_total)->.
Qed.

Lemma homo_sort_map (T : Type) (T' : eqType) (f : T -> T') leT leT' :
  antisymmetric (relpre f leT') -> transitive (relpre f leT') -> total leT ->
  {homo f : x y / leT x y >-> leT' x y} ->
  forall s : seq T, sort leT' (map f s) = map f (sort leT s).

Proof.

move=> leT'_asym leT'_trans leT_total f_homo s; case Ds: s => // [x s'].
rewrite -{}Ds -(mkseq_nth x s) [in RHS]sort_map -!map_comp /comp.
apply: (@sorted_eq_in _ leT') => [? ? ?|? ?|||]; rewrite ?mem_sort.
- by move=> /mapP[? _ ->] /mapP[? _ ->] /mapP[? _ ->]; apply/leT'_trans.
- by move=> /mapP[? _ ->] /mapP[? _ ->] /leT'_asym ->.
- apply: (sort_sorted_in _ (allss _)) => _ _ /mapP[y _ ->] /mapP[z _ ->].
  by case/orP: (leT_total (nth x s y) (nth x s z)) => /f_homo ->; rewrite ?orbT.
- by rewrite map_comp -sort_map; exact/homo_sorted/sort_sorted.
- by rewrite perm_sort perm_map // perm_sym perm_sort.
Qed.

Lemma homo_sort_map_in
      (T : Type) (T' : eqType) (P : {pred T}) (f : T -> T') leT leT' :
  {in P &, antisymmetric (relpre f leT')} ->
  {in P & &, transitive (relpre f leT')} -> {in P &, total leT} ->
  {in P &, {homo f : x y / leT x y >-> leT' x y}} ->
  forall s : seq T, all P s ->
        sort leT' [seq f x | x <- s] = [seq f x | x <- sort leT s].

Proof.

move=> /in2_sig leT'_asym /in3_sig leT'_trans /in2_sig leT_total.
move=> /in2_sig f_homo _ /all_sigP[s ->].
rewrite [in RHS]sort_map -!map_comp /comp.
by apply: homo_sort_map => // ? ? /leT'_asym /val_inj.
Qed.

Notation fpath f := (path (coerced_frel f)).
Notation fcycle f := (cycle (coerced_frel f)).
Notation ufcycle f := (ucycle (coerced_frel f)).

Prenex Implicits path next prev cycle ucycle mem2.

Section Trajectory.

Variables (T : Type) (f : T -> T).

Fixpoint traject x n := if n is n'.+1 then x :: traject (f x) n' else [::].

Lemma trajectS x n : traject x n.+1 = x :: traject (f x) n.

Proof.

by []. Qed.

Lemma trajectSr x n : traject x n.+1 = rcons (traject x n) (iter n f x).

Proof.

by elim: n x => //= n IHn x; rewrite IHn -iterSr. Qed.

Lemma last_traject x n : last x (traject (f x) n) = iter n f x.

Proof.

by case: n => // n; rewrite iterSr trajectSr last_rcons. Qed.

Lemma traject_iteri x n :
  traject x n = iteri n (fun i => rcons^~ (iter i f x)) [::].

Proof.

by elim: n => //= n <-; rewrite -trajectSr. Qed.

Lemma size_traject x n : size (traject x n) = n.

Proof.

by elim: n x => //= n IHn x //=; rewrite IHn. Qed.

Lemma nth_traject i n : i < n -> forall x, nth x (traject x n) i = iter i f x.

Proof.

elim: n => // n IHn; rewrite ltnS => le_i_n x.
rewrite trajectSr nth_rcons size_traject.
by case: ltngtP le_i_n => [? _||->] //; apply: IHn.
Qed.

Lemma trajectD m n x :
  traject x (m + n) = traject x m ++ traject (iter m f x) n.

Proof.

by elim: m => //m IHm in x *; rewrite addSn !trajectS IHm -iterSr. Qed.

Lemma take_traject n k x : k <= n -> take k (traject x n) = traject x k.

Proof.

by move=> /subnKC<-; rewrite trajectD take_size_cat ?size_traject. Qed.

End Trajectory.

Section EqTrajectory.

Variables (T : eqType) (f : T -> T).

Lemma eq_fpath f' : f =1 f' -> fpath f =2 fpath f'.

Proof.

by move/eq_frel/eq_path. Qed.

Lemma eq_fcycle f' : f =1 f' -> fcycle f =1 fcycle f'.

Proof.

by move/eq_frel/eq_cycle. Qed.

Lemma fpathE x p : fpath f x p -> p = traject f (f x) (size p).

Proof.

by elim: p => //= y p IHp in x * => /andP[/eqP{y}<- /IHp<-]. Qed.

Lemma fpathP x p : reflect (exists n, p = traject f (f x) n) (fpath f x p).

Proof.

apply: (iffP idP) => [/fpathE->|[n->]]; first by exists (size p).
by elim: n => //= n IHn in x *; rewrite eqxx IHn.
Qed.

Lemma fpath_traject x n : fpath f x (traject f (f x) n).

Proof.

by apply/(fpathP x); exists n. Qed.

Definition looping x n := iter n f x \in traject f x n.

Lemma loopingP x n :
  reflect (forall m, iter m f x \in traject f x n) (looping x n).

Proof.

apply: (iffP idP) => loop_n; last exact: loop_n.
case: n => // n in loop_n *; elim=> [|m /= IHm]; first exact: mem_head.
move: (fpath_traject x n) loop_n; rewrite /looping !iterS -last_traject /=.
move: (iter m f x) IHm => y /splitPl[p1 p2 def_y].
rewrite cat_path last_cat def_y; case: p2 => // z p2 /and3P[_ /eqP-> _] _.
by rewrite inE mem_cat mem_head !orbT.
Qed.

Lemma trajectP x n y :
  reflect (exists2 i, i < n & y = iter i f x) (y \in traject f x n).

Proof.

elim: n x => [|n IHn] x /=; first by right; case.
rewrite inE; have [-> | /= neq_xy] := eqP; first by left; exists 0.
apply: {IHn}(iffP (IHn _)) => [[i] | [[|i]]] // lt_i_n ->.
  by exists i.+1; rewrite ?iterSr.
by exists i; rewrite ?iterSr.
Qed.

Lemma looping_uniq x n : uniq (traject f x n.+1) = ~~ looping x n.

Proof.

rewrite /looping; elim: n x => [|n IHn] x //.
rewrite [n.+1 in LHS]lock [iter]lock /= -!lock {}IHn -iterSr -negb_or inE.
congr (~~ _); apply: orb_id2r => /trajectP no_loop.
apply/idP/eqP => [/trajectP[m le_m_n def_x] | {1}<-]; last first.
  by rewrite iterSr -last_traject mem_last.
have loop_m: looping x m.+1 by rewrite /looping iterSr -def_x mem_head.
have/trajectP[[|i] // le_i_m def_fn1x] := loopingP _ _ loop_m n.+1.
by case: no_loop; exists i; rewrite -?iterSr // -ltnS (leq_trans le_i_m).
Qed.

End EqTrajectory.

Arguments fpathP {T f x p}.
Arguments loopingP {T f x n}.
Arguments trajectP {T f x n y}.
Prenex Implicits traject.

Section Fcycle.
Variables (T : eqType) (f : T -> T) (p : seq T) (f_p : fcycle f p).

Lemma nextE (x : T) (p_x : x \in p) : next p x = f x.

Proof.

exact/esym/eqP/(next_cycle f_p). Qed.

Lemma mem_fcycle : {homo f : x / x \in p}.

Proof.

by move=> x xp; rewrite -nextE// mem_next. Qed.

Lemma inj_cycle : {in p &, injective f}.

Proof.

apply: can_in_inj (iter (size p).-1 f) _ => x /rot_to[i q rip].
have /fpathE qxE : fcycle f (x :: q) by rewrite -rip rot_cycle.
have -> : size p = size (rcons q x) by rewrite size_rcons -(size_rot i) rip.
by rewrite -iterSr -last_traject prednK -?qxE ?size_rcons// last_rcons.
Qed.

End Fcycle.

Section UniqCycle.

Variables (n0 : nat) (T : eqType) (e : rel T) (p : seq T).

Hypothesis Up : uniq p.

Lemma prev_next : cancel (next p) (prev p).

Proof.

move=> x; rewrite prev_nth mem_next next_nth; case p_x: (x \in p) => //.
case Dp: p Up p_x => // [y q]; rewrite [uniq _]/= -Dp => /andP[q'y Uq] p_x.
rewrite -[RHS](nth_index y p_x); congr (nth y _ _); set i := index x p.
have: i <= size q by rewrite -index_mem -/i Dp in p_x.
case: ltngtP => // [lt_i_q|->] _; first by rewrite index_uniq.
by apply/eqP; rewrite nth_default // eqn_leq index_size leqNgt index_mem.
Qed.

Lemma next_prev : cancel (prev p) (next p).

Proof.

move=> x; rewrite next_nth mem_prev prev_nth; case p_x: (x \in p) => //.
case def_p: p p_x => // [y q]; rewrite -def_p => p_x.
rewrite index_uniq //; first by rewrite def_p ltnS index_size.
case q_x: (x \in q); first exact: nth_index.
rewrite nth_default; first by rewrite leqNgt index_mem q_x.
by apply/eqP; rewrite def_p inE q_x orbF eq_sym in p_x.
Qed.

Lemma cycle_next : fcycle (next p) p.

Proof.

case def_p: p Up => [|x q] Uq //; rewrite -[in next _]def_p.
apply/(pathP x)=> i; rewrite size_rcons => le_i_q.
rewrite -cats1 -cat_cons nth_cat le_i_q /= next_nth {}def_p mem_nth //.
rewrite index_uniq // nth_cat /= ltn_neqAle andbC -ltnS le_i_q.
by case: (i =P _) => //= ->; rewrite subnn nth_default.
Qed.

Lemma cycle_prev : cycle (fun x y => x == prev p y) p.

Proof.

apply: etrans cycle_next; symmetry; case def_p: p => [|x q] //.
by apply: eq_path; rewrite -def_p; apply: (can2_eq prev_next next_prev).
Qed.

Lemma cycle_from_next : (forall x, x \in p -> e x (next p x)) -> cycle e p.

Proof.

case: p (next p) cycle_next => //= [x q] n; rewrite -(belast_rcons x q x).
move: {q}(rcons q x) => q n_q /allP.
by elim: q x n_q => //= _ q IHq x /andP[/eqP <- n_q] /andP[-> /IHq->].
Qed.

Lemma cycle_from_prev : (forall x, x \in p -> e (prev p x) x) -> cycle e p.

Proof.

move=> e_p; apply: cycle_from_next => x.
by rewrite -mem_next => /e_p; rewrite prev_next.
Qed.

Lemma next_rot : next (rot n0 p) =1 next p.

Proof.

move=> x; have n_p := cycle_next; rewrite -(rot_cycle n0) in n_p.
case p_x: (x \in p); last by rewrite !next_nth mem_rot p_x.
by rewrite (eqP (next_cycle n_p _)) ?mem_rot.
Qed.

Lemma prev_rot : prev (rot n0 p) =1 prev p.

Proof.

move=> x; have p_p := cycle_prev; rewrite -(rot_cycle n0) in p_p.
case p_x: (x \in p); last by rewrite !prev_nth mem_rot p_x.
by rewrite (eqP (prev_cycle p_p _)) ?mem_rot.
Qed.

End UniqCycle.

Section UniqRotrCycle.

Variables (n0 : nat) (T : eqType) (p : seq T).

Hypothesis Up : uniq p.

Lemma next_rotr : next (rotr n0 p) =1 next p

Proof.

exact: next_rot. Qed.

Lemma prev_rotr : prev (rotr n0 p) =1 prev p

Proof.

exact: prev_rot. Qed.

End UniqRotrCycle.

Section UniqCycleRev.

Variable T : eqType.
Implicit Type p : seq T.

Lemma prev_rev p : uniq p -> prev (rev p) =1 next p.

Proof.

move=> Up x; case p_x: (x \in p); last first.
  by rewrite next_nth prev_nth mem_rev p_x.
case/rot_to: p_x (Up) => [i q def_p] Urp; rewrite -rev_uniq in Urp.
rewrite -(prev_rotr i Urp); do 2 rewrite -(prev_rotr 1) ?rotr_uniq //.
rewrite -rev_rot -(next_rot i Up) {i p Up Urp}def_p.
by case: q => // y q; rewrite !rev_cons !(=^~ rcons_cons, rotr1_rcons) /= eqxx.
Qed.

Lemma next_rev p : uniq p -> next (rev p) =1 prev p.

Proof.

by move=> Up x; rewrite -[p in RHS]revK prev_rev // rev_uniq. Qed.

End UniqCycleRev.

Section MapPath.

Variables (T T' : Type) (h : T' -> T) (e : rel T) (e' : rel T').

Definition rel_base (b : pred T) :=
  forall x' y', ~~ b (h x') -> e (h x') (h y') = e' x' y'.

Lemma map_path b x' p' (Bb : rel_base b) :
    ~~ has (preim h b) (belast x' p') ->
  path e (h x') (map h p') = path e' x' p'.

Proof.

by elim: p' x' => [|y' p' IHp'] x' //= /norP[/Bb-> /IHp'->]. Qed.

End MapPath.

Section MapEqPath.

Variables (T T' : eqType) (h : T' -> T) (e : rel T) (e' : rel T').

Hypothesis Ih : injective h.

Lemma mem2_map x' y' p' : mem2 (map h p') (h x') (h y') = mem2 p' x' y'.

Proof.

by rewrite [LHS]/mem2 (index_map Ih) -map_drop mem_map. Qed.

Lemma next_map p : uniq p -> forall x, next (map h p) (h x) = h (next p x).

Proof.

move=> Up x; case p_x: (x \in p); last by rewrite !next_nth (mem_map Ih) p_x.
case/rot_to: p_x => i p' def_p.
rewrite -(next_rot i Up); rewrite -(map_inj_uniq Ih) in Up.
rewrite -(next_rot i Up) -map_rot {i p Up}def_p /=.
by case: p' => [|y p''] //=; rewrite !eqxx.
Qed.

Lemma prev_map p : uniq p -> forall x, prev (map h p) (h x) = h (prev p x).

Proof.

move=> Up x; rewrite -[x in LHS](next_prev Up) -(next_map Up).
by rewrite prev_next ?map_inj_uniq.
Qed.

End MapEqPath.

Definition fun_base (T T' : eqType) (h : T' -> T) f f' :=
  rel_base h (frel f) (frel f').

Section CycleArc.

Variable T : eqType.
Implicit Type p : seq T.

Definition arc p x y := let px := rot (index x p) p in take (index y px) px.

Lemma arc_rot i p : uniq p -> {in p, arc (rot i p) =2 arc p}.

Proof.

move=> Up x p_x y; congr (fun q => take (index y q) q); move: Up p_x {y}.
rewrite -{1 2 5 6}(cat_take_drop i p) /rot cat_uniq => /and3P[_ Up12 _].
rewrite !drop_cat !take_cat !index_cat mem_cat orbC.
case p2x: (x \in drop i p) => /= => [_ | p1x].
  rewrite index_mem p2x [x \in _](negbTE (hasPn Up12 _ p2x)) /= addKn.
  by rewrite ltnNge leq_addr catA.
by rewrite p1x index_mem p1x addKn ltnNge leq_addr /= catA.
Qed.

Lemma left_arc x y p1 p2 (p := x :: p1 ++ y :: p2) :
  uniq p -> arc p x y = x :: p1.

Proof.

rewrite /arc /p [index x _]/= eqxx rot0 -cat_cons cat_uniq index_cat.
move: (x :: p1) => xp1 /and3P[_ /norP[/= /negbTE-> _] _].
by rewrite eqxx addn0 take_size_cat.
Qed.

Lemma right_arc x y p1 p2 (p := x :: p1 ++ y :: p2) :
  uniq p -> arc p y x = y :: p2.

Proof.

rewrite -[p]cat_cons -rot_size_cat rot_uniq => Up.
by rewrite arc_rot ?left_arc ?mem_head.
Qed.

Variant rot_to_arc_spec p x y :=
    RotToArcSpec i p1 p2 of x :: p1 = arc p x y
                          & y :: p2 = arc p y x
                          & rot i p = x :: p1 ++ y :: p2 :
    rot_to_arc_spec p x y.

Lemma rot_to_arc p x y :
  uniq p -> x \in p -> y \in p -> x != y -> rot_to_arc_spec p x y.

Proof.

move=> Up p_x p_y ne_xy; case: (rot_to p_x) (p_y) (Up) => [i q def_p] q_y.
rewrite -(mem_rot i) def_p inE eq_sym (negbTE ne_xy) in q_y.
rewrite -(rot_uniq i) def_p.
case/splitPr: q / q_y def_p => q1 q2 def_p Uq12; exists i q1 q2 => //.
  by rewrite -(arc_rot i Up p_x) def_p left_arc.
by rewrite -(arc_rot i Up p_y) def_p right_arc.
Qed.

End CycleArc.

Prenex Implicits arc.