Add `pairwise r xs` predicate

which asserts that the relation `r` holds for any i-th and j-th element of `xs`
such that i < j.

2 files changed, 344 insertions, 130 deletions

diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 8ee8bea..d5c9488 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -126,14 +126,15 @@ 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 rot_cycle p : cycle (rot n0 p) = cycle p.
+Lemma cycle_catC p q : cycle (p ++ q) = cycle (q ++ p).
 Proof.
-case: n0 p => [|n] [|y0 p] //=; first by rewrite /rot /= cats0.
-rewrite /rot /= -[p in RHS](cat_take_drop n) -cats1 -catA cat_path.
-case: (drop n p) => [|z0 q]; rewrite /= -cats1 !cat_path /= !andbT andbC //.
-by rewrite last_cat; repeat bool_congr.
+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.
 
@@ -147,24 +148,46 @@ Proof. by case: s => //= y s /andP [->]. Qed.
 
 End Path.
 
+Section RevPath.
+
+Variables (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.
+
+End RevPath.
+
 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_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_cycle_in s : all P s -> cycle e s -> cycle e' s.
+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_path_in; rewrite /= all_rcons Px.
+by apply: sub_in_path; rewrite /= all_rcons Px.
 Qed.
 
-Lemma sub_sorted_in s : all P s -> sorted e s -> sorted e' s.
-Proof. by case: s => //; apply: sub_path_in. 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.
 
@@ -176,11 +199,11 @@ 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_path_in x s : all P (x :: s) -> path e x s = path e' x s.
-Proof. by move=> Pxs; apply/idP/idP; apply: sub_path_in Pxs. 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_cycle_in s : all P s -> cycle e s = cycle e' s.
-Proof. by move=> Ps; apply/idP/idP; apply: sub_cycle_in Ps. 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.
 
 End EqPath_in.
 
@@ -189,7 +212,7 @@ 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_path_in/all_predT; apply: in2W. Qed.
+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.
@@ -198,7 +221,7 @@ 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_path_in/all_predT; apply: in2W. Qed.
+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.
@@ -219,43 +242,41 @@ Qed.
 
 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_sorted_inE x s :
+  all P (x :: s) -> path leT x s = all (leT x) s && sorted leT s.
 Proof.
-elim: m s x => [|[] m ih] [|y s] x //=.
-  by case/and3P=> ? ? ? /andP [-> /ih ->] //; apply/andP.
-case/andP=> Px Pys /andP [xy ys]; case/andP: (Pys) => Py Ps.
-case: (mask _ _) (all_mask m Ps) (ih s y Pys ys) => //=.
-by move=> z t /andP [Pz Pt] /andP [] /(leT_tr Py Px Pz xy) ->.
+move=> Pxs; apply/idP/idP => [xs|/andP[/path_min_sorted<-//]].
+by rewrite (order_path_min_in leT_tr) //; apply: path_sorted xs.
 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_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 sorted_mask_in m s : all P s -> sorted leT s -> sorted leT (mask m s).
 Proof.
-elim: m s => [|[] m ih] [|x s] //= Pxs; first exact: path_mask_in.
-by move/path_sorted/ih; apply; case/andP: Pxs.
+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_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 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.
-elim: s => // x s ihs Pxs path_xs [|i] [|j] //=; rewrite -!topredE /= !ltnS.
-  by move=> _ js _; apply/all_nthP/js/order_path_min_in.
-by apply/ihs/path_sorted/path_xs; case/andP: Pxs.
-Qed.
+Proof. by move=> Ps; rewrite sorted_pairwise_in //; apply/pairwiseP. Qed.
 
 Hypothesis leT_refl : {in P, reflexive leT}.
 
@@ -282,11 +303,14 @@ Hypothesis leT_tr : transitive leT.
 
 Let leT_tr' : {in predT & &, transitive leT}. Proof. exact: in3W. 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_sortedE x s : path leT x s = all (leT x) s && sorted leT s.
+Proof. exact/path_sorted_inE/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_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.
@@ -294,8 +318,11 @@ 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_sortedE x s : path leT x s = all (leT x) s && sorted leT s.
-Proof. exact/path_sorted_inE/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}}.
@@ -315,48 +342,26 @@ Arguments pathP {T e x p}.
 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_mask_in {T P leT} leT_tr {x m s}.
-Arguments path_filter_in {T P leT} leT_tr {x a 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_sorted_inE {T P leT} leT_tr {x 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_mask {T leT} leT_tr {x} m {s}.
-Arguments path_filter {T leT} leT_tr {x} a {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_sortedE {T leT} leT_tr x 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}.
 
-Lemma cycle_catC (T : Type) (e : rel T) (p q : seq T) :
-  cycle e (p ++ q) = cycle e (q ++ p).
-Proof. by rewrite -rot_size_cat rot_cycle. Qed.
-
-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.
-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.
-
-End RevPath.
-
 Section HomoPath.
 
 Variables (T T' : Type) (P : {pred T}) (f : T -> T') (e : rel T) (e' : rel T').
@@ -372,23 +377,23 @@ 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_path_in. Qed.
+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_cycle_in. Qed.
+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_sorted_in. Qed.
+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_path_in. Qed.
+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_cycle_in. Qed.
+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.
@@ -436,6 +441,30 @@ 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 s /all_sigP [{}s ->].
+by rewrite cycle_map allrel_mapl allrel_mapr; apply: cycle_all2rel.
+Qed.
+
+End CycleAll2Rel.
+
 Section EqSorted.
 
 Variables (T : eqType) (leT : rel T).
@@ -478,25 +507,12 @@ 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.
-move=> leT_irr; elim=> //= x s IHs s_ord.
-rewrite (IHs (path_sorted s_ord)) andbT; apply/negP=> s_x.
-by case/allPn: (order_path_min leT_tr s_ord); exists x; rewrite // leT_irr.
-Qed.
+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.
-move=> leT_asym; elim=> [|x1 s1 IHs1] s2 //= ord_s1 ord_s2 eq_s12.
-  by case: {+}s2 (perm_size eq_s12).
-have s2_x1: x1 \in s2 by rewrite -(perm_mem eq_s12) mem_head.
-case: s2 s2_x1 eq_s12 ord_s2 => //= x2 s2; rewrite in_cons.
-case: eqP => [<- _| ne_x12 /= s2_x1] eq_s12 ord_s2.
-  by rewrite {IHs1}(IHs1 s2) ?(@path_sorted _ leT x1) // -(perm_cons x1).
-case: (ne_x12); apply: leT_asym; rewrite (allP (order_path_min _ ord_s2))//.
-have: x2 \in x1 :: s1 by rewrite (perm_mem eq_s12) mem_head.
-case/predU1P=> [eq_x12 | s1_x2]; first by case ne_x12.
-by rewrite (allP (order_path_min _ ord_s1)).
+by move=> leT_asym s1 s2; rewrite !sorted_pairwise //; apply: pairwise_eq.
 Qed.
 
 Lemma irr_sorted_eq : irreflexive leT ->
@@ -871,6 +887,28 @@ elim: s [::] => /= [|x s ihs] ss allss.
     [rewrite /= ht | apply/ihss/merge_sorted].
 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 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.
+
 Lemma size_merge s1 s2 : size (merge s1 s2) = size (s1 ++ s2).
 Proof.
 rewrite size_cat; elim: s1 s2 => // x s1 IH1.
@@ -894,30 +932,10 @@ Qed.
 Hypothesis leT_tr : transitive leT.
 
 Lemma sorted_merge s t : sorted (s ++ t) -> merge s t = s ++ t.
-Proof.
-elim: s => //= x s; case: t; rewrite ?cats0 //= => y t ih hp.
-move: (order_path_min leT_tr hp).
-by rewrite ih ?(path_sorted hp) // all_cat /= => /and3P [_ -> _].
-Qed.
+Proof. by rewrite sorted_pairwise // pairwise_cat => /and3P[/allrel_merge]. Qed.
 
 Lemma sorted_sort s : sorted 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 => h_sorted.
-  rewrite -ihss ?sorted_merge //.
-  by elim: (catss _) h_sorted => //= ? ? ih /path_sorted.
-- move=> h_sorted.
-  suff x_ss_E: catss (merge_sort_push [:: x] ss) = catss ([:: x] :: ss)
-    by rewrite (catA _ [:: _]) -[catss _ ++ _]/(catss ([:: x] :: ss)) -x_ss_E
-               ihs // x_ss_E /= -catA.
-  have {h_sorted}: sorted (catss ss ++ [:: x]).
-    case: (catss _) h_sorted => //= ? ?.
-    by rewrite (catA _ [:: _]) cat_path => /andP [].
-  elim: ss [:: x] => {x s ihs} //= -[|x s] ss ihss t h_sorted;
-    rewrite /= cats0 // sorted_merge ?ihss ?catA //.
-  by elim: (catss ss) h_sorted => //= ? ? ih /path_sorted.
-Qed.
+Proof. by rewrite sorted_pairwise //; apply/pairwise_sort. Qed.
 
 End SortSeq.
 
@@ -925,6 +943,8 @@ Arguments merge {T} relT !s1 !s2 : rename.
 Arguments merge_path {T leT} leT_total {x s1 s2}.
 Arguments merge_sorted {T leT} leT_total {s1 s2}.
 Arguments sort_sorted {T leT} leT_total s.
+Arguments allrel_merge {T leT s1 s2}.
+Arguments pairwise_sort {T leT s}.
 Arguments sorted_merge {T leT} leT_tr {s t}.
 Arguments sorted_sort {T leT} leT_tr {s}.
 
@@ -1121,7 +1141,7 @@ End Stability_merge.
 
 Section Stability_iota.
 
-Variables (leN : rel nat) (leN_total : total leN) (leN_tr : transitive leN).
+Variables (leN : rel nat) (leN_total : total leN).
 
 Let lt_lex := [rel n m | leN n m && (leN m n ==> (n < m))].
 
@@ -1172,16 +1192,24 @@ Qed.
 
 End Stability_iota.
 
-Lemma sort_stable T (leT leT' : rel T) :
-  total leT -> transitive leT' -> forall s : seq T, sorted leT' s ->
+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 leT'_tr s sorted_s; case Ds: s => // [x s1].
+move=> leT_total s pairwise_s; case Ds: s => // [x s1].
 rewrite -{s1}Ds -(mkseq_nth x s) sort_map.
 have leN_total: total (relpre (nth x s) leT) by move=> n m; apply: leT_total.
 apply: (homo_sorted_in _ (allss _)) (sort_iota_stable leN_total _) => /= y z.
 rewrite !mem_sort !mem_iota !leq0n add0n /= => ys zs /andP [->] /=.
-by case: (leT _ _); first apply: sorted_ltn_nth.
+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 filter_sort T (leT : rel T) :
@@ -1649,6 +1677,8 @@ End CycleArc.
 
 Prenex Implicits arc.
 
+(* Deprecated in 1.12.0 *)
+
 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)
@@ -1686,3 +1716,25 @@ 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).
+
+(* Deprecated in 1.13.0 *)
+
+Notation "@ 'sub_path_in'" :=
+  (deprecate sub_path_in sub_in_path) (at level 10, only parsing) : fun_scope.
+Notation "@ 'sub_cycle_in'" :=
+  (deprecate sub_cycle_in sub_in_cycle) (at level 10, only parsing) : fun_scope.
+Notation "@ 'sub_sorted_in'" := (deprecate sub_sorted_in sub_in_sorted)
+  (at level 10, only parsing) : fun_scope.
+Notation "@ 'eq_path_in'" :=
+  (deprecate eq_path_in eq_in_path) (at level 10, only parsing) : fun_scope.
+Notation "@ 'eq_cycle_in'" :=
+  (deprecate eq_cycle_in eq_in_cycle) (at level 10, only parsing) : fun_scope.
+
+Notation sub_path_in :=
+  (fun ee' => @sub_path_in _ _ _ _ ee' _ _) (only parsing).
+Notation sub_cycle_in :=
+  (fun ee' => @sub_cycle_in _ _ _ _ ee' _) (only parsing).
+Notation sub_sorted_in :=
+  (fun ee' => @sub_sorted_in _ _ _ _ ee' _) (only parsing).
+Notation eq_path_in := (fun ee' => @eq_path_in _ _ _ _ ee' _ _) (only parsing).
+Notation eq_cycle_in := (fun ee' => @eq_cycle_in _ _ _ _ ee' _) (only parsing).
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index abca0d9..2d5c5b8 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -133,9 +133,11 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 (*                      [seq f x y | x <- s, y <- t]                          *)
 (*               := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] *)
 (* allrel r xs ys := all [pred x | all (r x) ys] xs                           *)
-(*                == r x y holds whenever x is in xs and y is in ys           *)
+(*                <=> r x y holds whenever x is in xs and y is in ys          *)
 (*   all2rel r xs := allrel r xs xs                                           *)
-(*                == the proposition r x y holds for all possible x, y in xs. *)
+(*                <=> the proposition r x y holds for all possible x, y in xs.*)
+(*  pairwise r xs <=> the relation r holds for any i-th and j-th element of   *)
+(*                    xs such that i < j.                                     *)
 (*        map f s == the sequence [:: f x_1, ..., f x_n].                     *)
 (*      pmap pf s == the sequence [:: y_i1, ..., y_ik] where i1 < ... < ik,   *)
 (*                   pf x_i = Some y_i, and pf x_j = None iff j is not in     *)
@@ -3523,6 +3525,20 @@ elim: ys => /= [|y ys ihys]; first by rewrite allrel0r.
 by rewrite !allrel_consr ihys andbA.
 Qed.
 
+Lemma allrel_maskl m xs ys : allrel xs ys -> allrel (mask m xs) ys.
+Proof.
+by elim: m xs => [|[] m IHm] [|x xs] //= /andP [xys /IHm->]; rewrite ?xys.
+Qed.
+
+Lemma allrel_maskr m xs ys : allrel xs ys -> allrel xs (mask m ys).
+Proof. by elim: xs => //= x xs IHxs /andP [/all_mask->]. Qed.
+
+Lemma allrel_filterl a xs ys : allrel xs ys -> allrel (filter a xs) ys.
+Proof. by rewrite filter_mask; apply: allrel_maskl. Qed.
+
+Lemma allrel_filterr a xs ys : allrel xs ys -> allrel xs (filter a ys).
+Proof. by rewrite filter_mask; apply: allrel_maskr. Qed.
+
 Lemma allrel_allpairsE xs ys :
   allrel xs ys = all id [seq r x y | x <- xs, y <- ys].
 Proof. by elim: xs => //= x xs ->; rewrite all_cat all_map. Qed.
@@ -3538,20 +3554,40 @@ Arguments allrel1l {T S} r x ys.
 Arguments allrel1r {T S} r xs y.
 Arguments allrel_catl {T S} r xs xs' ys.
 Arguments allrel_catr {T S} r xs ys ys'.
+Arguments allrel_maskl {T S} r m xs ys.
+Arguments allrel_maskr {T S} r m xs ys.
+Arguments allrel_filterl {T S} r a xs ys.
+Arguments allrel_filterr {T S} r a xs ys.
 Arguments allrel_allpairsE {T S} r xs ys.
 
 Notation all2rel r xs := (allrel r xs xs).
 
+Lemma sub_in_allrel
+      {T S : Type} (P : {pred T}) (Q : {pred S}) (r r' : T -> S -> bool) :
+  {in P & Q, forall x y, r x y -> r' x y} ->
+  forall xs ys, all P xs -> all Q ys -> allrel r xs ys -> allrel r' xs ys.
+Proof.
+move=> rr' + ys; elim=> //= x xs IHxs /andP [Px Pxs] Qys.
+rewrite !allrel_consl => /andP [+ {}/IHxs-> //]; rewrite andbT.
+by elim: ys Qys => //= y ys IHys /andP [Qy Qys] /andP [/rr'-> // /IHys->].
+Qed.
+
+Lemma sub_allrel {T S : Type} (r r' : T -> S -> bool) :
+  (forall x y, r x y -> r' x y) ->
+  forall xs ys, allrel r xs ys -> allrel r' xs ys.
+Proof.
+by move=> rr' xs ys; apply/sub_in_allrel/all_predT/all_predT; apply: in2W.
+Qed.
+
 Lemma eq_in_allrel {T S : Type} (P : {pred T}) (Q : {pred S}) r r' :
   {in P & Q, r =2 r'} ->
   forall xs ys, all P xs -> all Q ys -> allrel r xs ys = allrel r' xs ys.
 Proof.
-move=> rr' + ys; elim=> //= x xs IH /andP [Px Pxs] Qys.
-congr andb => /=; last exact: IH.
-by elim: ys Qys {IH} => //= y ys IH /andP [Qy Qys]; rewrite rr' // IH.
+move=> rr' xs ys Pxs Qys.
+by apply/idP/idP; apply/sub_in_allrel/Qys/Pxs => ? ? ? ?; rewrite rr'.
 Qed.
 
-Lemma eq_allrel {T S : Type} (r r': T -> S -> bool) :
+Lemma eq_allrel {T S : Type} (r r' : T -> S -> bool) :
   r =2 r' -> allrel r =2 allrel r'.
 Proof. by move=> rr' xs ys; apply/eq_in_allrel/all_predT/all_predT. Qed.
 
@@ -3592,6 +3628,132 @@ Qed.
 
 End All2Rel.
 
+Section Pairwise.
+
+Variables (T : Type) (r : T -> T -> bool).
+Implicit Types (x y : T) (xs ys : seq T).
+
+Fixpoint pairwise xs : bool :=
+  if xs is x :: xs then all (r x) xs && pairwise xs else true.
+
+Lemma pairwise_cons x xs : pairwise (x :: xs) = all (r x) xs && pairwise xs.
+Proof. by []. Qed.
+
+Lemma pairwise_cat xs ys :
+  pairwise (xs ++ ys) = [&& allrel r xs ys, pairwise xs & pairwise ys].
+Proof. by elim: xs => //= x xs ->; rewrite all_cat -!andbA; bool_congr. Qed.
+
+Lemma pairwise_rcons xs x :
+  pairwise (rcons xs x) = all (r^~ x) xs && pairwise xs.
+Proof. by rewrite -cats1 pairwise_cat allrel1r andbT. Qed.
+
+Lemma pairwise2 x y : pairwise [:: x; y] = r x y.
+Proof. by rewrite /= !andbT. Qed.
+
+Lemma pairwise_mask m xs : pairwise xs -> pairwise (mask m xs).
+Proof.
+by elim: m xs => [|[] m IHm] [|x xs] //= /andP [? ?]; rewrite ?IHm // all_mask.
+Qed.
+
+Lemma pairwise_filter a xs : pairwise xs -> pairwise (filter a xs).
+Proof. by rewrite filter_mask; apply: pairwise_mask. Qed.
+
+Lemma pairwiseP x0 xs :
+  reflect {in gtn (size xs) &, {homo nth x0 xs : i j / i < j >-> r i j}}
+          (pairwise xs).
+Proof.
+elim: xs => /= [|x xs IHxs]; first exact: (iffP idP).
+apply: (iffP andP) => [[r_x_xs pxs] i j|Hnth]; rewrite -?topredE /= ?ltnS.
+  by case: i j => [|i] [|j] //= gti gtj ij; [exact/all_nthP | exact/IHxs].
+split; last by apply/IHxs => // i j; apply/(Hnth i.+1 j.+1).
+by apply/(all_nthP x0) => i gti; apply/(Hnth 0 i.+1).
+Qed.
+
+Lemma pairwise_all2rel :
+  reflexive r -> symmetric r -> forall xs, pairwise xs = all2rel r xs.
+Proof.
+by move=> r_refl r_sym; elim => //= x xs ->; rewrite all2rel_cons // r_refl.
+Qed.
+
+End Pairwise.
+
+Arguments pairwise {T} r xs.
+Arguments pairwise_cons {T} r x xs.
+Arguments pairwise_cat {T} r xs ys.
+Arguments pairwise_rcons {T} r xs x.
+Arguments pairwise2 {T} r x y.
+Arguments pairwise_mask {T r} m {xs}.
+Arguments pairwise_filter {T r} a {xs}.
+Arguments pairwiseP {T r} x0 {xs}.
+Arguments pairwise_all2rel {T r} r_refl r_sym xs.
+
+Lemma sub_in_pairwise {T : Type} (P : {pred T}) (r r' : rel T) :
+  {in P &, subrel r r'} ->
+  forall xs, all P xs -> pairwise r xs -> pairwise r' xs.
+Proof.
+move=> rr'; elim=> //= x xs IHxs /andP [Px Pxs] /andP [+ {}/IHxs->] //.
+rewrite andbT; elim: xs Pxs => //= x' xs IHxs /andP [? ?] /andP [+ /IHxs->] //.
+by rewrite andbT; apply: rr'.
+Qed.
+
+Lemma sub_pairwise {T : Type} (r r' : rel T) xs :
+  subrel r r' -> pairwise r xs -> pairwise r' xs.
+Proof. by move=> rr'; apply/sub_in_pairwise/all_predT; apply: in2W. Qed.
+
+Lemma eq_in_pairwise {T : Type} (P : {pred T}) (r r' : rel T) :
+  {in P &, r =2 r'} -> forall xs, all P xs -> pairwise r xs = pairwise r' xs.
+Proof.
+move=> rr' xs Pxs.
+by apply/idP/idP; apply/sub_in_pairwise/Pxs => ? ? ? ?; rewrite rr'.
+Qed.
+
+Lemma eq_pairwise {T : Type} (r r' : rel T) :
+  r =2 r' -> pairwise r =i pairwise r'.
+Proof. by move=> rr' xs; apply/eq_in_pairwise/all_predT. Qed.
+
+Lemma pairwise_map {T T' : Type} (f : T' -> T) (r : rel T) xs :
+  pairwise r (map f xs) = pairwise (relpre f r) xs.
+Proof. by elim: xs => //= x xs ->; rewrite all_map. Qed.
+
+Section EqPairwise.
+
+Variables (T : eqType) (r : T -> T -> bool).
+Implicit Types (xs ys : seq T).
+
+Lemma subseq_pairwise xs ys : subseq xs ys -> pairwise r ys -> pairwise r xs.
+Proof. by case/subseqP => m _ ->; apply: pairwise_mask. Qed.
+
+Lemma uniq_pairwise xs : uniq xs = pairwise [rel x y | x != y] xs.
+Proof.
+elim: xs => //= x xs ->; congr andb; rewrite -has_pred1 -all_predC.
+by elim: xs => //= x' xs ->; case: eqVneq.
+Qed.
+
+Lemma pairwise_uniq xs : irreflexive r -> pairwise r xs -> uniq xs.
+Proof.
+move=> r_irr; rewrite uniq_pairwise; apply/sub_pairwise => x y.
+by apply: contraTneq => ->; rewrite r_irr.
+Qed.
+
+Lemma pairwise_eq : antisymmetric r ->
+  forall xs ys, pairwise r xs -> pairwise r ys -> perm_eq xs ys -> xs = ys.
+Proof.
+move=> r_asym; elim=> [|x xs IHxs] [|y ys] //=; try by move=> ? ? /perm_size.
+move=> /andP [r_x_xs pxs] /andP [r_y_ys pys] eq_xs_ys.
+move: (mem_head y ys) (mem_head x xs).
+rewrite -(perm_mem eq_xs_ys) [x \in _](perm_mem eq_xs_ys) !inE.
+case: eqVneq eq_xs_ys => /= [->|ne_xy] eq_xs_ys ys_x xs_y.
+  by rewrite (IHxs ys) // -(perm_cons x).
+by case/eqP: ne_xy; apply: r_asym; rewrite (allP r_x_xs) ?(allP r_y_ys).
+Qed.
+
+End EqPairwise.
+
+Arguments subseq_pairwise {T r xs ys}.
+Arguments uniq_pairwise {T} xs.
+Arguments pairwise_uniq {T r xs}.
+Arguments pairwise_eq {T r} r_asym {xs ys}.
+
 Section Permutations.
 
 Variable T : eqType.