Merge pull request #533 from affeldt-aist/changelogs_before_release

edit changelogs before release

2 files changed, 125 insertions, 113 deletions

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d5d4f56..af55ce6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,11 +1,134 @@
 # Changelog
 All notable changes to this project will be documented in this file.
 
-Last releases: [[1.11.0+beta1] - 2020-04-15](#1110beta1---2020-04-15) and [[1.10.0] - 2019-11-29](#1100---2019-11-29).
+Last releases: [[1.11.0] - 2020-06-09](#1110---2020-06-09), [[1.11+beta1] - 2020-04-15](#111beta1---2020-04-15), and [[1.10.0] - 2019-11-29](#1100---2019-11-29).
 
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
-## [1.11.0+beta1] - 2020-04-15
+## [1.11.0] - 2020-06-09
+
+This release is compatible with Coq versions 8.7, 8.8, 8.9, 8.10, and 8.11.
+
+- Added lemmas about monotony of functions `nat -> T` where `T` is an
+  ordered type: `homo_ltn_lt_in`, `incn_inP`, `nondecn_inP`,
+  `nhomo_ltn_lt_in`, `decn_inP`, `nonincn_inP`, `homo_ltn_lt`,
+  `incnP`, `nondecnP`, `nhomo_ltn_lt`, `decnP`, `nonincnP` in file
+  `order.v`.
+
+- Added lemmas for swaping arguments of homomorphisms and
+  monomorphisms: `homo_sym`, `mono_sym`, `homo_sym_in`, `mono_sym_in`,
+  `homo_sym_in11`, `mono_sym_in11` in `ssrbool.v`
+
+### Added
+
+- in `ssrnum.v`, new lemmas:
+  + `(real_)ltr_normlW`, `(real_)ltrNnormlW`, `(real_)ler_normlW`, `(real_)lerNnormlW`
+  + `(real_)ltr_distl_addr`, `(real_)ler_distl_addr`, `(real_)ltr_distlC_addr`, `(real_)ler_distlC_addr`,
+    `(real_)ltr_distl_subl`, `(real_)ler_distl_subl`, `(real_)ltr_distlC_subl`, `(real_)ler_distlC_subl`
+
+- in `order.v`, defining `min` and `max` independently from `meet` and
+  `join`, and providing a theory about for min and max, hence generalizing
+  the theory of `Num.min` and `Num.max` from versions <= `1.10`, instead
+  of specializing to total order as in `1.11+beta1`:
+  ```
+  Definition min (T : porderType) (x y : T) := if x < y then x else y.
+  Definition max (T : porderType) (x y : T) := if x < y then y else x.
+  ```
+  + Lemmas: `min_l`, `min_r`, `max_l`, `max_r`, `minxx`, `maxxx`, `eq_minl`, `eq_maxr`,
+    `min_idPl`, `max_idPr`, `min_minxK`, `min_minKx`, `max_maxxK`, `max_maxKx`,
+    `comparable_minl`, `comparable_minr`,  `comparable_maxl`, and `comparable_maxr`
+  + Lemmas about interaction with lattice operations:  `meetEtotal`, `joinEtotal`,
+  + Lemmas under condition of pairwise comparability of a (sub)set of their arguments:
+    `comparable_minC`, `comparable_maxC`, `comparable_eq_minr`, `comparable_eq_maxl`,
+    `comparable_le_minr`, `comparable_le_minl`, `comparable_min_idPr`,
+    `comparable_max_idPl`, `comparableP`, `comparable_lt_minr`,
+    `comparable_lt_minl`, `comparable_le_maxr`, `comparable_le_maxl`,
+    `comparable_lt_maxr`, `comparable_lt_maxl`, `comparable_minxK`, `comparable_minKx`,
+    `comparable_maxxK`, `comparable_maxKx`,
+    `comparable_minA`, `comparable_maxA`, `comparable_max_minl`, `comparable_min_maxl`,
+    `comparable_minAC`, `comparable_maxAC`, `comparable_minCA`, `comparable_maxCA`,
+    `comparable_minACA`, `comparable_maxACA`, `comparable_max_minr`, `comparable_min_maxr`
+  + and the same but in a total order: `minC`, `maxC`, `minA`, `maxA`, `minAC`, `maxAC`,
+    `minCA`, `maxCA`, `minACA`, `maxACA`, `eq_minr`, `eq_maxl`,
+    `min_idPr`, `max_idPl`, `le_minr`, `le_minl`, `lt_minr`,
+    `lt_minl`, `le_maxr`,`le_maxl`, `lt_maxr`, `lt_maxl`, `minxK`, `minKx`,
+    `maxxK`, `maxKx`, `max_minl`, `min_maxl`, `max_minr`, `min_maxr`
+- in `ssrnum.v`, theory about `min` and `max` extended to `numDomainType`:
+  + Lemmas: `real_oppr_max`, `real_oppr_min`, `real_addr_minl`, `real_addr_minr`,
+    `real_addr_maxl`, `real_addr_maxr`, `minr_pmulr`, `maxr_pmulr`, `real_maxr_nmulr`,
+    `real_minr_nmulr`, `minr_pmull`, `maxr_pmull`, `real_minr_nmull`, `real_maxr_nmull`,
+    `real_maxrN`, `real_maxNr`, `real_minrN`, `real_minNr`
+- the compatibility module `ssrnum.mc_1_10` was extended to  support definitional
+  compatibility with `min` and `max` which had been lost in `1.11+beta1` for most instances.
+- in `fintype.v`, new lemmas: `seq_sub_default`, `seq_subE`
+- in `order.v`, new "unfolding" lemmas: `minEnat` and `maxEnat`
+
+- in `ssrbool.v`
+  + lemmas about the `cancel` predicate and `{in _, _}`/`{on _, _}` notations:
+    * `onW_can`, `onW_can_in`, `in_onW_can`, `onS_can`, `onS_can_in`, `in_onS_can`
+  + lemmas about the `cancel` predicate and injective functions:
+    * `inj_can_sym_in_on`, `inj_can_sym_on`, `inj_can_sym_in`
+
+### Changed
+
+- in `order.v`, `le_xor_gt`, `lt_xor_ge`, `compare`, `incompare`, `lel_xor_gt`,
+  `ltl_xor_ge`, `comparel`, `incomparel` have more parameters, so that the
+  the following now deal with `min` and `max`
+  + `comparable_ltgtP`, `comparable_leP`, `comparable_ltP`, `comparableP`
+  + `lcomparableP`, `lcomparable_ltgtP`, `lcomparable_leP`, `lcomparable_ltP`, `ltgtP`
+- in `order.v`:
+  + `[arg min_(i < i0 | P) M]` now for `porderType` (was for `orderType`)
+  + `[arg max_(i < i0 | P) M]` now for `porderType` (was for `orderType`)
+  + added `comparable_arg_minP`,  `comparable_arg_maxP`,  `real_arg_minP`,  `real_arg_maxP`,
+    in order to take advantage of the former generalizations.
+- in `ssrnum.v`, `maxr` is a notation for `(@Order.max ring_display _)` (was `Order.join`)
+  (resp. `minr` is a notation for `(@Order.min ring_display _)`)
+- in `ssrnum.v`, `ler_xor_gt`, `ltr_xor_ge`, `comparer`,
+  `ger0_xor_lt0`, `ler0_xor_gt0`, `comparer0` have now more parameters, so that
+  the following now deal with min and max:
+  + `real_leP`, `real_ltP x y`, `real_ltgtP`, `real_ge0P`, `real_le0P`, `real_ltgt0P`
+  + `lerP`, `ltrP`, `ltrgtP`, `ger0P`, `ler0P`, `ltrgt0P`
+- in `ssrnum.v`, the following have been restated (which were formerly derived from
+  `order.v` and stated with specializations of the `meet` and `join` operators):
+   + `minrC`, `minrr`, `minr_l`, `minr_r`, `maxrC`, `maxrr`, `maxr_l`,
+     `maxr_r`, `minrA`, `minrCA`, `minrAC`, `maxrA`, `maxrCA`, `maxrAC`
+   + `eqr_minl`, `eqr_minr`, `eqr_maxl`, `eqr_maxr`, `ler_minr`, `ler_minl`,
+     `ler_maxr`, `ler_maxl`, `ltr_minr`, `ltr_minl`, `ltr_maxr`, `ltr_maxl`
+   + `minrK`, `minKr`, `maxr_minl`, `maxr_minr`, `minr_maxl`, `minr_maxr`
+- The new definitions of `min` and `max` may require the following rewrite rules
+  changes when dealing with `max` and `min` instead of `meet` and `join`:
+  + `ltexI` -> `(le_minr,lt_minr)`
+  + `lteIx` -> `(le_minl,lt_minl)`
+  + `ltexU` -> `(le_maxr,lt_maxr)`
+  + `lteUx` -> `(le_maxl,lt_maxl)`
+  + `lexU` -> `le_maxr`
+  + `ltxU` -> `lt_maxr`
+  + `lexU` -> `le_maxr`
+
+- in `ssrbool.v`
+  + lemmas about monotone functions and the `{in _, _}` notation:
+    * `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`, `monoRL_in`, `can_mono_in`
+
+### Renamed
+
+- in `fintype` we deprecate and rename the following:
+  + `arg_minP` -> `arg_minnP`
+  + `arg_maxP` -> `arg_maxnP`
+
+- in `order.v`, in module `NatOrder`, renamings:
+  + `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat`,
+    `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat`
+
+### Removed
+
+- in `order.v`, removed `total_display` (was used to provide the notation
+  `max` for `join` and `min` for `meet`).
+- in `order.v`, removed `minnE` and `maxnE`
+- in `order.v`,
+  + removed `meetEnat` (in favor of `meetEtotal` followed by `minEnat`)
+  + removed `joinEnat` (in favor of `joinEtotal` followed by `maxEnat`)
+
+## [1.11+beta1] - 2020-04-15
 
 This release is compatible with Coq versions 8.7, 8.8, 8.9 and 8.10.
 
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index a291d48..13e1d1b 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -8,125 +8,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ## [Unreleased]
 
-- Added lemmas about monotony of functions `nat -> T` where `T` is an
-  ordered type: `homo_ltn_lt_in`, `incn_inP`, `nondecn_inP`,
-  `nhomo_ltn_lt_in`, `decn_inP`, `nonincn_inP`, `homo_ltn_lt`,
-  `incnP`, `nondecnP`, `nhomo_ltn_lt`, `decnP`, `nonincnP` in file
-  `order.v`.
-
-- Added lemmas for swaping arguments of homomorphisms and
-  monomorphisms: `homo_sym`, `mono_sym`, `homo_sym_in`, `mono_sym_in`,
-  `homo_sym_in11`, `mono_sym_in11` in `ssrbool.v`
-
 ### Added
 
-- in `ssrnum.v`, new lemmas:
-  + `(real_)ltr_normlW`, `(real_)ltrNnormlW`, `(real_)ler_normlW`, `(real_)lerNnormlW`
-  + `(real_)ltr_distl_addr`, `(real_)ler_distl_addr`, `(real_)ltr_distlC_addr`, `(real_)ler_distlC_addr`,
-    `(real_)ltr_distl_subl`, `(real_)ler_distl_subl`, `(real_)ltr_distlC_subl`, `(real_)ler_distlC_subl`
-
-- in `order.v`, defining `min` and `max` independently from `meet` and
-  `join`, and providing a theory about for min and max, hence generalizing
-  the theory of `Num.min` and `Num.max` from versions <= `1.10`, instead
-  of specializing to total order as in `1.11+beta1`:
-  ```
-  Definition min (T : porderType) (x y : T) := if x < y then x else y.
-  Definition max (T : porderType) (x y : T) := if x < y then y else x.
-  ```
-  + Lemmas: `min_l`, `min_r`, `max_l`, `max_r`, `minxx`, `maxxx`, `eq_minl`, `eq_maxr`,
-    `min_idPl`, `max_idPr`, `min_minxK`, `min_minKx`, `max_maxxK`, `max_maxKx`,
-    `comparable_minl`, `comparable_minr`,  `comparable_maxl`, and `comparable_maxr`
-  + Lemmas about interaction with lattice operations:  `meetEtotal`, `joinEtotal`,
-  + Lemmas under condition of pairwise comparability of a (sub)set of their arguments:
-    `comparable_minC`, `comparable_maxC`, `comparable_eq_minr`, `comparable_eq_maxl`,
-    `comparable_le_minr`, `comparable_le_minl`, `comparable_min_idPr`,
-    `comparable_max_idPl`, `comparableP`, `comparable_lt_minr`,
-    `comparable_lt_minl`, `comparable_le_maxr`, `comparable_le_maxl`,
-    `comparable_lt_maxr`, `comparable_lt_maxl`, `comparable_minxK`, `comparable_minKx`,
-    `comparable_maxxK`, `comparable_maxKx`,
-    `comparable_minA`, `comparable_maxA`, `comparable_max_minl`, `comparable_min_maxl`,
-    `comparable_minAC`, `comparable_maxAC`, `comparable_minCA`, `comparable_maxCA`,
-    `comparable_minACA`, `comparable_maxACA`, `comparable_max_minr`, `comparable_min_maxr`
-  + and the same but in a total order: `minC`, `maxC`, `minA`, `maxA`, `minAC`, `maxAC`,
-    `minCA`, `maxCA`, `minACA`, `maxACA`, `eq_minr`, `eq_maxl`,
-    `min_idPr`, `max_idPl`, `le_minr`, `le_minl`, `lt_minr`,
-    `lt_minl`, `le_maxr`,`le_maxl`, `lt_maxr`, `lt_maxl`, `minxK`, `minKx`,
-    `maxxK`, `maxKx`, `max_minl`, `min_maxl`, `max_minr`, `min_maxr`
-- in `ssrnum.v`, theory about `min` and `max` extended to `numDomainType`:
-  + Lemmas: `real_oppr_max`, `real_oppr_min`, `real_addr_minl`, `real_addr_minr`,
-    `real_addr_maxl`, `real_addr_maxr`, `minr_pmulr`, `maxr_pmulr`, `real_maxr_nmulr`,
-    `real_minr_nmulr`, `minr_pmull`, `maxr_pmull`, `real_minr_nmull`, `real_maxr_nmull`,
-    `real_maxrN`, `real_maxNr`, `real_minrN`, `real_minNr`
-- the compatibility module `ssrnum.mc_1_10` was extended to  support definitional
-  compatibility with `min` and `max` which had been lost in `1.11+beta1` for most instances.
-- in `fintype.v`, new lemmas: `seq_sub_default`, `seq_subE`
-- in `order.v`, new "unfolding" lemmas: `minEnat` and `maxEnat`
-
-- in `ssrbool.v`
-  + lemmas about the `cancel` predicate and `{in _, _}`/`{on _, _}` notations:
-    * `onW_can`, `onW_can_in`, `in_onW_can`, `onS_can`, `onS_can_in`, `in_onS_can`
-  + lemmas about the `cancel` predicate and injective functions:
-    * `inj_can_sym_in_on`, `inj_can_sym_on`, `inj_can_sym_in`
-
 ### Changed
 
-- in `order.v`, `le_xor_gt`, `lt_xor_ge`, `compare`, `incompare`, `lel_xor_gt`,
-  `ltl_xor_ge`, `comparel`, `incomparel` have more parameters, so that the
-  the following now deal with `min` and `max`
-  + `comparable_ltgtP`, `comparable_leP`, `comparable_ltP`, `comparableP`
-  + `lcomparableP`, `lcomparable_ltgtP`, `lcomparable_leP`, `lcomparable_ltP`, `ltgtP`
-- in `order.v`:
-  + `[arg min_(i < i0 | P) M]` now for `porderType` (was for `orderType`)
-  + `[arg max_(i < i0 | P) M]` now for `porderType` (was for `orderType`)
-  + added `comparable_arg_minP`,  `comparable_arg_maxP`,  `real_arg_minP`,  `real_arg_maxP`,
-    in order to take advantage of the former generalizations.
-- in `ssrnum.v`, `maxr` is a notation for `(@Order.max ring_display _)` (was `Order.join`)
-  (resp. `minr` is a notation for `(@Order.min ring_display _)`)
-- in `ssrnum.v`, `ler_xor_gt`, `ltr_xor_ge`, `comparer`,
-  `ger0_xor_lt0`, `ler0_xor_gt0`, `comparer0` have now more parameters, so that
-  the following now deal with min and max:
-  + `real_leP`, `real_ltP x y`, `real_ltgtP`, `real_ge0P`, `real_le0P`, `real_ltgt0P`
-  + `lerP`, `ltrP`, `ltrgtP`, `ger0P`, `ler0P`, `ltrgt0P`
-- in `ssrnum.v`, the following have been restated (which were formerly derived from
-  `order.v` and stated with specializations of the `meet` and `join` operators):
-   + `minrC`, `minrr`, `minr_l`, `minr_r`, `maxrC`, `maxrr`, `maxr_l`,
-     `maxr_r`, `minrA`, `minrCA`, `minrAC`, `maxrA`, `maxrCA`, `maxrAC`
-   + `eqr_minl`, `eqr_minr`, `eqr_maxl`, `eqr_maxr`, `ler_minr`, `ler_minl`,
-     `ler_maxr`, `ler_maxl`, `ltr_minr`, `ltr_minl`, `ltr_maxr`, `ltr_maxl`
-   + `minrK`, `minKr`, `maxr_minl`, `maxr_minr`, `minr_maxl`, `minr_maxr`
-- The new definitions of `min` and `max` may require the following rewrite rules
-  changes when dealing with `max` and `min` instead of `meet` and `join`:
-  + `ltexI` -> `(le_minr,lt_minr)`
-  + `lteIx` -> `(le_minl,lt_minl)`
-  + `ltexU` -> `(le_maxr,lt_maxr)`
-  + `lteUx` -> `(le_maxl,lt_maxl)`
-  + `lexU` -> `le_maxr`
-  + `ltxU` -> `lt_maxr`
-  + `lexU` -> `le_maxr`
-
-- in `ssrbool.v`
-  + lemmas about monotone functions and the `{in _, _}` notation:
-    * `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`, `monoRL_in`, `can_mono_in`
-
 ### Renamed
 
-- in `fintype` we deprecate and rename the following:
-  + `arg_minP` -> `arg_minnP`
-  + `arg_maxP` -> `arg_maxnP`
-
-- in `order.v`, in module `NatOrder`, renamings:
-  + `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat`,
-    `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat`
-
 ### Removed
 
-- in `order.v`, removed `total_display` (was used to provide the notation
-  `max` for `join` and `min` for `meet`).
-- in `order.v`, removed `minnE` and `maxnE`
-- in `order.v`,
-  + removed `meetEnat` (in favor of `meetEtotal` followed by `minEnat`)
-  + removed `joinEnat` (in favor of `joinEtotal` followed by `maxEnat`).
-
 ### Infrastructure
 
 ### Misc