tentative changelog

- mostly gathered the changes from previous commits
- add `minrC`
- minor doc addition to `order.v`

CHANGELOG_UNRELEASED.md

@@ -10,12 +10,95 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ### Added
 
++ in `order.v`, theory about for min and max
+  ```
+  Definition min x y := if x < y then x else y.
+  Definition max x y := if x < y then y else x.
+  ...
+  Definition meet := @min _ T.
+  Definition join := @max _ T.
+  ```
+  + Lemmas: `min_l`, `min_r`, `max_l`, `max_r`, `minxx`, `maxxx`,
+    `eq_minl`, `eq_maxr`, `comparable_minl`, `comparable_minr`,
+    `comparable_maxl`, `comparable_maxr`
+  + Lemmas under condition `x >=< y`:
+    `comparable_minC`, `comparable_maxC`, `comparable_eq_minr`, `comparable_eq_maxl`,
+    `comparable_le_minr`, `comparable_le_minl`, `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`
+  + Lemmas under conditions  x >=< y x >=< z y >=< z:
+    `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`
+  + Lemmas about interaction with lattice operations:
+    `meetEtotal`, `joinEtotal`, `minC`, `maxC`, `minA`, `maxA`, `minAC`, `maxAC`,
+    `minCA`, `maxCA`, `minACA`, `maxACA`, `eq_minr`, `eq_maxl`, `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 `order.v`:
+  + in module `NatOrder`, added `nat_display` (instead of the now removed `total_display`)
+  + in module `BoolOrder`, added `bool_display` (instead of the now removed `total_display`)
+- in `ssrnum.v`, theory about min anx max:
+  + 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`
+- in `ssrnum.v`,
+  + new lemma: `comparable0r`
+  + in module `NumIntegralDomainTheory`:
+    ```
+    Definition minr x y := if x <= y then x else y.
+    Definition maxr x y := if x <= y then y else x.
+    ```
+- in `fintype.v`, new lemmas: `seq_sub_default`, `seq_subE`
+
 ### Changed
 
+- in `order.v`, `le_xor_gt`, `lt_xor_ge`, `compare`, `incompare`, `lel_xor_gt`,
+  `ltl_xor_ge`, `comparel`, `incomparel` have more parameters
+  + 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 minr_(i < i0 | P) M]` now for `porderType` (was for `orderType`)
+- 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
+  + 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`:
+  + `oppr_min` now restricted to the real subset
+  + the following have been redefined (were before derived from
+    `order.v` with `meet` and `join` lemmas):
+    * `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`
+
 ### Renamed
 
+- The added theories of min and max cause the following renamings:
+  + `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 `order.v`, in module `NatOrder`, renamings:
+  + `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat`,
+    `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat`
+
 ### Removed
 
+- in `order.v`, removed `total_display` (was defining `max` using
+  `join` and `min` using `meet`)
+- in `order.v`, removed `minnE` and `maxnE`
+
 ### Infrastructure
 
 ### Misc

mathcomp/algebra/ssrnum.v

@@ -5551,6 +5551,7 @@ Ltac mexact x := by mapply x.
 Local Notation min := minr.
 Local Notation max := maxr.
 
+Lemma minrC : @commutative R R min. Proof. mexact @minC. Qed.
 Lemma minrr : @idempotent R min. Proof. mexact @minxx. Qed.
 Lemma minr_l x y : x <= y -> min x y = x. Proof. mexact @min_l. Qed.
 Lemma minr_r x y : y <= x -> min x y = y. Proof. mexact @min_r. Qed.

mathcomp/ssreflect/order.v

@@ -74,6 +74,8 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 (* For x, y of type T, where T is canonically a porderType d:                 *)
 (*            x <= y <-> x is less than or equal to y.                        *)
 (*             x < y <-> x is less than y (:= (y != x) && (x <= y)).          *)
+(*           min x y <-> if x < y then x else y                               *)
+(*           max x y <-> if x < y then y else x                               *)
 (*            x >= y <-> x is greater than or equal to y (:= y <= x).         *)
 (*             x > y <-> x is greater than y (:= y < x).                      *)
 (*   x <= y ?= iff C <-> x is less than y, or equal iff C is true.            *)