Library mathcomp.ssreflect.path

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
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.

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.

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

Lemma take_path x p i : path x p → path x (take i p).

Lemma pathP x p x0 :
  reflect (∀ i, i < size p → e (nth x0 (x :: p) i) (nth x0 p i))
          (path x p).

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.

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

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

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

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

Lemma sortedP s x :
  reflect (∀ i, i.+1 < size s → e (nth x s i) (nth x s i.+1)) (sorted s).

Lemma path_sorted x s : path x s → sorted s.

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

Lemma pairwise_sorted s : pairwise e s → sorted s.

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

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.

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

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

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.

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

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

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.

Lemma sub_in_cycle s : all P s → cycle e s → cycle e' s.

Lemma sub_in_sorted s : all P s → sorted e s → sorted e' s.

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'}.
Let e'_e : {in P &, subrel e' e}.

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

Lemma eq_in_cycle s : all P s → cycle e s = cycle e' s.

Lemma eq_in_sorted s : all P s → sorted e s = sorted e' s.

End EqPath_in.

Section SubPath.

Variables e e' : rel T.

Lemma sub_path : subrel e e' → ∀ x p, path e x p → path e' x p.

Lemma sub_cycle : subrel e e' → subpred (cycle e) (cycle e').

Lemma sub_sorted : subrel e e' → subpred (sorted e) (sorted e').

Lemma eq_path : e =2 e' → path e =2 path e'.

Lemma eq_cycle : e =2 e' → cycle e =1 cycle e'.

Lemma eq_sorted : e =2 e' → sorted e =1 sorted e'.

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.

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.

Lemma sorted_pairwise_in s : all P s → sorted leT s = pairwise leT s.

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

Lemma cat_sorted2 s s' : sorted leT (s ++ s') → sorted leT s × sorted leT s'.

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

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

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

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

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}}.

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}}.

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.

Hypothesis leT_tr : transitive leT.

Lemma path_le x x' s : leT x x' → path leT x' s → path leT x s.

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

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

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

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

Lemma sorted_mask m s : sorted leT s → sorted leT (mask m s).

Lemma sorted_filter a s : sorted leT s → sorted leT (filter a s).

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

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

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}}.

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}}.

Lemma take_sorted n s : sorted leT s → sorted leT (take n s).

Lemma drop_sorted n s : sorted leT s → sorted leT (drop n s).

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.

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

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

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).

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).

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).

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.

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.

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.

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).

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

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

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.

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

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

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 → ∀ s, cycle leT s = all2rel leT s.

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

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.

Lemma prefix_sorted s1 s2 : prefix s1 s2 → sorted s2 → sorted s1.

Lemma infix_sorted s1 s2 : infix s1 s2 → sorted s2 → sorted s1.

Lemma suffix_sorted s1 s2 : suffix s1 s2 → sorted s2 → sorted s1.

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.

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

Lemma sorted_ltn_index_in s : {in s & &, transitive leT} → sorted s →
  {in s &, ∀ x y, index x s < index y s → leT x y}.

Lemma sorted_leq_index_in s :
  {in s & &, transitive leT} → {in s, reflexive leT} → sorted s →
  {in s &, ∀ x y, index x s ≤ index y s → leT x y}.

Hypothesis leT_tr : transitive leT.

Lemma subseq_path x s1 s2 : subseq s1 s2 → path x s2 → path x s1.

Lemma subseq_sorted s1 s2 : subseq s1 s2 → sorted s2 → sorted s1.

Lemma sorted_uniq : irreflexive leT → ∀ s, sorted s → uniq s.

Lemma sorted_eq : antisymmetric leT →
  ∀ s1 s2, sorted s1 → sorted s2 → perm_eq s1 s2 → s1 = s2.

Lemma irr_sorted_eq : irreflexive leT →
  ∀ s1 s2, sorted s1 → sorted s2 → s1 =i s2 → s1 = s2.

Lemma sorted_ltn_index s :
  sorted s → {in s &, ∀ x y, index x s < index y s → leT x y}.

Lemma undup_path x s : path x s → path x (undup s).

Lemma undup_sorted s : sorted s → sorted (undup s).

Hypothesis leT_refl : reflexive leT.

Lemma sorted_leq_index s :
  sorted s → {in s &, ∀ x y, index x s ≤ index y s → leT x y}.

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.

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.

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.

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).

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.

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

Lemma splitPr p x : x \in p → splitr x p.

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 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 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.

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.

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

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

ucycleb is the boolean predicate, but ucycle is defined as a Prop so that it can be used as a coercion target.
Definition ucycleb p := cycle e p && uniq p.
Definition ucycle p : Prop := cycle e p && uniq p.

Projections, used for creating local lemmas.
Lemma ucycle_cycle p : ucycle p → cycle e p.

Lemma ucycle_uniq p : ucycle p → uniq p.

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

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

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

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

The "appears no later" partial preorder defined by a path.

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

Lemma mem2l p x y : mem2 p x y → x \in p.

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

Lemma mem2r p x y : mem2 p x y → y \in p.

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

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).

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

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

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).

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

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

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

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

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.

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

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.

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).

End EqPath.

Ordered paths and sorting.

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 [::].

The following definition `sort_rec1` is an auxiliary function for inductive reasoning on `sort`. One can rewrite `sort le s` to `sort_rec1 le [:: ] s` by `sortE` and apply the simple structural induction on `s` to reason about it.
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.

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

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

Lemma allrel_merge s1 s2 : allrel leT s1 s2 → merge s1 s2 = s1 ++ s2.

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

Lemma pairwise_sort s : pairwise leT s → sort s = s.

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

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).

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

End Stability.

Hypothesis leT_total : total leT.

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

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

Lemma merge_sorted s1 s2 :
  sorted leT s1 → sorted leT s2 → sorted leT (merge s1 s2).

Hypothesis leT_tr : transitive leT.

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

Lemma sorted_sort s : sorted leT s → sort s = s.

Lemma mergeA : associative merge.

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}.

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

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).

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

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} →
  ∀ s : seq T, all P s → sorted leT s → sort leT s = s.

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).

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

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

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

Lemma mem_sort s : sort leT s =i s.

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

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').

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}.

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.

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

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

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

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

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

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

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).

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

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

End Stability_iota.

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

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

Lemma sort_stable_in T (P : {pred T}) (leT leT' : rel T) :
  {in P &, total leT} → {in P & &, transitive leT'} →
  ∀ 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).

Lemma filter_sort T (leT : rel T) :
  total leT → transitive leT →
  ∀ p s, filter p (sort leT s) = sort leT (filter p s).

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

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)}.

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

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)}.

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}.

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}.

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

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

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).

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).

Lemma mem2_sort_in s :
  {in s &, total leT} → {in s & &, transitive leT} →
  ∀ x y, leT x y → mem2 s x y → mem2 (sort leT s) x y.

End Stability_subseq_in.

Lemma sort_sorted T (leT : rel T) :
  total leT → ∀ s, sorted leT (sort leT s).

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

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 →
  ∀ s1 s2, reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2).

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).

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} →
  ∀ s : seq T, sort leT' (map f s) = map f (sort leT s).

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}} →
  ∀ s : seq T, all P s →
        sort leT' [seq f x | x <- s] = [seq f x | x <- sort leT s].

Function trajectories.

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


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.

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

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

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

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

Lemma nth_traject i n : i < n → ∀ x, nth x (traject x n) i = iter i f x.

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

Lemma take_traject n k x : k ≤ n → take k (traject x n) = traject x k.

End Trajectory.

Section EqTrajectory.

Variables (T : eqType) (f : T → T).

Lemma eq_fpath f' : f =1 f' → fpath f =2 fpath f'.

Lemma eq_fcycle f' : f =1 f' → fcycle f =1 fcycle f'.

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

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

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

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

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

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

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

End EqTrajectory.

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

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.

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

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

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).

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

Lemma cycle_next : fcycle (next p) p.

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

Lemma cycle_from_next : (∀ x, x \in p → e x (next p x)) → cycle e p.

Lemma cycle_from_prev : (∀ x, x \in p → e (prev p x) x) → cycle e p.

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

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

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.

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

End UniqRotrCycle.

Section UniqCycleRev.

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

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

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

End UniqCycleRev.

Section MapPath.

Variables (T T' : Type) (h : T' → T) (e : rel T) (e' : rel T').

Definition rel_base (b : pred T) :=
  ∀ 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'.

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'.

Lemma next_map p : uniq p → ∀ x, next (map h p) (h x) = h (next p x).

Lemma prev_map p : uniq p → ∀ x, prev (map h p) (h x) = h (prev p x).

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}.

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

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

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.

End CycleArc.