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, 1 insertions, 1 deletions

diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 0a5bfde..95381ba 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -991,7 +991,7 @@ exists (block_mx 1 0 Ml L).
 exists (block_mx 1 Mu 0 R).
   by rewrite unitmxE det_ublock det_scalar1 mul1r.
 exists (1 :: d); set D1 := \matrix_(i, j) _ in dM1.
-  by rewrite /= path_min_sorted // => g _; apply: dvd1n.
+  by rewrite /= path_min_sorted //; apply/allP => g _; apply: dvd1n.
 rewrite [D in _ *m D *m _](_ : _ = block_mx 1 0 0 D1); last first.
   by apply/matrixP=> i j; do 3?[rewrite ?mxE ?ord1 //=; case: splitP => ? ->].
 rewrite !mulmx_block !(mul0mx, mulmx0, addr0) !mulmx1 add0r mul1mx -Da -dM1.