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 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 p.
  • 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 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 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 path_sorted x s : path x s → sorted s.

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

End Path.

Section SubPath_in.

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

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

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

Lemma sub_sorted_in 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_path_in x s : all P (x :: s) → path e x s = path e' x s.

Lemma eq_cycle_in s : all P s → cycle e s = cycle 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'.

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_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_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_sorted_inE x s :
  all P (x :: s) → path leT x s = all (leT x) s && sorted leT 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.

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

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_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_sortedE x s : path leT x s = all (leT x) s && sorted leT 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}}.

End Transitive.

End Paths.


Lemma cycle_catC (T : Type) (e : rel T) (p q : seq T) :
  cycle e (p ++ q) = cycle e (q ++ p).

Section RevPath.

Variables (T : Type) (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.

End RevPath.

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.


Section EqSorted.

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


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

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.


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') & subpred (mem p') (mem 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.


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.

Hypothesis leT_total : total leT.

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

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

Lemma sort_sorted s : sorted (sort s).

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

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

Hypothesis leT_tr : transitive leT.

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

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

End SortSeq.


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.


Section SortSeq_in.

Variables (T : Type) (P : {pred T}) (leT : rel T).
Let le_sT := relpre (val : sig P → _) leT.

Hypothesis leT_total : {in P &, total leT}.
Let le_sT_total : total le_sT := in2_sig leT_total.

Lemma sort_sorted_in s : all P s → sorted leT (sort leT s).

Hypothesis leT_tr : {in P & &, transitive leT}.
Let le_sT_tr : transitive le_sT := in3_sig leT_tr.

Lemma sorted_sort_in s : all P s → sorted leT s → sort leT s = s.

End SortSeq_in.


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

End EqSortSeq.

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 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_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 iota_sorted i n : sorted leq (iota i n).

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

Section Stability_merge.

Variables (T : Type) (leT 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 leT s1 s2).

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

End Stability_merge.

Section Stability_iota.

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

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


Let push_invariant := fix push_invariant (ss : seq (seq nat)) :=
  if ss is s :: ss' then
    sorted lt_lex s && perm_eq s (iota (size (flatten ss')) (size s)) &&
    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_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 filter_sort T (leT : rel T) :
  total leT → transitive leT →
  ∀ p s, filter p (sort leT s) = sort leT (filter p 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_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.

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.


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.


Notation "@ 'eq_sorted'" :=
  (deprecate eq_sorted sorted_eq) (at level 10, only parsing) : fun_scope.
Notation "@ 'eq_sorted_irr'" := (deprecate eq_sorted_irr irr_sorted_eq)
  (at level 10, only parsing) : fun_scope.
Notation "@ 'sorted_lt_nth'" :=
  (fun (T : Type) (leT : rel T) (leT_tr : transitive leT) ⇒
     deprecate sorted_lt_nth sorted_ltn_nth leT_tr)
  (at level 10, only parsing) : fun_scope.
Notation "@ 'sorted_le_nth'" :=
  (fun (T : Type) (leT : rel T) (leT_tr : transitive leT) ⇒
     deprecate sorted_le_nth sorted_leq_nth leT_tr)
  (at level 10, only parsing) : fun_scope.
Notation "@ 'ltn_index'" :=
  (fun (T : eqType) (leT : rel T) (leT_tr : transitive leT) ⇒
     deprecate ltn_index sorted_ltn_index leT_tr)
  (at level 10, only parsing) : fun_scope.
Notation "@ 'leq_index'" :=
  (fun (T : eqType) (leT : rel T) (leT_tr : transitive leT) ⇒
     deprecate leq_index sorted_leq_index leT_tr)
  (at level 10, only parsing) : fun_scope.
Notation "@ 'subseq_order_path'" := (deprecate subseq_order_path subseq_path)
  (at level 10, only parsing) : fun_scope.

Notation eq_sorted :=
  (fun le_tr le_asym ⇒ @eq_sorted _ _ le_tr le_asym _ _) (only parsing).
Notation eq_sorted_irr :=
  (fun le_tr le_irr ⇒ @eq_sorted_irr _ _ le_tr le_irr _ _) (only parsing).
Notation sorted_lt_nth :=
  (fun leT_tr x0 ⇒ @sorted_lt_nth _ _ leT_tr x0 _) (only parsing).
Notation sorted_le_nth :=
  (fun leT_tr leT_refl x0 ⇒ @sorted_le_nth _ _ leT_tr leT_refl x0 _)
  (only parsing).
Notation ltn_index := (fun leT_tr ⇒ @ltn_index _ _ leT_tr _) (only parsing).
Notation leq_index :=
  (fun leT_tr leT_refl ⇒ @leq_index _ _ leT_tr leT_refl _) (only parsing).
Notation subseq_order_path :=
  (fun leT_tr ⇒ @subseq_order_path _ _ leT_tr _ _ _) (only parsing).