diff options
| author | affeldt-aist | 2020-06-06 10:09:23 +0200 |
|---|---|---|
| committer | GitHub | 2020-06-06 10:09:23 +0200 |
| commit | 258f7f981174f0681bd089476706675fbd331a88 (patch) | |
| tree | 7e376f55fccf99a5a45b67ce346c9351c92ae3f0 | |
| parent | 43459547cbcd9d7987a083829171a589ba98bf81 (diff) | |
| parent | ccea59192ab383a9a0009d5ac5873e53f115c867 (diff) | |
Merge pull request #516 from CohenCyril/maxr
Generalizing max and min to porderType
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 86 | ||||
| -rw-r--r-- | mathcomp/algebra/interval.v | 8 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 439 | ||||
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/finfield.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/abelian.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 254 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 1007 |
9 files changed, 1191 insertions, 619 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index eb39d33..586b195 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -25,12 +25,98 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + `(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` + ### 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` + ### 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 diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 3ed2825..950546b 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -210,19 +210,19 @@ Proof. by case: b; apply lter_distl. Qed. Lemma lersif_minr : (x <= Num.min y z ?< if b) = (x <= y ?< if b) && (x <= z ?< if b). -Proof. by case: b; rewrite /= ltexI. Qed. +Proof. by case: b; rewrite /= (le_minr, lt_minr). Qed. Lemma lersif_minl : (Num.min y z <= x ?< if b) = (y <= x ?< if b) || (z <= x ?< if b). -Proof. by case: b; rewrite /= lteIx. Qed. +Proof. by case: b; rewrite /= (le_minl, lt_minl). Qed. Lemma lersif_maxr : (x <= Num.max y z ?< if b) = (x <= y ?< if b) || (x <= z ?< if b). -Proof. by case: b; rewrite /= ltexU. Qed. +Proof. by case: b; rewrite /= (le_maxr, lt_maxr). Qed. Lemma lersif_maxl : (Num.max y z <= x ?< if b) = (y <= x ?< if b) && (z <= x ?< if b). -Proof. by case: b; rewrite /= lteUx. Qed. +Proof. by case: b; rewrite /= (le_maxl, lt_maxl). Qed. End LersifOrdered. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 95c40cd..3bae08e 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -84,8 +84,7 @@ From mathcomp Require Import ssralg poly. (* and ><) and lattice operations (meet and join) defined in order.v are *) (* redefined for the ring_display in the ring_scope (%R). 0-ary ordering *) (* symbols for the ring_display have the suffix "%R", e.g., <%R. All the *) -(* other ordering notations are the same as order.v. The meet and join *) -(* operators for the ring_display are Num.min and Num.max. *) +(* other ordering notations are the same as order.v. *) (* *) (* Over these structures, we have the following operations *) (* `|x| == norm of x. *) @@ -389,10 +388,10 @@ Notation "@ 'lerif' R" := (@Order.leif ring_display R) Notation comparabler := (@Order.comparable ring_display _) (only parsing). Notation "@ 'comparabler' R" := (@Order.comparable ring_display R) (at level 10, R at level 8, only parsing) : fun_scope. -Notation maxr := (@Order.join ring_display _). +Notation maxr := (@Order.max ring_display _). Notation "@ 'maxr' R" := (@Order.join ring_display R) (at level 10, R at level 8, only parsing) : fun_scope. -Notation minr := (@Order.meet ring_display _). +Notation minr := (@Order.min ring_display _). Notation "@ 'minr' R" := (@Order.meet ring_display R) (at level 10, R at level 8, only parsing) : fun_scope. @@ -1550,6 +1549,8 @@ Definition subr_cp0 := (subr_lte0, subr_gte0). (* Comparability in a numDomain *) +Lemma comparable0r x : (0 >=< x)%R = (x \is Num.real). Proof. by []. Qed. + Lemma comparabler0 x : (x >=< 0)%R = (x \is Num.real). Proof. by rewrite comparable_sym. Qed. @@ -1676,11 +1677,7 @@ Lemma ler_leVge x y : x <= 0 -> y <= 0 -> (x <= y) || (y <= x). Proof. by rewrite -!oppr_ge0 => /(ger_leVge _) h /h; rewrite !ler_opp2. Qed. Lemma real_leVge x y : x \is real -> y \is real -> (x <= y) || (y <= x). -Proof. -rewrite !realE; have [x_ge0 _|x_nge0 /= x_le0] := boolP (_ <= _); last first. - by have [/(le_trans x_le0)->|_ /(ler_leVge x_le0) //] := boolP (0 <= _). -by have [/(ger_leVge x_ge0)|_ /le_trans->] := boolP (0 <= _); rewrite ?orbT. -Qed. +Proof. by rewrite -comparabler0 -comparable0r => /comparabler_trans P/P. Qed. Lemma real_comparable x y : x \is real -> y \is real -> x >=< y. Proof. exact: real_leVge. Qed. @@ -1699,35 +1696,37 @@ Proof. exact: rpredD. Qed. (* dichotomy and trichotomy *) -Variant ler_xor_gt (x y : R) : R -> R -> bool -> bool -> Set := - | LerNotGt of x <= y : ler_xor_gt x y (y - x) (y - x) true false - | GtrNotLe of y < x : ler_xor_gt x y (x - y) (x - y) false true. +Variant ler_xor_gt (x y : R) : R -> R -> R -> R -> R -> R -> + bool -> bool -> Set := + | LerNotGt of x <= y : ler_xor_gt x y x x y y (y - x) (y - x) true false + | GtrNotLe of y < x : ler_xor_gt x y y y x x (x - y) (x - y) false true. -Variant ltr_xor_ge (x y : R) : R -> R -> bool -> bool -> Set := - | LtrNotGe of x < y : ltr_xor_ge x y (y - x) (y - x) false true - | GerNotLt of y <= x : ltr_xor_ge x y (x - y) (x - y) true false. +Variant ltr_xor_ge (x y : R) : R -> R -> R -> R -> R -> R -> + bool -> bool -> Set := + | LtrNotGe of x < y : ltr_xor_ge x y x x y y (y - x) (y - x) false true + | GerNotLt of y <= x : ltr_xor_ge x y y y x x (x - y) (x - y) true false. -Variant comparer x y : R -> R -> - bool -> bool -> bool -> bool -> bool -> bool -> Set := - | ComparerLt of x < y : comparer x y (y - x) (y - x) +Variant comparer x y : R -> R -> R -> R -> R -> R -> + bool -> bool -> bool -> bool -> bool -> bool -> Set := + | ComparerLt of x < y : comparer x y x x y y (y - x) (y - x) false false false true false true - | ComparerGt of x > y : comparer x y (x - y) (x - y) + | ComparerGt of x > y : comparer x y y y x x (x - y) (x - y) false false true false true false - | ComparerEq of x = y : comparer x y 0 0 + | ComparerEq of x = y : comparer x y x x x x 0 0 true true true true false false. -Lemma real_leP x y : - x \is real -> y \is real -> - ler_xor_gt x y `|x - y| `|y - x| (x <= y) (y < x). +Lemma real_leP x y : x \is real -> y \is real -> + ler_xor_gt x y (min y x) (min x y) (max y x) (max x y) + `|x - y| `|y - x| (x <= y) (y < x). Proof. move=> xR yR; case: (comparable_leP (real_leVge xR yR)) => xy. - by rewrite [`|x - y|]distrC !ger0_norm ?subr_cp0 //; constructor. - by rewrite [`|y - x|]distrC !gtr0_norm ?subr_cp0 //; constructor. Qed. -Lemma real_ltP x y : - x \is real -> y \is real -> - ltr_xor_ge x y `|x - y| `|y - x| (y <= x) (x < y). +Lemma real_ltP x y : x \is real -> y \is real -> + ltr_xor_ge x y (min y x) (min x y) (max y x) (max x y) + `|x - y| `|y - x| (y <= x) (x < y). Proof. by move=> xR yR; case: real_leP=> //; constructor. Qed. Lemma real_ltNge : {in real &, forall x y, (x < y) = ~~ (y <= x)}. @@ -1737,46 +1736,52 @@ Lemma real_leNgt : {in real &, forall x y, (x <= y) = ~~ (y < x)}. Proof. by move=> x y xR yR /=; case: real_leP. Qed. Lemma real_ltgtP x y : x \is real -> y \is real -> - comparer x y `|x - y| `|y - x| - (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y). + comparer x y (min y x) (min x y) (max y x) (max x y) `|x - y| `|y - x| + (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y). Proof. -move=> xR yR; case: (comparable_ltgtP (real_leVge xR yR)) => [?|?|->]. -- by rewrite [`|x - y|]distrC !gtr0_norm ?subr_gt0//; constructor. +move=> xR yR; case: (comparable_ltgtP (real_leVge yR xR)) => [?|?|->]. - by rewrite [`|y - x|]distrC !gtr0_norm ?subr_gt0//; constructor. +- by rewrite [`|x - y|]distrC !gtr0_norm ?subr_gt0//; constructor. - by rewrite subrr normr0; constructor. Qed. -Variant ger0_xor_lt0 (x : R) : R -> bool -> bool -> Set := - | Ger0NotLt0 of 0 <= x : ger0_xor_lt0 x x false true - | Ltr0NotGe0 of x < 0 : ger0_xor_lt0 x (- x) true false. +Variant ger0_xor_lt0 (x : R) : R -> R -> R -> R -> R -> + bool -> bool -> Set := + | Ger0NotLt0 of 0 <= x : ger0_xor_lt0 x 0 0 x x x false true + | Ltr0NotGe0 of x < 0 : ger0_xor_lt0 x x x 0 0 (- x) true false. -Variant ler0_xor_gt0 (x : R) : R -> bool -> bool -> Set := - | Ler0NotLe0 of x <= 0 : ler0_xor_gt0 x (- x) false true - | Gtr0NotGt0 of 0 < x : ler0_xor_gt0 x x true false. +Variant ler0_xor_gt0 (x : R) : R -> R -> R -> R -> R -> + bool -> bool -> Set := + | Ler0NotLe0 of x <= 0 : ler0_xor_gt0 x x x 0 0 (- x) false true + | Gtr0NotGt0 of 0 < x : ler0_xor_gt0 x 0 0 x x x true false. -Variant comparer0 x : - R -> bool -> bool -> bool -> bool -> bool -> bool -> Set := - | ComparerGt0 of 0 < x : comparer0 x x false false false true false true - | ComparerLt0 of x < 0 : comparer0 x (- x) false false true false true false - | ComparerEq0 of x = 0 : comparer0 x 0 true true true true false false. +Variant comparer0 x : R -> R -> R -> R -> R -> + bool -> bool -> bool -> bool -> bool -> bool -> Set := + | ComparerGt0 of 0 < x : comparer0 x 0 0 x x x false false false true false true + | ComparerLt0 of x < 0 : comparer0 x x x 0 0 (- x) false false true false true false + | ComparerEq0 of x = 0 : comparer0 x 0 0 0 0 0 true true true true false false. -Lemma real_ge0P x : x \is real -> ger0_xor_lt0 x `|x| (x < 0) (0 <= x). +Lemma real_ge0P x : x \is real -> ger0_xor_lt0 x + (min 0 x) (min x 0) (max 0 x) (max x 0) + `|x| (x < 0) (0 <= x). Proof. -move=> hx; rewrite -{2}[x]subr0; case: real_ltP; +move=> hx; rewrite -[X in `|X|]subr0; case: real_leP; by rewrite ?subr0 ?sub0r //; constructor. Qed. -Lemma real_le0P x : x \is real -> ler0_xor_gt0 x `|x| (0 < x) (x <= 0). +Lemma real_le0P x : x \is real -> ler0_xor_gt0 x + (min 0 x) (min x 0) (max 0 x) (max x 0) + `|x| (0 < x) (x <= 0). Proof. -move=> hx; rewrite -{2}[x]subr0; case: real_ltP; +move=> hx; rewrite -[X in `|X|]subr0; case: real_ltP; by rewrite ?subr0 ?sub0r //; constructor. Qed. -Lemma real_ltgt0P x : - x \is real -> - comparer0 x `|x| (0 == x) (x == 0) (x <= 0) (0 <= x) (x < 0) (x > 0). +Lemma real_ltgt0P x : x \is real -> + comparer0 x (min 0 x) (min x 0) (max 0 x) (max x 0) + `|x| (0 == x) (x == 0) (x <= 0) (0 <= x) (x < 0) (x > 0). Proof. -move=> hx; rewrite -{2}[x]subr0; case: real_ltgtP; +move=> hx; rewrite -[X in `|X|]subr0; case: (@real_ltgtP 0 x); by rewrite ?subr0 ?sub0r //; constructor. Qed. @@ -2766,6 +2771,129 @@ Proof. by rewrite -invr_gt1 ?invr_gt0 ?unitrV // invrK. Qed. Definition invr_lte1 := (invr_le1, invr_lt1). Definition invr_cp1 := (invr_gte1, invr_lte1). +(* max and min *) + +Lemma addr_min_max x y : min x y + max x y = x + y. +Proof. by rewrite /min /max; case: ifP => //; rewrite addrC. Qed. + +Lemma addr_max_min x y : max x y + min x y = x + y. +Proof. by rewrite addrC addr_min_max. Qed. + +Lemma minr_to_max x y : min x y = x + y - max x y. +Proof. by rewrite -[x + y]addr_min_max addrK. Qed. + +Lemma maxr_to_min x y : max x y = x + y - min x y. +Proof. by rewrite -[x + y]addr_max_min addrK. Qed. + +Lemma real_oppr_max : {in real &, {morph -%R : x y / max x y >-> min x y : R}}. +Proof. +move=> x y x_real y_real; rewrite !(fun_if, if_arg) ltr_opp2. +by case: real_ltgtP => // ->. +Qed. + +Lemma real_oppr_min : {in real &, {morph -%R : x y / min x y >-> max x y : R}}. +Proof. +by move=> x y xr yr; rewrite -[RHS]opprK real_oppr_max ?realN// !opprK. +Qed. + +Lemma real_addr_minl : {in real & real & real, @left_distributive R R +%R min}. +Proof. +by move=> x y z xr yr zr; case: (@real_leP (_ + _)); rewrite ?realD//; + rewrite lter_add2; case: real_leP. +Qed. + +Lemma real_addr_minr : {in real & real & real, @right_distributive R R +%R min}. +Proof. by move=> x y z xr yr zr; rewrite !(addrC x) real_addr_minl. Qed. + +Lemma real_addr_maxl : {in real & real & real, @left_distributive R R +%R max}. +Proof. +by move=> x y z xr yr zr; case: (@real_leP (_ + _)); rewrite ?realD//; + rewrite lter_add2; case: real_leP. +Qed. + +Lemma real_addr_maxr : {in real & real & real, @right_distributive R R +%R max}. +Proof. by move=> x y z xr yr zr; rewrite !(addrC x) real_addr_maxl. Qed. + +Lemma minr_pmulr x y z : 0 <= x -> x * min y z = min (x * y) (x * z). +Proof. +have [|x_gt0||->]// := comparableP x; last by rewrite !mul0r minxx. +by rewrite !(fun_if, if_arg) lter_pmul2l//; case: (y < z). +Qed. + +Lemma maxr_pmulr x y z : 0 <= x -> x * max y z = max (x * y) (x * z). +Proof. +have [|x_gt0||->]// := comparableP x; last by rewrite !mul0r maxxx. +by rewrite !(fun_if, if_arg) lter_pmul2l//; case: (y < z). +Qed. + +Lemma real_maxr_nmulr x y z : x <= 0 -> y \is real -> z \is real -> + x * max y z = min (x * y) (x * z). +Proof. +move=> x0 yr zr; rewrite -[_ * _]opprK -mulrN real_oppr_max// -mulNr. +by rewrite minr_pmulr ?oppr_ge0// !(mulNr, mulrN, opprK). +Qed. + +Lemma real_minr_nmulr x y z : x <= 0 -> y \is real -> z \is real -> + x * min y z = max (x * y) (x * z). +Proof. +move=> x0 yr zr; rewrite -[_ * _]opprK -mulrN real_oppr_min// -mulNr. +by rewrite maxr_pmulr ?oppr_ge0// !(mulNr, mulrN, opprK). +Qed. + +Lemma minr_pmull x y z : 0 <= x -> min y z * x = min (y * x) (z * x). +Proof. by move=> *; rewrite mulrC minr_pmulr // ![_ * x]mulrC. Qed. + +Lemma maxr_pmull x y z : 0 <= x -> max y z * x = max (y * x) (z * x). +Proof. by move=> *; rewrite mulrC maxr_pmulr // ![_ * x]mulrC. Qed. + +Lemma real_minr_nmull x y z : x <= 0 -> y \is real -> z \is real -> + min y z * x = max (y * x) (z * x). +Proof. by move=> *; rewrite mulrC real_minr_nmulr // ![_ * x]mulrC. Qed. + +Lemma real_maxr_nmull x y z : x <= 0 -> y \is real -> z \is real -> + max y z * x = min (y * x) (z * x). +Proof. by move=> *; rewrite mulrC real_maxr_nmulr // ![_ * x]mulrC. Qed. + +Lemma real_maxrN x : x \is real -> max x (- x) = `|x|. +Proof. +move=> x_real; rewrite /max. +by case: real_ge0P => // [/ge0_cp [] | /lt0_cp []]; + case: (@real_leP (- x) x); rewrite ?realN. +Qed. + +Lemma real_maxNr x : x \is real -> max (- x) x = `|x|. +Proof. +by move=> x_real; rewrite comparable_maxC ?real_maxrN ?real_comparable ?realN. +Qed. + +Lemma real_minrN x : x \is real -> min x (- x) = - `|x|. +Proof. +by move=> x_real; rewrite -[LHS]opprK real_oppr_min ?opprK ?real_maxNr ?realN. +Qed. + +Lemma real_minNr x : x \is real -> min (- x) x = - `|x|. +Proof. +by move=> x_real; rewrite -[LHS]opprK real_oppr_min ?opprK ?real_maxrN ?realN. +Qed. + +Section RealDomainArgExtremum. + +Context {I : finType} (i0 : I). +Context (P : pred I) (F : I -> R) (Pi0 : P i0). +Hypothesis F_real : {in P, forall i, F i \is real}. + +Lemma real_arg_minP : extremum_spec <=%R P F [arg min_(i < i0 | P i) F i]. +Proof. +by apply: comparable_arg_minP => // i j iP jP; rewrite real_comparable ?F_real. +Qed. + +Lemma real_arg_maxP : extremum_spec >=%R P F [arg max_(i > i0 | P i) F i]. +Proof. +by apply: comparable_arg_maxP => // i j iP jP; rewrite real_comparable ?F_real. +Qed. + +End RealDomainArgExtremum. + (* norm *) Lemma real_ler_norm x : x \is real -> x <= `|x|. @@ -3594,25 +3722,30 @@ Implicit Types x y z t : R. Lemma num_real x : x \is real. Proof. exact: num_real. Qed. Hint Resolve num_real : core. -Lemma lerP x y : ler_xor_gt x y `|x - y| `|y - x| (x <= y) (y < x). +Lemma lerP x y : ler_xor_gt x y (min y x) (min x y) (max y x) (max x y) + `|x - y| `|y - x| (x <= y) (y < x). Proof. exact: real_leP. Qed. -Lemma ltrP x y : ltr_xor_ge x y `|x - y| `|y - x| (y <= x) (x < y). +Lemma ltrP x y : ltr_xor_ge x y (min y x) (min x y) (max y x) (max x y) + `|x - y| `|y - x| (y <= x) (x < y). Proof. exact: real_ltP. Qed. Lemma ltrgtP x y : - comparer x y `|x - y| `|y - x| (y == x) (x == y) + comparer x y (min y x) (min x y) (max y x) (max x y) + `|x - y| `|y - x| (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) . Proof. exact: real_ltgtP. Qed. -Lemma ger0P x : ger0_xor_lt0 x `|x| (x < 0) (0 <= x). +Lemma ger0P x : ger0_xor_lt0 x (min 0 x) (min x 0) (max 0 x) (max x 0) + `|x| (x < 0) (0 <= x). Proof. exact: real_ge0P. Qed. -Lemma ler0P x : ler0_xor_gt0 x `|x| (0 < x) (x <= 0). +Lemma ler0P x : ler0_xor_gt0 x (min 0 x) (min x 0) (max 0 x) (max x 0) + `|x| (0 < x) (x <= 0). Proof. exact: real_le0P. Qed. -Lemma ltrgt0P x : - comparer0 x `|x| (0 == x) (x == 0) (x <= 0) (0 <= x) (x < 0) (x > 0). +Lemma ltrgt0P x : comparer0 x (min 0 x) (min x 0) (max 0 x) (max x 0) + `|x| (0 == x) (x == 0) (x <= 0) (0 <= x) (x < 0) (x > 0). Proof. exact: real_ltgt0P. Qed. (* sign *) @@ -3862,93 +3995,40 @@ Proof. exact: real_leif_AGM2_scaled. Qed. Section MinMax. -(* GG: Many of the first lemmas hold unconditionally, and others hold for *) -(* the real subset of a general domain. *) - -Lemma addr_min_max x y : min x y + max x y = x + y. -Proof. -case: (lerP x y)=> [| /ltW] hxy; - first by rewrite (meet_idPl hxy) (join_idPl hxy). -by rewrite (meet_idPr hxy) (join_idPr hxy) addrC. -Qed. - -Lemma addr_max_min x y : max x y + min x y = x + y. -Proof. by rewrite addrC addr_min_max. Qed. - -Lemma minr_to_max x y : min x y = x + y - max x y. -Proof. by rewrite -[x + y]addr_min_max addrK. Qed. - -Lemma maxr_to_min x y : max x y = x + y - min x y. -Proof. by rewrite -[x + y]addr_max_min addrK. Qed. - Lemma oppr_max : {morph -%R : x y / max x y >-> min x y : R}. -Proof. -by move=> x y; case: leP; rewrite -lter_opp2 => hxy; - rewrite ?(meet_idPr hxy) ?(meet_idPl (ltW hxy)). -Qed. +Proof. by move=> x y; apply: real_oppr_max. Qed. Lemma oppr_min : {morph -%R : x y / min x y >-> max x y : R}. -Proof. by move=> x y; rewrite -[max _ _]opprK oppr_max !opprK. Qed. +Proof. by move=> x y; apply: real_oppr_min. Qed. Lemma addr_minl : @left_distributive R R +%R min. -Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed. +Proof. by move=> x y z; apply: real_addr_minl. Qed. Lemma addr_minr : @right_distributive R R +%R min. -Proof. by move=> x y z; rewrite !(addrC x) addr_minl. Qed. +Proof. by move=> x y z; apply: real_addr_minr. Qed. Lemma addr_maxl : @left_distributive R R +%R max. -Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed. +Proof. by move=> x y z; apply: real_addr_maxl. Qed. Lemma addr_maxr : @right_distributive R R +%R max. -Proof. by move=> x y z; rewrite !(addrC x) addr_maxl. Qed. - -Lemma minr_pmulr x y z : 0 <= x -> x * min y z = min (x * y) (x * z). -Proof. -case: sgrP=> // hx _; first by rewrite hx !mul0r meetxx. -by case: (leP (_ * _)); rewrite lter_pmul2l //; case: leP. -Qed. +Proof. by move=> x y z; apply: real_addr_maxr. Qed. Lemma minr_nmulr x y z : x <= 0 -> x * min y z = max (x * y) (x * z). -Proof. -move=> hx; rewrite -[_ * _]opprK -mulNr minr_pmulr ?oppr_cp0 //. -by rewrite oppr_min !mulNr !opprK. -Qed. - -Lemma maxr_pmulr x y z : 0 <= x -> x * max y z = max (x * y) (x * z). -Proof. -move=> hx; rewrite -[_ * _]opprK -mulrN oppr_max minr_pmulr //. -by rewrite oppr_min !mulrN !opprK. -Qed. +Proof. by move=> x_le0; apply: real_minr_nmulr. Qed. Lemma maxr_nmulr x y z : x <= 0 -> x * max y z = min (x * y) (x * z). -Proof. -move=> hx; rewrite -[_ * _]opprK -mulrN oppr_max minr_nmulr //. -by rewrite oppr_max !mulrN !opprK. -Qed. - -Lemma minr_pmull x y z : 0 <= x -> min y z * x = min (y * x) (z * x). -Proof. by move=> *; rewrite mulrC minr_pmulr // ![_ * x]mulrC. Qed. +Proof. by move=> x_le0; apply: real_maxr_nmulr. Qed. Lemma minr_nmull x y z : x <= 0 -> min y z * x = max (y * x) (z * x). -Proof. by move=> *; rewrite mulrC minr_nmulr // ![_ * x]mulrC. Qed. - -Lemma maxr_pmull x y z : 0 <= x -> max y z * x = max (y * x) (z * x). -Proof. by move=> *; rewrite mulrC maxr_pmulr // ![_ * x]mulrC. Qed. +Proof. by move=> x_le0; apply: real_minr_nmull. Qed. Lemma maxr_nmull x y z : x <= 0 -> max y z * x = min (y * x) (z * x). -Proof. by move=> *; rewrite mulrC maxr_nmulr // ![_ * x]mulrC. Qed. - -Lemma maxrN x : max x (- x) = `|x|. -Proof. by case: ger0P=> [/ge0_cp [] | /lt0_cp []]; case: (leP (- x) x). Qed. - -Lemma maxNr x : max (- x) x = `|x|. -Proof. by rewrite joinC maxrN. Qed. +Proof. by move=> x_le0; apply: real_maxr_nmull. Qed. -Lemma minrN x : min x (- x) = - `|x|. -Proof. by rewrite -[min _ _]opprK oppr_min opprK maxNr. Qed. - -Lemma minNr x : min (- x) x = - `|x|. -Proof. by rewrite -[min _ _]opprK oppr_min opprK maxrN. Qed. +Lemma maxrN x : max x (- x) = `|x|. Proof. exact: real_maxrN. Qed. +Lemma maxNr x : max (- x) x = `|x|. Proof. exact: real_maxNr. Qed. +Lemma minrN x : min x (- x) = - `|x|. Proof. exact: real_minrN. Qed. +Lemma minNr x : min (- x) x = - `|x|. Proof. exact: real_minNr. Qed. End MinMax. @@ -3959,7 +4039,7 @@ Variable p : {poly R}. Lemma poly_itv_bound a b : {ub | forall x, a <= x <= b -> `|p.[x]| <= ub}. Proof. have [ub le_p_ub] := poly_disk_bound p (Num.max `|a| `|b|). -exists ub => x /andP[le_a_x le_x_b]; rewrite le_p_ub // lexU !ler_normr. +exists ub => x /andP[le_a_x le_x_b]; rewrite le_p_ub // le_maxr !ler_normr. by have [_|_] := ler0P x; rewrite ?ler_opp2 ?le_a_x ?le_x_b orbT. Qed. @@ -5176,7 +5256,15 @@ Module Num. (* revert them in order to compile and commit. This problem will be solved *) (* in Coq 8.10. See also: https://github.com/math-comp/math-comp/pull/270. *) Export ssrnum.Num. -Import ssrnum.Num.Def. + +Module Import Def. +Export ssrnum.Num.Def. +Definition minr {R : numDomainType} (x y : R) := if x <= y then x else y. +Definition maxr {R : numDomainType} (x y : R) := if x <= y then y else x. +End Def. + +Notation min := minr. +Notation max := maxr. Module Import Syntax. Notation "`| x |" := @@ -5543,52 +5631,85 @@ Section RealDomainOperations. Variable R : realDomainType. Implicit Types x y z : R. Section MinMax. -Definition minrC : @commutative R R min := @meetC _ R. -Definition minrr : @idempotent R min := @meetxx _ R. -Definition minr_l x y : x <= y -> min x y = x := @meet_l _ _ x y. -Definition minr_r x y : y <= x -> min x y = y := @meet_r _ _ x y. -Definition maxrC : @commutative R R max := @joinC _ R. -Definition maxrr : @idempotent R max := @joinxx _ R. -Definition maxr_l x y : y <= x -> max x y = x := @join_l _ _ x y. -Definition maxr_r x y : x <= y -> max x y = y := @join_r _ _ x y. -Definition minrA x y z : min x (min y z) = min (min x y) z := meetA x y z. -Definition minrCA : @left_commutative R R min := meetCA. -Definition minrAC : @right_commutative R R min := meetAC. -Definition maxrA x y z : max x (max y z) = max (max x y) z := joinA x y z. -Definition maxrCA : @left_commutative R R max := joinCA. -Definition maxrAC : @right_commutative R R max := joinAC. -Definition eqr_minl x y : (min x y == x) = (x <= y) := eq_meetl x y. -Definition eqr_minr x y : (min x y == y) = (y <= x) := eq_meetr x y. -Definition eqr_maxl x y : (max x y == x) = (y <= x) := eq_joinl x y. -Definition eqr_maxr x y : (max x y == y) = (x <= y) := eq_joinr x y. -Definition ler_minr x y z : (x <= min y z) = (x <= y) && (x <= z) := lexI x y z. -Definition ler_minl x y z : (min y z <= x) = (y <= x) || (z <= x) := leIx x y z. -Definition ler_maxr x y z : (x <= max y z) = (x <= y) || (x <= z) := lexU x y z. -Definition ler_maxl x y z : (max y z <= x) = (y <= x) && (z <= x) := leUx y z x. -Definition ltr_minr x y z : (x < min y z) = (x < y) && (x < z) := ltxI x y z. -Definition ltr_minl x y z : (min y z < x) = (y < x) || (z < x) := ltIx x y z. -Definition ltr_maxr x y z : (x < max y z) = (x < y) || (x < z) := ltxU x y z. -Definition ltr_maxl x y z : (max y z < x) = (y < x) && (z < x) := ltUx x y z. + +Let mrE x y : ((min x y = Order.min x y) * (maxr x y = Order.max x y))%type. +Proof. by rewrite /minr /min /maxr /max; case: comparableP. Qed. +Ltac mapply x := do ?[rewrite !mrE|apply: x|move=> ?]. +Ltac mexact x := by mapply x. + +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. +Lemma maxrC : @commutative R R max. Proof. mexact @maxC. Qed. +Lemma maxrr : @idempotent R max. Proof. mexact @maxxx. Qed. +Lemma maxr_l x y : y <= x -> max x y = x. Proof. mexact @max_l. Qed. +Lemma maxr_r x y : x <= y -> max x y = y. Proof. mexact @max_r. Qed. + +Lemma minrA x y z : min x (min y z) = min (min x y) z. +Proof. mexact @minA. Qed. + +Lemma minrCA : @left_commutative R R min. Proof. mexact @minCA. Qed. +Lemma minrAC : @right_commutative R R min. Proof. mexact @minAC. Qed. +Lemma maxrA x y z : max x (max y z) = max (max x y) z. +Proof. mexact @maxA. Qed. + +Lemma maxrCA : @left_commutative R R max. Proof. mexact @maxCA. Qed. +Lemma maxrAC : @right_commutative R R max. Proof. mexact @maxAC. Qed. +Lemma eqr_minl x y : (min x y == x) = (x <= y). Proof. mexact @eq_minl. Qed. +Lemma eqr_minr x y : (min x y == y) = (y <= x). Proof. mexact @eq_minr. Qed. +Lemma eqr_maxl x y : (max x y == x) = (y <= x). Proof. mexact @eq_maxl. Qed. +Lemma eqr_maxr x y : (max x y == y) = (x <= y). Proof. mexact @eq_maxr. Qed. + +Lemma ler_minr x y z : (x <= min y z) = (x <= y) && (x <= z). +Proof. mexact @le_minr. Qed. + +Lemma ler_minl x y z : (min y z <= x) = (y <= x) || (z <= x). +Proof. mexact @le_minl. Qed. + +Lemma ler_maxr x y z : (x <= max y z) = (x <= y) || (x <= z). +Proof. mexact @le_maxr. Qed. + +Lemma ler_maxl x y z : (max y z <= x) = (y <= x) && (z <= x). +Proof. mexact @le_maxl. Qed. + +Lemma ltr_minr x y z : (x < min y z) = (x < y) && (x < z). +Proof. mexact @lt_minr. Qed. + +Lemma ltr_minl x y z : (min y z < x) = (y < x) || (z < x). +Proof. mexact @lt_minl. Qed. + +Lemma ltr_maxr x y z : (x < max y z) = (x < y) || (x < z). +Proof. mexact @lt_maxr. Qed. + +Lemma ltr_maxl x y z : (max y z < x) = (y < x) && (z < x). +Proof. mexact @lt_maxl. Qed. + Definition lter_minr := (ler_minr, ltr_minr). Definition lter_minl := (ler_minl, ltr_minl). Definition lter_maxr := (ler_maxr, ltr_maxr). Definition lter_maxl := (ler_maxl, ltr_maxl). -Definition minrK x y : max (min x y) x = x := meetUKC y x. -Definition minKr x y : min y (max x y) = y := joinKIC x y. -Definition maxr_minl : @left_distributive R R max min := @joinIl _ R. -Definition maxr_minr : @right_distributive R R max min := @joinIr _ R. -Definition minr_maxl : @left_distributive R R min max := @meetUl _ R. -Definition minr_maxr : @right_distributive R R min max := @meetUr _ R. + +Lemma minrK x y : max (min x y) x = x. Proof. rewrite minrC; mexact @minxK. Qed. +Lemma minKr x y : min y (max x y) = y. Proof. rewrite maxrC; mexact @maxKx. Qed. + +Lemma maxr_minl : @left_distributive R R max min. Proof. mexact @max_minl. Qed. +Lemma maxr_minr : @right_distributive R R max min. Proof. mexact @max_minr. Qed. +Lemma minr_maxl : @left_distributive R R min max. Proof. mexact @min_maxl. Qed. +Lemma minr_maxr : @right_distributive R R min max. Proof. mexact @min_maxr. Qed. + Variant minr_spec x y : bool -> bool -> R -> Type := | Minr_r of x <= y : minr_spec x y true false x | Minr_l of y < x : minr_spec x y false true y. Lemma minrP x y : minr_spec x y (x <= y) (y < x) (min x y). -Proof. by case: leP; constructor. Qed. +Proof. by rewrite mrE; case: leP; constructor. Qed. + Variant maxr_spec x y : bool -> bool -> R -> Type := | Maxr_r of y <= x : maxr_spec x y true false x | Maxr_l of x < y : maxr_spec x y false true y. Lemma maxrP x y : maxr_spec x y (y <= x) (x < y) (max x y). -Proof. by case: (leP y); constructor. Qed. +Proof. by rewrite mrE; case: (leP y); constructor. Qed. + End MinMax. End RealDomainOperations. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 0a759e8..d8ad524 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -505,8 +505,8 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. have /(find_root r.1)[n ub_rp] := xab0; exists n. have [M Mgt0 ubM]: {M | 0 < M & {in Iab_ n, forall a, `|r.2.[a]| <= M}}. have [M ubM] := poly_itv_bound r.2 (ab_ n).1 (ab_ n).2. - exists (Num.max 1 M) => [|s /ubM vM]; first by rewrite ltxU ltr01. - by rewrite lexU orbC vM. + exists (Num.max 1 M) => [|s /ubM vM]; first by rewrite lt_maxr ltr01. + by rewrite le_maxr orbC vM. exists (h2 / M) => [|a xn_a]; first by rewrite divr_gt0 ?invr_gt0 ?ltr0n. rewrite ltr_pdivr_mulr // -(ltr_add2l h2) -mulr2n -mulr_natl divff //. rewrite -normr1 -(hornerC 1 a) -[1%:P]r_pq_1 hornerD. diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index f0d432f..492aed8 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -506,7 +506,7 @@ have [r r_dv_p irr_r]: {r | r %| p & irreducible_poly r}. pose rVp (v : 'rV_n) (r := rVpoly v) := (1 < size r) && (r %| p). have [v0 Dp]: {v0 | rVpoly v0 = p & rVp v0}. by exists (poly_rV p); rewrite /rVp poly_rV_K ?C'p /=. - case/(arg_minP (size \o rVpoly))=> /= v; set r := rVpoly v. + case/(arg_minnP (size \o rVpoly))=> /= v; set r := rVpoly v. case/andP=> C'r r_dv_p min_r; exists r => //; split=> // q C'q q_dv_r. have nz_r: r != 0 by rewrite -size_poly_gt0 ltnW. have le_q_r: size q <= size r by rewrite dvdp_leq. diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 95bc562..3a5caeb 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -264,7 +264,7 @@ Qed. Lemma exponent_witness G : nilpotent G -> {x | x \in G & exponent G = #[x]}. Proof. -move=> nilG; have [//=| /= x Gx max_x] := @arg_maxP _ 1 (mem G) order. +move=> nilG; have [//=| /= x Gx max_x] := @arg_maxnP _ 1 (mem G) order. exists x => //; apply/eqP; rewrite eqn_dvd dvdn_exponent // andbT. apply/dvdn_biglcmP=> y Gy; apply/dvdn_partP=> //= p. rewrite mem_primes => /andP[p_pr _]; have p_gt1: p > 1 := prime_gt1 p_pr. @@ -726,12 +726,12 @@ Qed. Lemma grank_min B : 'm(<<B>>) <= #|B|. Proof. -by rewrite /gen_rank; case: arg_minP => [|_ _ -> //]; rewrite genGid. +by rewrite /gen_rank; case: arg_minnP => [|_ _ -> //]; rewrite genGid. Qed. Lemma grank_witness G : {B | <<B>> = G & #|B| = 'm(G)}. Proof. -rewrite /gen_rank; case: arg_minP => [|B defG _]; first by rewrite genGid. +rewrite /gen_rank; case: arg_minnP => [|B defG _]; first by rewrite genGid. by exists B; first apply/eqP. Qed. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index e35d2c8..de03369 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1888,7 +1888,7 @@ Arguments bigmax_sup [I] i0 [P m F]. Lemma bigmax_eq_arg (I : finType) i0 (P : pred I) F : P i0 -> \max_(i | P i) F i = F [arg max_(i > i0 | P i) F i]. Proof. -move=> Pi0; case: arg_maxP => //= i Pi maxFi. +move=> Pi0; case: arg_maxnP => //= i Pi maxFi. by apply/eqP; rewrite eqn_leq leq_bigmax_cond // andbT; apply/bigmax_leqP. Qed. Arguments bigmax_eq_arg [I] i0 [P F]. @@ -1897,7 +1897,7 @@ Lemma eq_bigmax_cond (I : finType) (A : pred I) F : #|A| > 0 -> {i0 | i0 \in A & \max_(i in A) F i = F i0}. Proof. case: (pickP A) => [i0 Ai0 _ | ]; last by move/eq_card0->. -by exists [arg max_(i > i0 in A) F i]; [case: arg_maxP | apply: bigmax_eq_arg]. +by exists [arg max_(i > i0 in A) F i]; [case: arg_maxnP | apply: bigmax_eq_arg]. Qed. Lemma eq_bigmax (I : finType) F : #|I| > 0 -> {i0 : I | \max_i F i = F i0}. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 67f88a6..abed211 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -1007,108 +1007,6 @@ Notation "'exists_in_ view" := (exists_inPP _ (fun _ => view)) Notation "'forall_in_ view" := (forall_inPP _ (fun _ => view)) (at level 4, right associativity, format "''forall_in_' view"). -Section Extrema. - -Variant extremum_spec {T : eqType} (ord : rel T) {I : finType} - (P : pred I) (F : I -> T) : I -> Type := - ExtremumSpec (i : I) of P i & (forall j : I, P j -> ord (F i) (F j)) : - extremum_spec ord P F i. - -Let arg_pred {T : eqType} ord {I : finType} (P : pred I) (F : I -> T) := - [pred i | P i & [forall (j | P j), ord (F i) (F j)]]. - -Section Extremum. - -Context {T : eqType} {I : finType} (ord : rel T). -Context (i0 : I) (P : pred I) (F : I -> T). - -Hypothesis ord_refl : reflexive ord. -Hypothesis ord_trans : transitive ord. -Hypothesis ord_total : total ord. - -Definition extremum := odflt i0 (pick (arg_pred ord P F)). - -Hypothesis Pi0 : P i0. - -Lemma extremumP : extremum_spec ord P F extremum. -Proof. -rewrite /extremum; case: pickP => [i /andP[Pi /'forall_implyP/= min_i] | no_i]. - by split=> // j; apply/implyP. -have := sort_sorted ord_total [seq F i | i <- enum P]. -set s := sort _ _ => ss; have s_gt0 : size s > 0 - by rewrite size_sort size_map -cardE; apply/card_gt0P; exists i0. -pose t0 := nth (F i0) s 0; have: t0 \in s by rewrite mem_nth. -rewrite mem_sort => /mapP/sig2_eqW[it0]; rewrite mem_enum => it0P def_t0. -have /negP[/=] := no_i it0; rewrite [P _]it0P/=; apply/'forall_implyP=> j Pj. -have /(nthP (F i0))[k g_lt <-] : F j \in s by rewrite mem_sort map_f ?mem_enum. -by rewrite -def_t0 sorted_le_nth. -Qed. - -End Extremum. - -Notation "[ 'arg[' ord ]_( i < i0 | P ) F ]" := - (extremum ord i0 (fun i => P%B) (fun i => F)) - (at level 0, ord, i, i0 at level 10, - format "[ 'arg[' ord ]_( i < i0 | P ) F ]") : nat_scope. - -Notation "[ 'arg[' ord ]_( i < i0 'in' A ) F ]" := - [arg[ord]_(i < i0 | i \in A) F] - (at level 0, ord, i, i0 at level 10, - format "[ 'arg[' ord ]_( i < i0 'in' A ) F ]") : nat_scope. - -Notation "[ 'arg[' ord ]_( i < i0 ) F ]" := [arg[ord]_(i < i0 | true) F] - (at level 0, ord, i, i0 at level 10, - format "[ 'arg[' ord ]_( i < i0 ) F ]") : nat_scope. - -Section ArgMinMax. - -Variables (I : finType) (i0 : I) (P : pred I) (F : I -> nat) (Pi0 : P i0). - -Definition arg_min := extremum leq i0 P F. -Definition arg_max := extremum geq i0 P F. - -Lemma arg_minP : extremum_spec leq P F arg_min. -Proof. by apply: extremumP => //; [apply: leq_trans|apply: leq_total]. Qed. - -Lemma arg_maxP : extremum_spec geq P F arg_max. -Proof. -apply: extremumP => //; first exact: leqnn. - by move=> n m p mn np; apply: leq_trans mn. -by move=> ??; apply: leq_total. -Qed. - -End ArgMinMax. - -End Extrema. - -Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := - (arg_min i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'min_' ( i < i0 | P ) F ]") : nat_scope. - -Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" := - [arg min_(i < i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'min_' ( i < i0 'in' A ) F ]") : nat_scope. - -Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'min_' ( i < i0 ) F ]") : nat_scope. - -Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" := - (arg_max i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'max_' ( i > i0 | P ) F ]") : nat_scope. - -Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" := - [arg max_(i > i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'max_' ( i > i0 'in' A ) F ]") : nat_scope. - -Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'max_' ( i > i0 ) F ]") : nat_scope. - (**********************************************************************) (* *) (* Boolean injectivity test for functions with a finType domain *) @@ -1614,6 +1512,20 @@ Definition adhoc_seq_sub_finType := End SeqSubType. +Section SeqReplace. +Variables (T : eqType). +Implicit Types (s : seq T). + +Lemma seq_sub_default s : size s > 0 -> seq_sub s. +Proof. by case: s => // x s _; exists x; rewrite mem_head. Qed. + +Lemma seq_subE s (s_gt0 : size s > 0) : + s = map val (map (insubd (seq_sub_default s_gt0)) s : seq (seq_sub s)). +Proof. by rewrite -map_comp map_id_in// => x x_in_s /=; rewrite insubdK. Qed. + +End SeqReplace. +Notation in_sub_seq s_gt0 := (insubd (seq_sub_default s_gt0)). + Section SeqFinType. Variables (T : choiceType) (s : seq T). @@ -1634,6 +1546,144 @@ Qed. End SeqFinType. +Section Extrema. + +Variant extremum_spec {T : eqType} (ord : rel T) {I : finType} + (P : pred I) (F : I -> T) : I -> Type := + ExtremumSpec (i : I) of P i & (forall j : I, P j -> ord (F i) (F j)) : + extremum_spec ord P F i. + +Let arg_pred {T : eqType} ord {I : finType} (P : pred I) (F : I -> T) := + [pred i | P i & [forall (j | P j), ord (F i) (F j)]]. + +Section Extremum. + +Context {T : eqType} {I : finType} (ord : rel T). +Context (i0 : I) (P : pred I) (F : I -> T). + +Definition extremum := odflt i0 (pick (arg_pred ord P F)). + +Hypothesis ord_refl : reflexive ord. +Hypothesis ord_trans : transitive ord. +Hypothesis ord_total : total ord. +Hypothesis Pi0 : P i0. + +Lemma extremumP : extremum_spec ord P F extremum. +Proof. +rewrite /extremum; case: pickP => [i /andP[Pi /'forall_implyP/= min_i] | no_i]. + by split=> // j; apply/implyP. +have := sort_sorted ord_total [seq F i | i <- enum P]. +set s := sort _ _ => ss; have s_gt0 : size s > 0 + by rewrite size_sort size_map -cardE; apply/card_gt0P; exists i0. +pose t0 := nth (F i0) s 0; have: t0 \in s by rewrite mem_nth. +rewrite mem_sort => /mapP/sig2_eqW[it0]; rewrite mem_enum => it0P def_t0. +have /negP[/=] := no_i it0; rewrite [P _]it0P/=; apply/'forall_implyP=> j Pj. +have /(nthP (F i0))[k g_lt <-] : F j \in s by rewrite mem_sort map_f ?mem_enum. +by rewrite -def_t0 sorted_le_nth. +Qed. + +End Extremum. + +Section ExtremumIn. + +Context {T : eqType} {I : finType} (ord : rel T). +Context (i0 : I) (P : pred I) (F : I -> T). + +Hypothesis ord_refl : {in P, reflexive (relpre F ord)}. +Hypothesis ord_trans : {in P & P & P, transitive (relpre F ord)}. +Hypothesis ord_total : {in P &, total (relpre F ord)}. +Hypothesis Pi0 : P i0. + +Lemma extremum_inP : extremum_spec ord P F (extremum ord i0 P F). +Proof. +rewrite /extremum; case: pickP => [i /andP[Pi /'forall_implyP/= min_i] | no_i]. + by split=> // j; apply/implyP. +pose TP := seq_sub [seq F i | i <- enum P]. +have FPP (iP : {i | P i}) : F (proj1_sig iP) \in [seq F i | i <- enum P]. + by rewrite map_f// mem_enum; apply: valP. +pose FP := SeqSub (FPP _). +have []//= := @extremumP _ _ (relpre val ord) (exist P i0 Pi0) xpredT FP. +- by move=> [/= _/mapP[i iP ->]]; apply: ord_refl; rewrite mem_enum in iP. +- move=> [/= _/mapP[j jP ->]] [/= _/mapP[i iP ->]] [/= _/mapP[k kP ->]]. + by apply: ord_trans; rewrite !mem_enum in iP jP kP. +- move=> [/= _/mapP[i iP ->]] [/= _/mapP[j jP ->]]. + by apply: ord_total; rewrite !mem_enum in iP jP. +- rewrite /FP => -[/= i Pi] _ /(_ (exist _ _ _))/= ordF. + have /negP/negP/= := no_i i; rewrite Pi/= negb_forall => /existsP/sigW[j]. + by rewrite negb_imply => /andP[Pj]; rewrite ordF. +Qed. + +End ExtremumIn. + +Notation "[ 'arg[' ord ]_( i < i0 | P ) F ]" := + (extremum ord i0 (fun i => P%B) (fun i => F)) + (at level 0, ord, i, i0 at level 10, + format "[ 'arg[' ord ]_( i < i0 | P ) F ]") : nat_scope. + +Notation "[ 'arg[' ord ]_( i < i0 'in' A ) F ]" := + [arg[ord]_(i < i0 | i \in A) F] + (at level 0, ord, i, i0 at level 10, + format "[ 'arg[' ord ]_( i < i0 'in' A ) F ]") : nat_scope. + +Notation "[ 'arg[' ord ]_( i < i0 ) F ]" := [arg[ord]_(i < i0 | true) F] + (at level 0, ord, i, i0 at level 10, + format "[ 'arg[' ord ]_( i < i0 ) F ]") : nat_scope. + +Section ArgMinMax. + +Variables (I : finType) (i0 : I) (P : pred I) (F : I -> nat) (Pi0 : P i0). + +Definition arg_min := extremum leq i0 P F. +Definition arg_max := extremum geq i0 P F. + +Lemma arg_minnP : extremum_spec leq P F arg_min. +Proof. by apply: extremumP => //; [apply: leq_trans|apply: leq_total]. Qed. + +Lemma arg_maxnP : extremum_spec geq P F arg_max. +Proof. +apply: extremumP => //; first exact: leqnn. + by move=> n m p mn np; apply: leq_trans mn. +by move=> ??; apply: leq_total. +Qed. + +End ArgMinMax. + +End Extrema. + +Notation "@ 'arg_minP'" := + (deprecate arg_minP arg_minnP) (at level 10, only parsing) : fun_scope. +Notation arg_minP := (@arg_minP _ _ _) (only parsing). +Notation "@ 'arg_maxP'" := + (deprecate arg_maxP arg_maxnP) (at level 10, only parsing) : fun_scope. +Notation arg_maxP := (@arg_maxP _ _ _) (only parsing). + +Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := + (arg_min i0 (fun i => P%B) (fun i => F)) + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 | P ) F ]") : nat_scope. + +Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" := + [arg min_(i < i0 | i \in A) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 'in' A ) F ]") : nat_scope. + +Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 ) F ]") : nat_scope. + +Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" := + (arg_max i0 (fun i => P%B) (fun i => F)) + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 | P ) F ]") : nat_scope. + +Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" := + [arg max_(i > i0 | i \in A) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 'in' A ) F ]") : nat_scope. + +Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 ) F ]") : nat_scope. (**********************************************************************) (* *) diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index b907527..10a26f1 100644 --- a/mathcomp/ssreflect/order.v +++ b/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. *) @@ -186,24 +188,25 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* input for the inference. *) (* *) (* Existing displays are either dual_display d (where d is a display), *) -(* dvd_display (both explained above), total_display (to overload meet and *) -(* join using min and max) ring_display (from algebra/ssrnum to change the *) -(* scope of the usual notations to ring_scope). We also provide lexi_display *) -(* and prod_display for lexicographic and product order respectively. *) +(* dvd_display (both explained above), ring_display (from algebra/ssrnum *) +(* to change the scope of the usual notations to ring_scope). We also provide *) +(* lexi_display and prod_display for lexicographic and product order *) +(* respectively. *) (* The default display is tt and users can define their own as explained *) (* above. *) (* *) -(* For orderType we provide the following operations (in total_display) *) -(* [arg minr_(i < i0 | P) M] == a value i : T minimizing M : R, subject to *) +(* For porderType we provide the following operations *) +(* [arg min_(i < i0 | P) M] == a value i : T minimizing M : R, subject to *) (* the condition P (i may appear in P and M), and *) (* provided P holds for i0. *) -(* [arg maxr_(i > i0 | P) M] == a value i maximizing M subject to P and *) +(* [arg max_(i > i0 | P) M] == a value i maximizing M subject to P and *) (* provided P holds for i0. *) (* [arg min_(i < i0 in A) M] == an i \in A minimizing M if i0 \in A. *) (* [arg max_(i > i0 in A) M] == an i \in A maximizing M if i0 \in A. *) (* [arg min_(i < i0) M] == an i : T minimizing M, given i0 : T. *) (* [arg max_(i > i0) M] == an i : T maximizing M, given i0 : T. *) (* with head symbols Order.arg_min and Order.arg_max *) +(* The user may use extremumP or extremum_inP to eliminate them. *) (* *) (* In order to build the above structures, one must provide the appropriate *) (* mixin to the following structure constructors. The list of possible mixins *) @@ -715,6 +718,43 @@ Reserved Notation "\min_ ( i 'in' A ) F" (at level 41, F at level 41, i, A at level 50, format "'[' \min_ ( i 'in' A ) '/ ' F ']'"). +Reserved Notation "\max_ i F" + (at level 41, F at level 41, i at level 0, + format "'[' \max_ i '/ ' F ']'"). +Reserved Notation "\max_ ( i <- r | P ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \max_ ( i <- r | P ) '/ ' F ']'"). +Reserved Notation "\max_ ( i <- r ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \max_ ( i <- r ) '/ ' F ']'"). +Reserved Notation "\max_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \max_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\max_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \max_ ( m <= i < n ) '/ ' F ']'"). +Reserved Notation "\max_ ( i | P ) F" + (at level 41, F at level 41, i at level 50, + format "'[' \max_ ( i | P ) '/ ' F ']'"). +Reserved Notation "\max_ ( i : t | P ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\max_ ( i : t ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\max_ ( i < n | P ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \max_ ( i < n | P ) '/ ' F ']'"). +Reserved Notation "\max_ ( i < n ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \max_ ( i < n ) F ']'"). +Reserved Notation "\max_ ( i 'in' A | P ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \max_ ( i 'in' A | P ) '/ ' F ']'"). +Reserved Notation "\max_ ( i 'in' A ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \max_ ( i 'in' A ) '/ ' F ']'"). + Reserved Notation "\meet^d_ i F" (at level 41, F at level 41, i at level 0, format "'[' \meet^d_ i '/ ' F ']'"). @@ -789,6 +829,80 @@ Reserved Notation "\join^d_ ( i 'in' A ) F" (at level 41, F at level 41, i, A at level 50, format "'[' \join^d_ ( i 'in' A ) '/ ' F ']'"). +Reserved Notation "\min^d_ i F" + (at level 41, F at level 41, i at level 0, + format "'[' \min^d_ i '/ ' F ']'"). +Reserved Notation "\min^d_ ( i <- r | P ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \min^d_ ( i <- r | P ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( i <- r ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \min^d_ ( i <- r ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \min^d_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \min^d_ ( m <= i < n ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( i | P ) F" + (at level 41, F at level 41, i at level 50, + format "'[' \min^d_ ( i | P ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( i : t | P ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\min^d_ ( i : t ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\min^d_ ( i < n | P ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \min^d_ ( i < n | P ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( i < n ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \min^d_ ( i < n ) F ']'"). +Reserved Notation "\min^d_ ( i 'in' A | P ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \min^d_ ( i 'in' A | P ) '/ ' F ']'"). +Reserved Notation "\min^d_ ( i 'in' A ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \min^d_ ( i 'in' A ) '/ ' F ']'"). + +Reserved Notation "\max^d_ i F" + (at level 41, F at level 41, i at level 0, + format "'[' \max^d_ i '/ ' F ']'"). +Reserved Notation "\max^d_ ( i <- r | P ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \max^d_ ( i <- r | P ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( i <- r ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \max^d_ ( i <- r ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \max^d_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \max^d_ ( m <= i < n ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( i | P ) F" + (at level 41, F at level 41, i at level 50, + format "'[' \max^d_ ( i | P ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( i : t | P ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\max^d_ ( i : t ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\max^d_ ( i < n | P ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \max^d_ ( i < n | P ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( i < n ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \max^d_ ( i < n ) F ']'"). +Reserved Notation "\max^d_ ( i 'in' A | P ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \max^d_ ( i 'in' A | P ) '/ ' F ']'"). +Reserved Notation "\max^d_ ( i 'in' A ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \max^d_ ( i 'in' A ) '/ ' F ']'"). + Reserved Notation "\meet^p_ i F" (at level 41, F at level 41, i at level 0, format "'[' \meet^p_ i '/ ' F ']'"). @@ -863,80 +977,6 @@ Reserved Notation "\join^p_ ( i 'in' A ) F" (at level 41, F at level 41, i, A at level 50, format "'[' \join^p_ ( i 'in' A ) '/ ' F ']'"). -Reserved Notation "\min^l_ i F" - (at level 41, F at level 41, i at level 0, - format "'[' \min^l_ i '/ ' F ']'"). -Reserved Notation "\min^l_ ( i <- r | P ) F" - (at level 41, F at level 41, i, r at level 50, - format "'[' \min^l_ ( i <- r | P ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( i <- r ) F" - (at level 41, F at level 41, i, r at level 50, - format "'[' \min^l_ ( i <- r ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( m <= i < n | P ) F" - (at level 41, F at level 41, i, m, n at level 50, - format "'[' \min^l_ ( m <= i < n | P ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( m <= i < n ) F" - (at level 41, F at level 41, i, m, n at level 50, - format "'[' \min^l_ ( m <= i < n ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( i | P ) F" - (at level 41, F at level 41, i at level 50, - format "'[' \min^l_ ( i | P ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). -Reserved Notation "\min^l_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). -Reserved Notation "\min^l_ ( i < n | P ) F" - (at level 41, F at level 41, i, n at level 50, - format "'[' \min^l_ ( i < n | P ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( i < n ) F" - (at level 41, F at level 41, i, n at level 50, - format "'[' \min^l_ ( i < n ) F ']'"). -Reserved Notation "\min^l_ ( i 'in' A | P ) F" - (at level 41, F at level 41, i, A at level 50, - format "'[' \min^l_ ( i 'in' A | P ) '/ ' F ']'"). -Reserved Notation "\min^l_ ( i 'in' A ) F" - (at level 41, F at level 41, i, A at level 50, - format "'[' \min^l_ ( i 'in' A ) '/ ' F ']'"). - -Reserved Notation "\max^l_ i F" - (at level 41, F at level 41, i at level 0, - format "'[' \max^l_ i '/ ' F ']'"). -Reserved Notation "\max^l_ ( i <- r | P ) F" - (at level 41, F at level 41, i, r at level 50, - format "'[' \max^l_ ( i <- r | P ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( i <- r ) F" - (at level 41, F at level 41, i, r at level 50, - format "'[' \max^l_ ( i <- r ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( m <= i < n | P ) F" - (at level 41, F at level 41, i, m, n at level 50, - format "'[' \max^l_ ( m <= i < n | P ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( m <= i < n ) F" - (at level 41, F at level 41, i, m, n at level 50, - format "'[' \max^l_ ( m <= i < n ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( i | P ) F" - (at level 41, F at level 41, i at level 50, - format "'[' \max^l_ ( i | P ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). -Reserved Notation "\max^l_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). -Reserved Notation "\max^l_ ( i < n | P ) F" - (at level 41, F at level 41, i, n at level 50, - format "'[' \max^l_ ( i < n | P ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( i < n ) F" - (at level 41, F at level 41, i, n at level 50, - format "'[' \max^l_ ( i < n ) F ']'"). -Reserved Notation "\max^l_ ( i 'in' A | P ) F" - (at level 41, F at level 41, i, A at level 50, - format "'[' \max^l_ ( i 'in' A | P ) '/ ' F ']'"). -Reserved Notation "\max^l_ ( i 'in' A ) F" - (at level 41, F at level 41, i, A at level 50, - format "'[' \max^l_ ( i 'in' A ) '/ ' F ']'"). - Module Order. (**************) @@ -1032,39 +1072,52 @@ Definition leif (x y : T) C : Prop := ((x <= y) * ((x == y) = C))%type. Definition le_of_leif x y C (le_xy : @leif x y C) := le_xy.1 : le x y. -Variant le_xor_gt (x y : T) : bool -> bool -> Set := - | LeNotGt of x <= y : le_xor_gt x y true false - | GtNotLe of y < x : le_xor_gt x y false true. +Variant le_xor_gt (x y : T) : + T -> T -> T -> T -> bool -> bool -> Set := + | LeNotGt of x <= y : le_xor_gt x y x x y y true false + | GtNotLe of y < x : le_xor_gt x y y y x x false true. -Variant lt_xor_ge (x y : T) : bool -> bool -> Set := - | LtNotGe of x < y : lt_xor_ge x y false true - | GeNotLt of y <= x : lt_xor_ge x y true false. +Variant lt_xor_ge (x y : T) : + T -> T -> T -> T -> bool -> bool -> Set := + | LtNotGe of x < y : lt_xor_ge x y x x y y false true + | GeNotLt of y <= x : lt_xor_ge x y y y x x true false. + +Definition min x y := if x < y then x else y. +Definition max x y := if x < y then y else x. Variant compare (x y : T) : - bool -> bool -> bool -> bool -> bool -> bool -> Set := + T -> T -> T -> T -> + bool -> bool -> bool -> bool -> bool -> bool -> Set := | CompareLt of x < y : compare x y - false false false true false true + x x y y false false false true false true | CompareGt of y < x : compare x y - false false true false true false + y y x x false false true false true false | CompareEq of x = y : compare x y - true true true true false false. + x x x x true true true true false false. Variant incompare (x y : T) : + T -> T -> T -> T -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> Set := | InCompareLt of x < y : incompare x y - false false false true false true true true + x x y y false false false true false true true true | InCompareGt of y < x : incompare x y - false false true false true false true true - | InCompare of x >< y : incompare x y - false false false false false false false false + y y x x false false true false true false true true + | InCompare of x >< y : incompare x y + x y y x false false false false false false false false | InCompareEq of x = y : incompare x y - true true true true false false true true. + x x x x true true true true false false true true. + +Definition arg_min {I : finType} := @extremum T I le. +Definition arg_max {I : finType} := @extremum T I ge. End POrderDef. Prenex Implicits lt le leif. Arguments ge {_ _}. Arguments gt {_ _}. +Arguments min {_ _}. +Arguments max {_ _}. +Arguments comparable {_ _}. Module Import POSyntax. @@ -1116,6 +1169,34 @@ Notation ">< x" := (fun y => ~~ (comparable x y)) : order_scope. Notation ">< x :> T" := (>< (x : T)) (only parsing) : order_scope. Notation "x >< y" := (~~ (comparable x y)) : order_scope. +Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := + (arg_min i0 (fun i => P%B) (fun i => F)) + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 | P ) F ]") : order_scope. + +Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" := + [arg min_(i < i0 | i \in A) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 'in' A ) F ]") : order_scope. + +Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 ) F ]") : order_scope. + +Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" := + (arg_max i0 (fun i => P%B) (fun i => F)) + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 | P ) F ]") : order_scope. + +Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" := + [arg max_(i > i0 | i \in A) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 'in' A ) F ]") : order_scope. + +Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 ) F ]") : order_scope. + End POSyntax. Module POCoercions. @@ -1202,35 +1283,38 @@ Context {T : latticeType}. Definition meet : T -> T -> T := Lattice.meet (Lattice.class T). Definition join : T -> T -> T := Lattice.join (Lattice.class T). -Variant lel_xor_gt (x y : T) : T -> T -> T -> T -> bool -> bool -> Set := - | LelNotGt of x <= y : lel_xor_gt x y x x y y true false - | GtlNotLe of y < x : lel_xor_gt x y y y x x false true. +Variant lel_xor_gt (x y : T) : + T -> T -> T -> T -> T -> T -> T -> T -> bool -> bool -> Set := + | LelNotGt of x <= y : lel_xor_gt x y x x y y x x y y true false + | GtlNotLe of y < x : lel_xor_gt x y y y x x y y x x false true. -Variant ltl_xor_ge (x y : T) : T -> T -> T -> T -> bool -> bool -> Set := - | LtlNotGe of x < y : ltl_xor_ge x y x x y y false true - | GelNotLt of y <= x : ltl_xor_ge x y y y x x true false. +Variant ltl_xor_ge (x y : T) : + T -> T -> T -> T -> T -> T -> T -> T -> bool -> bool -> Set := + | LtlNotGe of x < y : ltl_xor_ge x y x x y y x x y y false true + | GelNotLt of y <= x : ltl_xor_ge x y y y x x y y x x true false. Variant comparel (x y : T) : - T -> T -> T -> T -> bool -> bool -> bool -> bool -> bool -> bool -> Set := + T -> T -> T -> T -> T -> T -> T -> T -> + bool -> bool -> bool -> bool -> bool -> bool -> Set := | ComparelLt of x < y : comparel x y - x x y y false false false true false true + x x y y x x y y false false false true false true | ComparelGt of y < x : comparel x y - y y x x false false true false true false + y y x x y y x x false false true false true false | ComparelEq of x = y : comparel x y - x x x x true true true true false false. + x x x x x x x x true true true true false false. Variant incomparel (x y : T) : - T -> T -> T -> T -> + T -> T -> T -> T -> T -> T -> T -> T -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> Set := | InComparelLt of x < y : incomparel x y - x x y y false false false true false true true true + x x y y x x y y false false false true false true true true | InComparelGt of y < x : incomparel x y - y y x x false false true false true false true true + y y x x y y x x false false true false true false true true | InComparel of x >< y : incomparel x y - (meet x y) (meet x y) (join x y) (join x y) + x y y x (meet y x) (meet x y) (join y x) (join x y) false false false false false false false false | InComparelEq of x = y : incomparel x y - x x x x true true true true false false true true. + x x x x x x x x true true true true false false true true. End LatticeDef. @@ -1928,105 +2012,6 @@ End Exports. End Total. Import Total.Exports. -Section TotalDef. -Context {disp : unit} {T : orderType disp} {I : finType}. -Definition arg_min := @extremum T I <=%O. -Definition arg_max := @extremum T I >=%O. -End TotalDef. - -Module Import TotalSyntax. - -Fact total_display : unit. Proof. exact: tt. Qed. - -Notation max := (@join total_display _). -Notation "@ 'max' T" := - (@join total_display T) (at level 10, T at level 8, only parsing) : fun_scope. -Notation min := (@meet total_display _). -Notation "@ 'min' T" := - (@meet total_display T) (at level 10, T at level 8, only parsing) : fun_scope. - -Notation "\max_ ( i <- r | P ) F" := - (\big[max/0%O]_(i <- r | P%B) F%O) : order_scope. -Notation "\max_ ( i <- r ) F" := - (\big[max/0%O]_(i <- r) F%O) : order_scope. -Notation "\max_ ( i | P ) F" := - (\big[max/0%O]_(i | P%B) F%O) : order_scope. -Notation "\max_ i F" := - (\big[max/0%O]_i F%O) : order_scope. -Notation "\max_ ( i : I | P ) F" := - (\big[max/0%O]_(i : I | P%B) F%O) (only parsing) : - order_scope. -Notation "\max_ ( i : I ) F" := - (\big[max/0%O]_(i : I) F%O) (only parsing) : order_scope. -Notation "\max_ ( m <= i < n | P ) F" := - (\big[max/0%O]_(m <= i < n | P%B) F%O) : order_scope. -Notation "\max_ ( m <= i < n ) F" := - (\big[max/0%O]_(m <= i < n) F%O) : order_scope. -Notation "\max_ ( i < n | P ) F" := - (\big[max/0%O]_(i < n | P%B) F%O) : order_scope. -Notation "\max_ ( i < n ) F" := - (\big[max/0%O]_(i < n) F%O) : order_scope. -Notation "\max_ ( i 'in' A | P ) F" := - (\big[max/0%O]_(i in A | P%B) F%O) : order_scope. -Notation "\max_ ( i 'in' A ) F" := - (\big[max/0%O]_(i in A) F%O) : order_scope. - -Notation "\min_ ( i <- r | P ) F" := - (\big[min/1%O]_(i <- r | P%B) F%O) : order_scope. -Notation "\min_ ( i <- r ) F" := - (\big[min/1%O]_(i <- r) F%O) : order_scope. -Notation "\min_ ( i | P ) F" := - (\big[min/1%O]_(i | P%B) F%O) : order_scope. -Notation "\min_ i F" := - (\big[min/1%O]_i F%O) : order_scope. -Notation "\min_ ( i : I | P ) F" := - (\big[min/1%O]_(i : I | P%B) F%O) (only parsing) : - order_scope. -Notation "\min_ ( i : I ) F" := - (\big[min/1%O]_(i : I) F%O) (only parsing) : order_scope. -Notation "\min_ ( m <= i < n | P ) F" := - (\big[min/1%O]_(m <= i < n | P%B) F%O) : order_scope. -Notation "\min_ ( m <= i < n ) F" := - (\big[min/1%O]_(m <= i < n) F%O) : order_scope. -Notation "\min_ ( i < n | P ) F" := - (\big[min/1%O]_(i < n | P%B) F%O) : order_scope. -Notation "\min_ ( i < n ) F" := - (\big[min/1%O]_(i < n) F%O) : order_scope. -Notation "\min_ ( i 'in' A | P ) F" := - (\big[min/1%O]_(i in A | P%B) F%O) : order_scope. -Notation "\min_ ( i 'in' A ) F" := - (\big[min/1%O]_(i in A) F%O) : order_scope. - -Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := - (arg_min i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'min_' ( i < i0 | P ) F ]") : order_scope. - -Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" := - [arg min_(i < i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'min_' ( i < i0 'in' A ) F ]") : order_scope. - -Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'min_' ( i < i0 ) F ]") : order_scope. - -Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" := - (arg_max i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'max_' ( i > i0 | P ) F ]") : order_scope. - -Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" := - [arg max_(i > i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'max_' ( i > i0 'in' A ) F ]") : order_scope. - -Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'max_' ( i > i0 ) F ]") : order_scope. - -End TotalSyntax. - (**********) (* FINITE *) (**********) @@ -2577,13 +2562,15 @@ Notation "><^d x" := (fun y => ~~ (>=<^d%O x y)) : order_scope. Notation "><^d x :> T" := (><^d (x : T)) (only parsing) : order_scope. Notation "x ><^d y" := (~~ (><^d%O x y)) : order_scope. -Notation "x `&^d` y" := (@meet (dual_display _) _ x y) : order_scope. -Notation "x `|^d` y" := (@join (dual_display _) _ x y) : order_scope. - Notation dual_bottom := (@bottom (dual_display _)). Notation dual_top := (@top (dual_display _)). Notation dual_join := (@join (dual_display _) _). Notation dual_meet := (@meet (dual_display _) _). +Notation dual_max := (@max (dual_display _) _). +Notation dual_min := (@min (dual_display _) _). + +Notation "x `&^d` y" := (@meet (dual_display _) _ x y) : order_scope. +Notation "x `|^d` y" := (@join (dual_display _) _ x y) : order_scope. Notation "\join^d_ ( i <- r | P ) F" := (\big[join/0]_(i <- r | P%B) F%O) : order_scope. @@ -2648,7 +2635,7 @@ Context {disp : unit}. Local Notation porderType := (porderType disp). Context {T : porderType}. -Implicit Types x y : T. +Implicit Types (x y : T) (s : seq T). Lemma geE x y : ge x y = (y <= x). Proof. by []. Qed. Lemma gtE x y : gt x y = (y < x). Proof. by []. Qed. @@ -2746,8 +2733,7 @@ Proof. by rewrite andbC lt_le_asym. Qed. Definition lte_anti := (=^~ eq_le, lt_asym, lt_le_asym, le_lt_asym). -Lemma lt_sorted_uniq_le (s : seq T) : - sorted lt s = uniq s && sorted le s. +Lemma lt_sorted_uniq_le s : sorted lt s = uniq s && sorted le s. Proof. case: s => //= n s; elim: s n => //= m s IHs n. rewrite inE lt_neqAle negb_or IHs -!andbA. @@ -2756,12 +2742,11 @@ rewrite andbF; apply/and5P=> [[ne_nm lenm _ _ le_ms]]; case/negP: ne_nm. by rewrite eq_le lenm /=; apply: (allP (order_path_min le_trans le_ms)). Qed. -Lemma eq_sorted_lt (s1 s2 : seq T) : - sorted lt s1 -> sorted lt s2 -> s1 =i s2 -> s1 = s2. +Lemma eq_sorted_lt s1 s2 : sorted lt s1 -> sorted lt s2 -> s1 =i s2 -> s1 = s2. Proof. by apply: eq_sorted_irr => //; apply: lt_trans. Qed. -Lemma eq_sorted_le (s1 s2 : seq T) : - sorted le s1 -> sorted le s2 -> perm_eq s1 s2 -> s1 = s2. +Lemma eq_sorted_le s1 s2 : sorted le s1 -> sorted le s2 -> + perm_eq s1 s2 -> s1 = s2. Proof. by apply: eq_sorted; [apply: le_trans|apply: le_anti]. Qed. Lemma comparable_leNgt x y : x >=< y -> (x <= y) = ~~ (y < x). @@ -2777,19 +2762,22 @@ by rewrite lt_neqAle eq_le; move: c_xy => /orP [] -> //; rewrite andbT. Qed. Lemma comparable_ltgtP x y : x >=< y -> - compare x y (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y). + compare x y (min y x) (min x y) (max y x) (max x y) + (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y). Proof. -rewrite />=<%O !le_eqVlt [y == x]eq_sym. +rewrite /min /max />=<%O !le_eqVlt [y == x]eq_sym. have := (eqVneq x y, (boolP (x < y), boolP (y < x))). move=> [[->//|neq_xy /=] [[] xy [] //=]] ; do ?by rewrite ?ltxx; constructor. by rewrite ltxx in xy. by rewrite le_gtF // ltW. Qed. -Lemma comparable_leP x y : x >=< y -> le_xor_gt x y (x <= y) (y < x). +Lemma comparable_leP x y : x >=< y -> + le_xor_gt x y (min y x) (min x y) (max y x) (max x y) (x <= y) (y < x). Proof. by move=> /comparable_ltgtP [?|?|->]; constructor; rewrite // ltW. Qed. -Lemma comparable_ltP x y : x >=< y -> lt_xor_ge x y (y <= x) (x < y). +Lemma comparable_ltP x y : x >=< y -> + lt_xor_ge x y (min y x) (min x y) (max y x) (max x y) (y <= x) (x < y). Proof. by move=> /comparable_ltgtP [?|?|->]; constructor; rewrite // ltW. Qed. Lemma comparable_sym x y : (y >=< x) = (x >=< y). @@ -2808,13 +2796,14 @@ Lemma incomparable_ltF x y : (x >< y) -> (x < y) = false. Proof. by rewrite lt_neqAle => /incomparable_leF ->; rewrite andbF. Qed. Lemma comparableP x y : incompare x y + (min y x) (min x y) (max y x) (max x y) (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) (y >=< x) (x >=< y). Proof. rewrite ![y >=< _]comparable_sym; have [c_xy|i_xy] := boolP (x >=< y). by case: (comparable_ltgtP c_xy) => ?; constructor. -by rewrite ?incomparable_eqF ?incomparable_leF ?incomparable_ltF // - 1?comparable_sym //; constructor. +by rewrite /min /max ?incomparable_eqF ?incomparable_leF; + rewrite ?incomparable_ltF// 1?comparable_sym //; constructor. Qed. Lemma le_comparable (x y : T) : x <= y -> x >=< y. @@ -2869,6 +2858,280 @@ Proof. by move=> /leifP; case: C comparableP => [] []. Qed. Lemma eqTleif x y C : x <= y ?= iff C -> C -> x = y. Proof. by move=> /eq_leif<-/eqP. Qed. +(* min and max *) + +Lemma minElt x y : min x y = if x < y then x else y. Proof. by []. Qed. +Lemma maxElt x y : max x y = if x < y then y else x. Proof. by []. Qed. + +Lemma minEle x y : min x y = if x <= y then x else y. +Proof. by case: comparableP. Qed. + +Lemma maxEle x y : max x y = if x <= y then y else x. +Proof. by case: comparableP. Qed. + +Lemma comparable_minEgt x y : x >=< y -> min x y = if x > y then y else x. +Proof. by case: comparableP. Qed. +Lemma comparable_maxEgt x y : x >=< y -> max x y = if x > y then x else y. +Proof. by case: comparableP. Qed. +Lemma comparable_minEge x y : x >=< y -> min x y = if x >= y then y else x. +Proof. by case: comparableP. Qed. +Lemma comparable_maxEge x y : x >=< y -> max x y = if x >= y then x else y. +Proof. by case: comparableP. Qed. + +Lemma min_l x y : x <= y -> min x y = x. Proof. by case: comparableP. Qed. +Lemma min_r x y : y <= x -> min x y = y. Proof. by case: comparableP. Qed. +Lemma max_l x y : y <= x -> max x y = x. Proof. by case: comparableP. Qed. +Lemma max_r x y : x <= y -> max x y = y. Proof. by case: comparableP. Qed. + +Lemma minxx : idempotent (min : T -> T -> T). +Proof. by rewrite /min => x; rewrite ltxx. Qed. + +Lemma maxxx : idempotent (max : T -> T -> T). +Proof. by rewrite /max => x; rewrite ltxx. Qed. + +Lemma eq_minl x y : (min x y == x) = (x <= y). +Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP. Qed. + +Lemma eq_maxr x y : (max x y == y) = (x <= y). +Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP. Qed. + +Lemma min_idPl x y : reflect (min x y = x) (x <= y). +Proof. by apply: (iffP idP); rewrite (rwP eqP) eq_minl. Qed. + +Lemma max_idPr x y : reflect (max x y = y) (x <= y). +Proof. by apply: (iffP idP); rewrite (rwP eqP) eq_maxr. Qed. + +Lemma min_minKx x y : min (min x y) y = min x y. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed. + +Lemma min_minxK x y : min x (min x y) = min x y. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed. + +Lemma max_maxKx x y : max (max x y) y = max x y. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed. + +Lemma max_maxxK x y : max x (max x y) = max x y. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP. Qed. + +Lemma comparable_minl x y z : x >=< z -> y >=< z -> min x y >=< z. +Proof. by move=> cmp_xz cmp_yz; rewrite /min; case: ifP. Qed. + +Lemma comparable_minr x y z : z >=< x -> z >=< y -> z >=< min x y. +Proof. by move=> cmp_xz cmp_yz; rewrite /min; case: ifP. Qed. + +Lemma comparable_maxl x y z : x >=< z -> y >=< z -> max x y >=< z. +Proof. by move=> cmp_xz cmp_yz; rewrite /max; case: ifP. Qed. + +Lemma comparable_maxr x y z : z >=< x -> z >=< y -> z >=< max x y. +Proof. by move=> cmp_xz cmp_yz; rewrite /max; case: ifP. Qed. + +Section Comparable2. +Variables (z x y : T) (cmp_xy : x >=< y). + +Lemma comparable_minC : min x y = min y x. +Proof. by case: comparableP cmp_xy. Qed. + +Lemma comparable_maxC : max x y = max y x. +Proof. by case: comparableP cmp_xy. Qed. + +Lemma comparable_eq_minr : (min x y == y) = (y <= x). +Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP cmp_xy. Qed. + +Lemma comparable_eq_maxl : (max x y == x) = (y <= x). +Proof. by rewrite !(fun_if, if_arg) eqxx; case: comparableP cmp_xy. Qed. + +Lemma comparable_min_idPr : reflect (min x y = y) (y <= x). +Proof. by apply: (iffP idP); rewrite (rwP eqP) comparable_eq_minr. Qed. + +Lemma comparable_max_idPl : reflect (max x y = x) (y <= x). +Proof. by apply: (iffP idP); rewrite (rwP eqP) comparable_eq_maxl. Qed. + +Lemma comparable_le_minr : (z <= min x y) = (z <= x) && (z <= y). +Proof. +case: comparableP cmp_xy => // [||<-//]; rewrite ?andbb//; last rewrite andbC; + by case: (comparableP z) => // [/lt_trans xlt/xlt|->] /ltW. +Qed. + +Lemma comparable_le_minl : (min x y <= z) = (x <= z) || (y <= z). +Proof. +case: comparableP cmp_xy => // [||<-//]; rewrite ?orbb//; last rewrite orbC; + by move=> xy _; apply/idP/idP => [->|/orP[]]//; apply/le_trans/ltW. +Qed. + +Lemma comparable_lt_minr : (z < min x y) = (z < x) && (z < y). +Proof. +case: comparableP cmp_xy => // [||<-//]; rewrite ?andbb//; last rewrite andbC; + by case: (comparableP z) => // /lt_trans xlt/xlt. +Qed. + +Lemma comparable_lt_minl : (min x y < z) = (x < z) || (y < z). +Proof. +case: comparableP cmp_xy => // [||<-//]; rewrite ?orbb//; last rewrite orbC; + by move=> xy _; apply/idP/idP => [->|/orP[]]//; apply/lt_trans. +Qed. + +Lemma comparable_le_maxr : (z <= max x y) = (z <= x) || (z <= y). +Proof. +case: comparableP cmp_xy => // [||<-//]; rewrite ?orbb//; first rewrite orbC; + by move=> xy _; apply/idP/idP => [->|/orP[]]// /le_trans->//; apply/ltW. +Qed. + +Lemma comparable_le_maxl : (max x y <= z) = (x <= z) && (y <= z). +Proof. +case: comparableP cmp_xy => // [||<-//]; rewrite ?andbb//; first rewrite andbC; + by case: (comparableP z) => // [ylt /lt_trans /(_ _)/ltW|->/ltW]->. +Qed. + +Lemma comparable_lt_maxr : (z < max x y) = (z < x) || (z < y). +Proof. +case: comparableP cmp_xy => // [||<-//]; rewrite ?orbb//; first rewrite orbC; + by move=> xy _; apply/idP/idP => [->|/orP[]]// /lt_trans->. +Qed. + +Lemma comparable_lt_maxl : (max x y < z) = (x < z) && (y < z). +Proof. +case: comparableP cmp_xy => // [||<-//]; rewrite ?andbb//; first rewrite andbC; +by case: (comparableP z) => // ylt /lt_trans->. +Qed. + +Lemma comparable_minxK : max (min x y) y = y. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed. + +Lemma comparable_minKx : max x (min x y) = x. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed. + +Lemma comparable_maxxK : min (max x y) y = y. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed. + +Lemma comparable_maxKx : min x (max x y) = x. +Proof. by rewrite !(fun_if, if_arg) ltxx/=; case: comparableP cmp_xy. Qed. + +End Comparable2. + +Section Comparable3. +Variables (x y z : T) (cmp_xy : x >=< y) (cmp_xz : x >=< z) (cmp_yz : y >=< z). +Let P := comparableP. + +Lemma comparable_minA : min x (min y z) = min (min x y) z. +Proof. +move: cmp_xy cmp_xz cmp_yz; rewrite !(fun_if, if_arg)/=. +move: (P x y) (P x z) (P y z) => [xy|xy|xy|<-] [xz|xz|xz|<-]// []//= yz. +- by have := lt_trans xy (lt_trans yz xz); rewrite ltxx. +- by have := lt_trans xy (lt_trans xz yz); rewrite ltxx. +- by have := lt_trans xy xz; rewrite yz ltxx. +Qed. + +Lemma comparable_maxA : max x (max y z) = max (max x y) z. +Proof. +move: cmp_xy cmp_xz cmp_yz; rewrite !(fun_if, if_arg)/=. +move: (P x y) (P x z) (P y z) => [xy|xy|xy|<-] [xz|xz|xz|<-]// []//= yz. +- by have := lt_trans xy (lt_trans yz xz); rewrite ltxx. +- by have := lt_trans xy (lt_trans xz yz); rewrite ltxx. +- by have := lt_trans xy xz; rewrite yz ltxx. +Qed. + +Lemma comparable_max_minl : max (min x y) z = min (max x z) (max y z). +Proof. +move: cmp_xy cmp_xz cmp_yz; rewrite !(fun_if, if_arg)/=. +move: (P x y) (P x z) (P y z). +move=> [xy|xy|xy|<-] [xz|xz|xz|<-] [yz|yz|yz|//->]//= _; rewrite ?ltxx//. +- by have := lt_trans xy (lt_trans yz xz); rewrite ltxx. +- by have := lt_trans xy (lt_trans xz yz); rewrite ltxx. +Qed. + +Lemma comparable_min_maxl : min (max x y) z = max (min x z) (min y z). +Proof. +move: cmp_xy cmp_xz cmp_yz; rewrite !(fun_if, if_arg)/=. +move: (P x y) (P x z) (P y z). +move=> [xy|xy|xy|<-] [xz|xz|xz|<-] []yz//= _; rewrite ?ltxx//. +- by have := lt_trans xy (lt_trans yz xz); rewrite ltxx. +- by have := lt_trans xy yz; rewrite ltxx. +- by have := lt_trans xy (lt_trans xz yz); rewrite ltxx. +- by have := lt_trans xy xz; rewrite yz ltxx. +Qed. + +End Comparable3. + +Lemma comparable_minAC x y z : x >=< y -> x >=< z -> y >=< z -> + min (min x y) z = min (min x z) y. +Proof. +move=> xy xz yz; rewrite -comparable_minA// [min y z]comparable_minC//. +by rewrite comparable_minA// 1?comparable_sym. +Qed. + +Lemma comparable_maxAC x y z : x >=< y -> x >=< z -> y >=< z -> + max (max x y) z = max (max x z) y. +Proof. +move=> xy xz yz; rewrite -comparable_maxA// [max y z]comparable_maxC//. +by rewrite comparable_maxA// 1?comparable_sym. +Qed. + +Lemma comparable_minCA x y z : x >=< y -> x >=< z -> y >=< z -> + min x (min y z) = min y (min x z). +Proof. +move=> xy xz yz; rewrite comparable_minA// [min x y]comparable_minC//. +by rewrite -comparable_minA// 1?comparable_sym. +Qed. + +Lemma comparable_maxCA x y z : x >=< y -> x >=< z -> y >=< z -> + max x (max y z) = max y (max x z). +Proof. +move=> xy xz yz; rewrite comparable_maxA// [max x y]comparable_maxC//. +by rewrite -comparable_maxA// 1?comparable_sym. +Qed. + +Lemma comparable_minACA x y z t : + x >=< y -> x >=< z -> x >=< t -> y >=< z -> y >=< t -> z >=< t -> + min (min x y) (min z t) = min (min x z) (min y t). +Proof. +move=> xy xz xt yz yt zt; rewrite comparable_minA// ?comparable_minl//. +rewrite [min _ z]comparable_minAC// -comparable_minA// ?comparable_minl//. +by rewrite comparable_sym. +Qed. + +Lemma comparable_maxACA x y z t : + x >=< y -> x >=< z -> x >=< t -> y >=< z -> y >=< t -> z >=< t -> + max (max x y) (max z t) = max (max x z) (max y t). +Proof. +move=> xy xz xt yz yt zt; rewrite comparable_maxA// ?comparable_maxl//. +rewrite [max _ z]comparable_maxAC// -comparable_maxA// ?comparable_maxl//. +by rewrite comparable_sym. +Qed. + +Lemma comparable_max_minr x y z : x >=< y -> x >=< z -> y >=< z -> + max x (min y z) = min (max x y) (max x z). +Proof. +move=> xy xz yz; rewrite ![max x _]comparable_maxC// ?comparable_minr//. +by rewrite comparable_max_minl// 1?comparable_sym. +Qed. + +Lemma comparable_min_maxr x y z : x >=< y -> x >=< z -> y >=< z -> + min x (max y z) = max (min x y) (min x z). +Proof. +move=> xy xz yz; rewrite ![min x _]comparable_minC// ?comparable_maxr//. +by rewrite comparable_min_maxl// 1?comparable_sym. +Qed. + +Section ArgExtremum. + +Context (I : finType) (i0 : I) (P : {pred I}) (F : I -> T) (Pi0 : P i0). +Hypothesis F_comparable : {in P &, forall i j, F i >=< F j}. + +Lemma comparable_arg_minP: extremum_spec <=%O P F (arg_min i0 P F). +Proof. +by apply: extremum_inP => // [x _|y x z _ _ _]; [apply: lexx|apply: le_trans]. +Qed. + +Lemma comparable_arg_maxP: extremum_spec >=%O P F (arg_max i0 P F). +Proof. +apply: extremum_inP => // [x _|y x z _ _ _|]; [exact: lexx|exact: ge_trans|]. +by move=> x y xP yP; rewrite orbC [_ || _]F_comparable. +Qed. + +End ArgExtremum. + +(* monotonicity *) + Lemma mono_in_leif (A : {pred T}) (f : T -> T) C : {in A &, {mono f : x y / x <= y}} -> {in A &, forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C)}. @@ -2975,6 +3238,10 @@ Arguments mono_in_leif [disp T A f C]. Arguments nmono_in_leif [disp T A f C]. Arguments mono_leif [disp T f C]. Arguments nmono_leif [disp T f C]. +Arguments min_idPl {disp T x y}. +Arguments max_idPr {disp T x y}. +Arguments comparable_min_idPr {disp T x y _}. +Arguments comparable_max_idPl {disp T x y _}. Module Import DualPOrder. Section DualPOrder. @@ -3204,31 +3471,38 @@ Lemma leU2 x y z t : x <= z -> y <= t -> x `|` y <= z `|` t. Proof. exact: (@leI2 _ [latticeType of L^d]). Qed. Lemma lcomparableP x y : incomparel x y + (min y x) (min x y) (max y x) (max x y) (y `&` x) (x `&` y) (y `|` x) (x `|` y) (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) (y >=< x) (x >=< y). Proof. by case: (comparableP x) => [hxy|hxy|hxy|->]; do 1?have hxy' := ltW hxy; - rewrite ?(meetxx, joinxx, meetC y, joinC y) - ?(meet_idPl hxy', meet_idPr hxy', join_idPl hxy', join_idPr hxy'); - constructor. + rewrite ?(meetxx, joinxx); + rewrite ?(meet_idPl hxy', meet_idPr hxy', join_idPl hxy', join_idPr hxy'); + constructor. Qed. Lemma lcomparable_ltgtP x y : x >=< y -> - comparel x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) + comparel x y (min y x) (min x y) (max y x) (max x y) + (y `&` x) (x `&` y) (y `|` x) (x `|` y) (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y). Proof. by case: (lcomparableP x) => // *; constructor. Qed. Lemma lcomparable_leP x y : x >=< y -> - lel_xor_gt x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (x <= y) (y < x). + lel_xor_gt x y (min y x) (min x y) (max y x) (max x y) + (y `&` x) (x `&` y) (y `|` x) (x `|` y) (x <= y) (y < x). Proof. by move/lcomparable_ltgtP => [/ltW xy|xy|->]; constructor. Qed. Lemma lcomparable_ltP x y : x >=< y -> - ltl_xor_ge x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (y <= x) (x < y). + ltl_xor_ge x y (min y x) (min x y) (max y x) (max x y) + (y `&` x) (x `&` y) (y `|` x) (x `|` y) (y <= x) (x < y). Proof. by move=> /lcomparable_ltgtP [xy|/ltW xy|->]; constructor. Qed. End LatticeTheoryJoin. End LatticeTheoryJoin. +Arguments meet_idPl {disp L x y}. +Arguments join_idPl {disp L x y}. + Module Import DistrLatticeTheory. Section DistrLatticeTheory. Context {disp : unit}. @@ -3262,7 +3536,7 @@ Section TotalTheory. Context {disp : unit}. Local Notation orderType := (orderType disp). Context {T : orderType}. -Implicit Types (x y z t : T). +Implicit Types (x y z t : T) (s : seq T). Lemma le_total : total (<=%O : rel T). Proof. by case: T => [? [?]]. Qed. Hint Resolve le_total : core. @@ -3274,13 +3548,14 @@ Hint Resolve ge_total : core. Lemma comparableT x y : x >=< y. Proof. exact: le_total. Qed. Hint Resolve comparableT : core. -Lemma sort_le_sorted (s : seq T) : sorted <=%O (sort <=%O s). +Lemma sort_le_sorted s : sorted <=%O (sort <=%O s). Proof. exact: sort_sorted. Qed. +Hint Resolve sort_le_sorted : core. -Lemma sort_lt_sorted (s : seq T) : sorted lt (sort le s) = uniq s. +Lemma sort_lt_sorted s : sorted lt (sort le s) = uniq s. Proof. by rewrite lt_sorted_uniq_le sort_uniq sort_le_sorted andbT. Qed. -Lemma sort_le_id (s : seq T) : sorted le s -> sort le s = s. +Lemma sort_le_id s : sorted le s -> sort le s = s. Proof. by move=> ss; apply: eq_sorted_le; rewrite ?sort_le_sorted // perm_sort. Qed. @@ -3324,21 +3599,106 @@ Lemma eq_ltRL x y z t : (x < y -> z < t) -> (y <= x -> t <= z) -> (z < t) = (x < y). Proof. by move=> *; symmetry; apply: eq_ltLR. Qed. -(* interaction with lattice operations *) +(* max and min is join and meet *) + +Lemma meetEtotal x y : x `&` y = min x y. Proof. by case: leP. Qed. +Lemma joinEtotal x y : x `|` y = max x y. Proof. by case: leP. Qed. + +(* max and min theory *) + +Lemma minEgt x y : min x y = if x > y then y else x. Proof. by case: ltP. Qed. +Lemma maxEgt x y : max x y = if x > y then x else y. Proof. by case: ltP. Qed. +Lemma minEge x y : min x y = if x >= y then y else x. Proof. by case: leP. Qed. +Lemma maxEge x y : max x y = if x >= y then x else y. Proof. by case: leP. Qed. + +Lemma minC : commutative (min : T -> T -> T). +Proof. by move=> x y; apply: comparable_minC. Qed. + +Lemma maxC : commutative (max : T -> T -> T). +Proof. by move=> x y; apply: comparable_maxC. Qed. + +Lemma minA : associative (min : T -> T -> T). +Proof. by move=> x y z; apply: comparable_minA. Qed. + +Lemma maxA : associative (max : T -> T -> T). +Proof. by move=> x y z; apply: comparable_maxA. Qed. + +Lemma minAC : right_commutative (min : T -> T -> T). +Proof. by move=> x y z; apply: comparable_minAC. Qed. + +Lemma maxAC : right_commutative (max : T -> T -> T). +Proof. by move=> x y z; apply: comparable_maxAC. Qed. + +Lemma minCA : left_commutative (min : T -> T -> T). +Proof. by move=> x y z; apply: comparable_minCA. Qed. + +Lemma maxCA : left_commutative (max : T -> T -> T). +Proof. by move=> x y z; apply: comparable_maxCA. Qed. + +Lemma minACA : interchange (min : T -> T -> T) min. +Proof. by move=> x y z t; apply: comparable_minACA. Qed. + +Lemma maxACA : interchange (max : T -> T -> T) max. +Proof. by move=> x y z t; apply: comparable_maxACA. Qed. + +Lemma eq_minr x y : (min x y == y) = (y <= x). +Proof. exact: comparable_eq_minr. Qed. + +Lemma eq_maxl x y : (max x y == x) = (y <= x). +Proof. exact: comparable_eq_maxl. Qed. + +Lemma min_idPr x y : reflect (min x y = y) (y <= x). +Proof. exact: comparable_min_idPr. Qed. + +Lemma max_idPl x y : reflect (max x y = x) (y <= x). +Proof. exact: comparable_max_idPl. Qed. + +Lemma le_minr z x y : (z <= min x y) = (z <= x) && (z <= y). +Proof. exact: comparable_le_minr. Qed. + +Lemma le_minl z x y : (min x y <= z) = (x <= z) || (y <= z). +Proof. exact: comparable_le_minl. Qed. + +Lemma lt_minr z x y : (z < min x y) = (z < x) && (z < y). +Proof. exact: comparable_lt_minr. Qed. + +Lemma lt_minl z x y : (min x y < z) = (x < z) || (y < z). +Proof. exact: comparable_lt_minl. Qed. + +Lemma le_maxr z x y : (z <= max x y) = (z <= x) || (z <= y). +Proof. exact: comparable_le_maxr. Qed. + +Lemma le_maxl z x y : (max x y <= z) = (x <= z) && (y <= z). +Proof. exact: comparable_le_maxl. Qed. + +Lemma lt_maxr z x y : (z < max x y) = (z < x) || (z < y). +Proof. exact: comparable_lt_maxr. Qed. + +Lemma lt_maxl z x y : (max x y < z) = (x < z) && (y < z). +Proof. exact: comparable_lt_maxl. Qed. + +Lemma minxK x y : max (min x y) y = y. Proof. exact: comparable_minxK. Qed. +Lemma minKx x y : max x (min x y) = x. Proof. exact: comparable_minKx. Qed. +Lemma maxxK x y : min (max x y) y = y. Proof. exact: comparable_maxxK. Qed. +Lemma maxKx x y : min x (max x y) = x. Proof. exact: comparable_maxKx. Qed. + +Lemma max_minl : left_distributive (max : T -> T -> T) min. +Proof. by move=> x y z; apply: comparable_max_minl. Qed. + +Lemma min_maxl : left_distributive (min : T -> T -> T) max. +Proof. by move=> x y z; apply: comparable_min_maxl. Qed. + +Lemma max_minr : right_distributive (max : T -> T -> T) min. +Proof. by move=> x y z; apply: comparable_max_minr. Qed. + +Lemma min_maxr : right_distributive (min : T -> T -> T) max. +Proof. by move=> x y z; apply: comparable_min_maxr. Qed. Lemma leIx x y z : (meet y z <= x) = (y <= x) || (z <= x). -Proof. -by case: (leP y z) => hyz; case: leP => ?; - rewrite ?(orbT, orbF) //=; apply/esym/negbTE; - rewrite -ltNge ?(lt_le_trans _ hyz) ?(lt_trans _ hyz). -Qed. +Proof. by rewrite meetEtotal le_minl. Qed. Lemma lexU x y z : (x <= join y z) = (x <= y) || (x <= z). -Proof. -by case: (leP y z) => hyz; case: leP => ?; - rewrite ?(orbT, orbF) //=; apply/esym/negbTE; - rewrite -ltNge ?(le_lt_trans hyz) ?(lt_trans hyz). -Qed. +Proof. by rewrite joinEtotal le_maxr. Qed. Lemma ltxI x y z : (x < meet y z) = (x < y) && (x < z). Proof. by rewrite !ltNge leIx negb_or. Qed. @@ -3361,9 +3721,6 @@ Section ArgExtremum. Context (I : finType) (i0 : I) (P : {pred I}) (F : I -> T) (Pi0 : P i0). -Definition arg_minnP := arg_minP. -Definition arg_maxnP := arg_maxP. - Lemma arg_minP: extremum_spec <=%O P F (arg_min i0 P F). Proof. by apply: extremumP => //; apply: le_trans. Qed. @@ -3373,6 +3730,10 @@ Proof. by apply: extremumP => //; [apply: ge_refl | apply: ge_trans]. Qed. End ArgExtremum. End TotalTheory. + +Arguments min_idPr {disp T x y}. +Arguments max_idPl {disp T x y}. + Section TotalMonotonyTheory. Context {disp : unit} {disp' : unit}. @@ -4034,14 +4395,16 @@ Implicit Types (x y z : T). Let comparableT x y : x >=< y := m x y. Fact ltgtP x y : - compare x y (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y). + compare x y (min y x) (min x y) (max y x) (max x y) + (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y). Proof. exact: comparable_ltgtP. Qed. -Fact leP x y : le_xor_gt x y (x <= y) (y < x). +Fact leP x y : le_xor_gt x y + (min y x) (min x y) (max y x) (max x y) (x <= y) (y < x). Proof. exact: comparable_leP. Qed. -Definition meet x y := if x <= y then x else y. -Definition join x y := if y <= x then x else y. +Definition meet := @min _ T. +Definition join := @max _ T. Fact meetC : commutative meet. Proof. by move=> x y; rewrite /meet; have [] := ltgtP. Qed. @@ -4051,25 +4414,31 @@ Proof. by move=> x y; rewrite /join; have [] := ltgtP. Qed. Fact meetA : associative meet. Proof. -move=> x y z; rewrite /meet; case: (leP y z) => yz; case: (leP x y) => xy //=. -- by rewrite (le_trans xy). -- by rewrite yz. -by rewrite !lt_geF // (lt_trans yz). +move=> x y z; rewrite /meet /min !(fun_if, if_arg). +case: (leP z y) (leP y x) (leP z x) => [] zy [] yx [] zx//=. + by have := le_lt_trans (le_trans zy yx) zx; rewrite ltxx. +by apply/eqP; rewrite eq_le zx ltW// (lt_trans yx). Qed. Fact joinA : associative join. Proof. -move=> x y z; rewrite /join; case: (leP z y) => yz; case: (leP y x) => xy //=. -- by rewrite (le_trans yz). -- by rewrite yz. -by rewrite !lt_geF // (lt_trans xy). +move=> x y z; rewrite /meet /min !(fun_if, if_arg). +case: (leP z y) (leP y x) (leP z x) => [] zy [] yx [] zx//=. + by have := le_lt_trans (le_trans zy yx) zx; rewrite ltxx. +by apply/eqP; rewrite eq_le zx ltW// (lt_trans yx). Qed. Fact joinKI y x : meet x (join x y) = x. -Proof. by rewrite /meet /join; case: (leP y x) => yx; rewrite ?lexx ?ltW. Qed. +Proof. +rewrite /meet /join /min /max !(fun_if, if_arg). +by have []// := ltgtP x y; rewrite ltxx. +Qed. Fact meetKU y x : join x (meet x y) = x. -Proof. by rewrite /meet /join; case: (leP x y) => yx; rewrite ?lexx ?ltW. Qed. +Proof. +rewrite /meet /join /min /max !(fun_if, if_arg). +by have []// := ltgtP x y; rewrite ltxx. +Qed. Fact leEmeet x y : (x <= y) = (meet x y == x). Proof. by rewrite /meet; case: leP => ?; rewrite ?eqxx ?lt_eqF. Qed. @@ -4079,8 +4448,7 @@ Definition latticeMixin := meetC joinC meetA joinA joinKI meetKU leEmeet. Definition totalLatticeMixin : - totalLatticeMixin (LatticeType T latticeMixin) := - m. + totalLatticeMixin (LatticeType T latticeMixin) := m. End TotalPOrderMixin. @@ -4219,8 +4587,8 @@ Record of_ := Build { meet : T -> T -> T; join : T -> T -> T; lt_def : forall x y, lt x y = (y != x) && le x y; - meet_def : forall x y, meet x y = if le x y then x else y; - join_def : forall x y, join x y = if le y x then x else y; + meet_def : forall x y, meet x y = if lt x y then x else y; + join_def : forall x y, join x y = if lt x y then y else x; le_anti : antisymmetric le; le_trans : transitive le; le_total : total le; @@ -4294,7 +4662,7 @@ Record of_ := Build { join : T -> T -> T; le_def : forall x y, le x y = (x == y) || lt x y; meet_def : forall x y, meet x y = if lt x y then x else y; - join_def : forall x y, join x y = if lt y x then x else y; + join_def : forall x y, join x y = if lt x y then y else x; lt_irr : irreflexive lt; lt_trans : transitive lt; lt_total : forall x y, x != y -> lt x y || lt y x; @@ -4305,11 +4673,11 @@ Variables (m : of_). Fact lt_def x y : lt m x y = (y != x) && le m x y. Proof. by rewrite le_def; case: eqVneq => //= ->; rewrite lt_irr. Qed. -Fact meet_def_le x y : meet m x y = if le m x y then x else y. -Proof. by rewrite meet_def le_def; case: eqP => //= ->; rewrite lt_irr. Qed. +Fact meet_def_le x y : meet m x y = if lt m x y then x else y. +Proof. by rewrite meet_def lt_def; case: eqP. Qed. -Fact join_def_le x y : join m x y = if le m y x then x else y. -Proof. by rewrite join_def le_def; case: eqP => //= ->; rewrite lt_irr. Qed. +Fact join_def_le x y : join m x y = if lt m x y then y else x. +Proof. by rewrite join_def lt_def; case: eqP. Qed. Fact le_anti : antisymmetric (le m). Proof. @@ -4534,9 +4902,8 @@ Import SubOrder.Exports. (******************************************************************************) (* The Module NatOrder defines leq as the canonical order on the type nat, *) -(* i.e. without creating a "copy". We use the predefined total_display, which *) -(* is designed to parse and print meet and join as minn and maxn. This looks *) -(* like standard canonical structure declaration, except we use a display. *) +(* i.e. without creating a "copy". We define and use nat_display and proceed *) +(* like standard canonical structure declaration, except we use this display. *) (* We also use a single factory LeOrderMixin to instantiate three different *) (* canonical declarations porderType, distrLatticeType, orderType *) (* We finish by providing theorems to convert the operations of ordered and *) @@ -4546,19 +4913,16 @@ Import SubOrder.Exports. Module NatOrder. Section NatOrder. -Lemma minnE x y : minn x y = if (x <= y)%N then x else y. -Proof. by case: leqP. Qed. - -Lemma maxnE x y : maxn x y = if (y <= x)%N then x else y. -Proof. by case: leqP. Qed. +Lemma nat_display : unit. Proof. exact: tt. Qed. Lemma ltn_def x y : (x < y)%N = (y != x) && (x <= y)%N. Proof. by rewrite ltn_neqAle eq_sym. Qed. Definition orderMixin := - LeOrderMixin ltn_def minnE maxnE anti_leq leq_trans leq_total. + LeOrderMixin ltn_def (fun _ _ => erefl) (fun _ _ => erefl) + anti_leq leq_trans leq_total. -Canonical porderType := POrderType total_display nat orderMixin. +Canonical porderType := POrderType nat_display nat orderMixin. Canonical latticeType := LatticeType nat orderMixin. Canonical bLatticeType := BLatticeType nat (BLatticeMixin leq0n). Canonical distrLatticeType := DistrLatticeType nat orderMixin. @@ -4567,8 +4931,8 @@ Canonical orderType := OrderType nat orderMixin. Lemma leEnat : le = leq. Proof. by []. Qed. Lemma ltEnat : lt = ltn. Proof. by []. Qed. -Lemma meetEnat : meet = minn. Proof. by []. Qed. -Lemma joinEnat : join = maxn. Proof. by []. Qed. +Lemma minEnat : min = minn. Proof. by []. Qed. +Lemma maxEnat : max = maxn. Proof. by []. Qed. Lemma botEnat : 0%O = 0%N :> nat. Proof. by []. Qed. End NatOrder. @@ -4582,8 +4946,8 @@ Canonical bDistrLatticeType. Canonical orderType. Definition leEnat := leEnat. Definition ltEnat := ltEnat. -Definition meetEnat := meetEnat. -Definition joinEnat := joinEnat. +Definition minEnat := minEnat. +Definition maxEnat := maxEnat. Definition botEnat := botEnat. End Exports. End NatOrder. @@ -4850,10 +5214,12 @@ Module BoolOrder. Section BoolOrder. Implicit Types (x y : bool). -Fact andbE x y : x && y = if (x <= y)%N then x else y. +Fact bool_display : unit. Proof. exact: tt. Qed. + +Fact andbE x y : x && y = if (x < y)%N then x else y. Proof. by case: x y => [] []. Qed. -Fact orbE x y : x || y = if (y <= x)%N then x else y. +Fact orbE x y : x || y = if (x < y)%N then y else x. Proof. by case: x y => [] []. Qed. Fact ltn_def x y : (x < y)%N = (y != x) && (x <= y)%N. @@ -4870,7 +5236,7 @@ Lemma joinIB x y : (x && y) || sub x y = x. Proof. by case: x y => [] []. Qed. Definition orderMixin := LeOrderMixin ltn_def andbE orbE anti leq_trans leq_total. -Canonical porderType := POrderType total_display bool orderMixin. +Canonical porderType := POrderType bool_display bool orderMixin. Canonical latticeType := LatticeType bool orderMixin. Canonical bLatticeType := BLatticeType bool (@BLatticeMixin _ _ false leq0n). @@ -5095,61 +5461,11 @@ Notation "><^l x" := (fun y => ~~ (>=<^l%O x y)) : order_scope. Notation "><^l x :> T" := (><^l (x : T)) (only parsing) : order_scope. Notation "x ><^l y" := (~~ (><^l%O x y)) : order_scope. -Notation minlexi := (@meet lexi_display _). -Notation maxlexi := (@join lexi_display _). - -Notation "x `&^l` y" := (minlexi x y) : order_scope. -Notation "x `|^l` y" := (maxlexi x y) : order_scope. - -Notation "\max^l_ ( i <- r | P ) F" := - (\big[maxlexi/0]_(i <- r | P%B) F%O) : order_scope. -Notation "\max^l_ ( i <- r ) F" := - (\big[maxlexi/0]_(i <- r) F%O) : order_scope. -Notation "\max^l_ ( i | P ) F" := - (\big[maxlexi/0]_(i | P%B) F%O) : order_scope. -Notation "\max^l_ i F" := - (\big[maxlexi/0]_i F%O) : order_scope. -Notation "\max^l_ ( i : I | P ) F" := - (\big[maxlexi/0]_(i : I | P%B) F%O) (only parsing) : order_scope. -Notation "\max^l_ ( i : I ) F" := - (\big[maxlexi/0]_(i : I) F%O) (only parsing) : order_scope. -Notation "\max^l_ ( m <= i < n | P ) F" := - (\big[maxlexi/0]_(m <= i < n | P%B) F%O) : order_scope. -Notation "\max^l_ ( m <= i < n ) F" := - (\big[maxlexi/0]_(m <= i < n) F%O) : order_scope. -Notation "\max^l_ ( i < n | P ) F" := - (\big[maxlexi/0]_(i < n | P%B) F%O) : order_scope. -Notation "\max^l_ ( i < n ) F" := - (\big[maxlexi/0]_(i < n) F%O) : order_scope. -Notation "\max^l_ ( i 'in' A | P ) F" := - (\big[maxlexi/0]_(i in A | P%B) F%O) : order_scope. -Notation "\max^l_ ( i 'in' A ) F" := - (\big[maxlexi/0]_(i in A) F%O) : order_scope. - -Notation "\min^l_ ( i <- r | P ) F" := - (\big[minlexi/1]_(i <- r | P%B) F%O) : order_scope. -Notation "\min^l_ ( i <- r ) F" := - (\big[minlexi/1]_(i <- r) F%O) : order_scope. -Notation "\min^l_ ( i | P ) F" := - (\big[minlexi/1]_(i | P%B) F%O) : order_scope. -Notation "\min^l_ i F" := - (\big[minlexi/1]_i F%O) : order_scope. -Notation "\min^l_ ( i : I | P ) F" := - (\big[minlexi/1]_(i : I | P%B) F%O) (only parsing) : order_scope. -Notation "\min^l_ ( i : I ) F" := - (\big[minlexi/1]_(i : I) F%O) (only parsing) : order_scope. -Notation "\min^l_ ( m <= i < n | P ) F" := - (\big[minlexi/1]_(m <= i < n | P%B) F%O) : order_scope. -Notation "\min^l_ ( m <= i < n ) F" := - (\big[minlexi/1]_(m <= i < n) F%O) : order_scope. -Notation "\min^l_ ( i < n | P ) F" := - (\big[minlexi/1]_(i < n | P%B) F%O) : order_scope. -Notation "\min^l_ ( i < n ) F" := - (\big[minlexi/1]_(i < n) F%O) : order_scope. -Notation "\min^l_ ( i 'in' A | P ) F" := - (\big[minlexi/1]_(i in A | P%B) F%O) : order_scope. -Notation "\min^l_ ( i 'in' A ) F" := - (\big[minlexi/1]_(i in A) F%O) : order_scope. +Notation meetlexi := (@meet lexi_display _). +Notation joinlexi := (@join lexi_display _). + +Notation "x `&^l` y" := (meetlexi x y) : order_scope. +Notation "x `|^l` y" := (joinlexi x y) : order_scope. End LexiSyntax. @@ -6690,7 +7006,6 @@ Export BLatticeSyntax. Export TBLatticeSyntax. Export CBDistrLatticeSyntax. Export CTBDistrLatticeSyntax. -Export TotalSyntax. Export DualSyntax. Export DvdSyntax. End Syntax. |