Stability proofs of sort (#358)

* Modified the definition of sort to work on any type

* Other Generalizations, fixes and CHANGELOG entry

* Add stability lemmas for `path.sort`

- Inverse the comparison in `merge` and swap arguments of it everywhere.
- Add `sort_rec1` and `sortE` to simplify inductive proofs on `sort`.
- Add `seq.mask_filter`, `mem2E`, `path_mask`, `path_filter`, and `sorted_mask`.
- Generalize `sorted_filter`, `homo_path_in`, `mono_path_in`, `homo_sorted_in`,
  and `mono_sorted_in` to non-`eqType`s.
- Add the following lemmas to state the stability of `path.merge` and `path.sort`.

sorted_merge
     : forall (T : Type) (leT : rel T),
       transitive leT ->
       forall s t : seq T, sorted leT (s ++ t) -> merge leT s t = s ++ t

merge_stable_path
     : forall (T : Type) (leT leT' : rel T),
       total leT ->
       forall (x : T) (s1 s2 : seq T),
       all (fun y : T => all (leT' y) s2) s1 ->
       path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x s1 ->
       path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x s2 ->
       path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x
         (merge leT s1 s2)

merge_stable_sorted
     : forall (T : Type) (leT leT' : rel T),
       total leT ->
       forall s1 s2 : seq T,
       all (fun x : T => all (leT' x) s2) s1 ->
       sorted [rel x y | leT x y && (leT y x ==> leT' x y)] s1 ->
       sorted [rel x y | leT x y && (leT y x ==> leT' x y)] s2 ->
       sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (merge leT s1 s2)

sorted_sort
     : forall (T : Type) (leT : rel T),
       transitive leT -> forall s : seq T, sorted leT s -> sort leT s = s

sort_stable
     : forall (T : Type) (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)

filter_sort
     : forall (T : Type) (leT : rel T),
       total leT -> transitive leT ->
       forall (p : pred T) (s : seq T),
       [seq x <- sort leT s | p x] = sort leT [seq x <- s | p x]

mask_sort
     : forall (T : Type) (leT : rel T),
       total leT -> transitive leT ->
       forall (s : seq T) (m : bitseq),
       {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}

mask_sort'
     : forall (T : Type) (leT : rel T),
       total leT -> transitive leT ->
       forall (s : seq T) (m : bitseq),
       sorted leT (mask m s) ->
       {m_s : bitseq | mask m_s (sort leT s) = mask m s}

subseq_sort
     : forall (T : eqType) (leT : rel T),
       total leT -> transitive leT -> {homo sort leT : t s / subseq t s}

subseq_sort'
     : forall (T : eqType) (leT : rel T),
       total leT -> transitive leT ->
       forall t s : seq T, subseq t s -> sorted leT t -> subseq t (sort leT s)

mem2_sort
     : forall (T : eqType) (leT : rel T),
       total leT -> transitive leT ->
       forall (s : seq T) (x y : T),
       leT x y -> mem2 s x y -> mem2 (sort leT s) x y

* Avoid some eta-expansions

* Get the proper fix of `order_path_min` and remove `sort_map_in`

* Update documentation and CHANGELOG entries

1 files changed, 10 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index e310593..c45f7fc 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -2077,6 +2077,16 @@ Notation "[ 'seq' E : R | i : T <- s & C ]" :=
 Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s.
 Proof. by elim: s => //= x s <-; case: (a x). Qed.
 
+Lemma mask_filter (T : eqType) (s : seq T) (m : bitseq) :
+  uniq s -> mask m s = [seq i <- s | i \in mask m s].
+Proof.
+elim: m s => [|[] m ih] [|x s] //=.
+- by move=> _; elim: s.
+- case/andP => /negP x_notin_s /ih {1}->; rewrite inE eqxx /=; congr cons.
+  by apply/eq_in_filter => ?; rewrite inE; case: eqP => // ->.
+- by case: ifP => [/mem_mask -> // | _ /andP [] _ /ih].
+Qed.
+
 Section FilterSubseq.
 
 Variable T : eqType.