From 6542e973cdc5d10dce2e7b7b7230a804dda4e73b Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 25 Oct 2019 09:46:34 +0200
Subject: 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
---
 CHANGELOG_UNRELEASED.md | 30 +++++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

(limited to 'CHANGELOG_UNRELEASED.md')

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 97ee41a..a1b0b78 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -21,7 +21,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Added theorems `ffact_prod`, `prime_modn_expSn` and `fermat_little`
   in `binomial.v`
 
-- Added theorems `flatten_map1` and `allpairs_consr` in `seq.v`.
+- Added theorems `flatten_map1`, `allpairs_consr`, and `mask_filter` in `seq.v`.
 
 - Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`,
   `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`.
@@ -32,6 +32,27 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - Arithmetic theorems: `modn_divl` and `divn_modl`.
 
+- Added map/parametricity theorems about `path`, `sort` and `sorted`:
+
+- Added `mem2E` in `path.v`.
+
+- Added `sort_rec1` and `sortE` to help inductive reasoning on `sort`.
+
+- Added map/parametricity theorems about `path`, `sort`, and `sorted`:
+  `homo_path`, `mono_path`, `homo_path_in`, `mono_path_in`,
+  `homo_sorted`, `mono_sorted`, `map_merge`, `merge_map`, `map_sort`,
+  `sort_map`, `sorted_map`, `homo_sorted_in`, `mono_sorted_in`.
+
+- Added the theorem `perm_iota_sort` to express that the sorting of
+  any sequence `s` is equal to a mapping of `iota 0 (size s)` to the
+  nth elements of `s`, so that one can still reason on `nat`, even
+  though the elements of `s` are not in an `eqType`.
+
+- Added stability theorems about `merge` and `sort`: `sorted_merge`,
+  `merge_stable_path`, `merge_stable_sorted`, `sorted_sort`, `sort_stable`,
+  `filter_sort`, `mask_sort`, `sorted_mask_sort`, `subseq_sort`,
+  `sorted_subseq_sort`, and `mem2_sort`.
+
 ### Changed
 
 - `eqVneq` lemma is changed from `{x = y} + {x != y}` to
@@ -45,6 +66,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`.
 
+- Generalized `sort` to non-`eqType`s (as well as `merge`,
+  `merge_sort_push`, `merge_sort_pop`), together with all the lemmas
+  that did not really rely on an `eqType`: `size_merge`, `size_sort`,
+  `merge_path`, `merge_sorted`, `sort_sorted`, `path_min_sorted`
+  (which statement was modified to remove the dependency in `eqType`),
+  and `order_path_min`.
+
 ### Infrastructure
 
 - `Makefile` now supports the `test-suite` and `only` targets. Currently,
-- 
cgit v1.2.3