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 (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 oten 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 sequece c (viewed as a cycle) starting at the first occurrence of x in c, and ending just before the next ocurrence 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 simulaneously 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 attemps to subsitute 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 thepath 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.

End Path.

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

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

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

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

End Paths.

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

Section HomoPath.

Variables (T T' : Type) (f : T → T') (leT : rel T) (leT' : rel T').

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

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

End HomoPath.

Section EqPath.

Variables (n0 : nat) (T : eqType) (x0_cycle : T) (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 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.

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.

Section EqHomoPath.

Variables (T : eqType) (T' : Type) (f : T → T') (leT : rel T) (leT' : rel T').

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

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

End EqHomoPath.

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.

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

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

Hypothesis leT_total : total leT.

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 s1 → sorted s2 → sorted (merge s1 s2).

Lemma sort_sorted s : sorted (sort s).

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

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

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

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.

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 s → sorted (mask m s).

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

End SortSeq.

Section SortMap.
Variables (T T' : Type) (f : T' → T).

Section Monotonicity.
Variables (leT' : rel T') (leT : rel T).

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

Section Strict.
Hypothesis f_mono : {mono f : x y / leT' x y >-> leT x y }.

Lemma mono_sorted : {mono map f : s / sorted leT' s >-> sorted leT s }.

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 Strict.
End Monotonicity.

Variable (leT : rel T).

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

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

Lemma sorted_map s : sorted leT (map f s) = sorted leTf s.

End SortMap.

Lemma rev_sorted (T : Type) (leT : rel T) s :
  sorted leT (rev s) = sorted (fun y x ⇒ leT x y) s.

Section EqSortSeq.

Variable T : eqType.
Variable leT : rel T.

Section Transitive.

Hypothesis leT_tr : transitive leT.

Lemma subseq_order_path x s1 s2 :
  subseq s1 s2 → path leT x s2 → path leT 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 eq_sorted : antisymmetric leT →
  ∀ s1 s2, sorted s1 → sorted s2 → perm_eq s1 s2 → s1 = s2.

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

End Transitive.

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

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

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

Lemma perm_sort s : perm_eql (sort s) s.

Lemma mem_sort s : sort s =i s.

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

Lemma perm_sortP :
  total leT → transitive leT → antisymmetric leT →
  ∀ s1 s2, reflect (sort s1 = sort s2) (perm_eq 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 size_sort (T : Type) (leT : rel T) s : size (sort leT s) = size s.

Section EqHomoSortSeq.

Variables (T : eqType) (T' : Type) (f : T → T') (leT : rel T) (leT' : rel T').

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

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

End EqHomoSortSeq.

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 :
  all (fun y ⇒ all (leT' y) s2) s1 →
  path leT_lex x s1 → path leT_lex x s2 → path leT_lex x (merge leT s1 s2).

Lemma merge_stable_sorted s1 s2 :
  all (fun x ⇒ all (leT' x) s2) s1 →
  sorted leT_lex s1 → sorted leT_lex s2 → sorted leT_lex (merge leT s1 s2).

End Stability_merge.

Section Stability.

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

Let push_invariant := fix push_invariant (ss : seq (seq nat)) :=
  if ss is s :: ss' then
    perm_eq s (iota (size (flatten ss')) (size s)) && push_invariant ss'
  else
    true.

Let push_stable x sT s1 ss :
  all (sorted (le_lex x sT)) (s1 :: ss) → push_invariant (s1 :: ss) →
  let ss' := merge_sort_push (leN x sT) s1 ss in
  all (sorted (le_lex x sT)) ss' && push_invariant ss'.

Let pop_stable x sT s1 ss :
  all (sorted (le_lex x sT)) (s1 :: ss) → push_invariant (s1 :: ss) →
  sorted (le_lex x sT) (merge_sort_pop (leN x sT) s1 ss).

Let sort_iota_stable x sT n : sorted (le_lex x sT) (sort (leN x sT) (iota 0 n)).

Lemma sort_stable s :
    sorted leT' s →
  sorted [rel x y | leT x y && (leT y x ==> leT' x y )] (sort leT s).

End Stability.

Section Stability_filter.

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

Let le_lex_transitive x sT : transitive (le_lex x sT).

Lemma filter_sort p s : filter p (sort leT s) = sort leT (filter p s).

End Stability_filter.

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

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.

Section Monotonicity.

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

Hypothesis r_trans : transitive r.

Lemma sorted_lt_nth x0 (s : seq T) : sorted r s →
  {in [pred n | n < size s ] &, {homo nth x0 s : i j / i < j >-> r i j }}.

Lemma ltn_index (s : seq T) : sorted r s →
  {in s &, ∀ x y, index x s < index y s → r x y }.

Hypothesis r_refl : reflexive r.

Lemma sorted_le_nth x0 (s : seq T) : sorted r s →
  {in [pred n | n < size s ] &, {homo nth x0 s : i j / i ≤ j >-> r i j }}.

Lemma leq_index (s : seq T) : sorted r s →
  {in s &, ∀ x y, index x s ≤ index y s → r x y }.

End Monotonicity.