Reorganizing relation between comparability/real and big

3 files changed, 47 insertions, 32 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index a14b391..f79042d 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -31,8 +31,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
     `contraPleq`, `contraPltn`, `contra_not_leq`, `contra_not_ltn`, `contra_leq_not`, `contra_ltn_not`
 - in `ssralg.v`, new lemma `sumr_const_nat` and `iter_addr_0`
 - in `ssrnum.v`, new lemma `ler_sum_nat`
-- in `ssrnum.v`, new lemmas `max_real`, `min_real`, `bigmax_real`, `bigmin_real`
-- in `order.v`, new lemms `comparable_big`
+- in `ssrnum.v`, new lemmas `big_real`, `sum_real`, `prod_real`,
+  `max_real`, `min_real`, and `bigmax_real`, `bigmin_real`.
+- in `order.v`, new lemmas `comparable_bigl` and `comparable_bigr`.
 
 - in `seq.v`, new lemmas: `take_uniq`, `drop_uniq`
 - in `fintype.v`, new lemmas: `card_geqP`, `card_gt1P`, `card_gt2P`,
@@ -264,6 +265,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - The `class_of` records of structures are turned into primitive records to
   prevent prevent potential issues of ambiguous paths and convertibility of
   structure instances.
+- In `order.v`, rephrased `comparable_(min|max)[rl]` in terms of
+  `{in _, forall x y, _}`, hence reordering the arguments. Made them
+  hints for smoother combination with `comparable_big[lr]`.
+
 
 ### Renamed
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 36498b3..3c88ef0 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1479,6 +1479,19 @@ rewrite sqrf_eq1 => /orP[/eqP //|]; rewrite -ger0_def le0r oppr_eq0 oner_eq0.
 by move/(addr_gt0 ltr01); rewrite subrr ltxx.
 Qed.
 
+Lemma big_real x0 op I (P : pred I) F (s : seq I) :
+  {in real &, forall x y, op x y \is real} -> x0 \is real ->
+  {in P, forall i, F i \is real} -> \big[op/x0]_(i <- s | P i) F i \is real.
+Proof. exact: comparable_bigr. Qed.
+
+Lemma sum_real I (P : pred I) (F : I -> R) (s : seq I) :
+  {in P, forall i, F i \is real} -> \sum_(i <- s | P i) F i \is real.
+Proof. by apply/big_real; [apply: rpredD | apply: rpred0]. Qed.
+
+Lemma prod_real I (P : pred I) (F : I -> R) (s : seq I) :
+  {in P, forall i, F i \is real} -> \prod_(i <- s | P i) F i \is real.
+Proof. by apply/big_real; [apply: rpredM | apply: rpred1]. Qed.
+
 Section NormedZmoduleTheory.
 
 Variable V : normedZmodType R.
@@ -1780,24 +1793,20 @@ by rewrite ?subr0 ?sub0r //; constructor.
 Qed.
 
 Lemma max_real : {in real &, forall x y, max x y \is real}.
-Proof. by move=> x y ? ?; case: real_leP. Qed.
+Proof. exact: comparable_maxr. Qed.
 
 Lemma min_real : {in real &, forall x y, min x y \is real}.
-Proof. by move=> x y ? ?; case: real_leP. Qed.
+Proof. exact: comparable_minr. Qed.
 
 Lemma bigmax_real I x0 (r : seq I) (P : pred I) (f : I -> R):
   x0 \is real -> {in P, forall i : I, f i \is real} ->
   \big[max/x0]_(i <- r | P i) f i \is real.
-Proof.
-by move=> x0r Pr; elim/big_rec : _ => // i x Pi xr; rewrite max_real ?Pr.
-Qed.
+Proof. exact/big_real/max_real. Qed.
 
 Lemma bigmin_real I x0 (r : seq I) (P : pred I) (f : I -> R):
-  x0 \is real -> {in P, forall t : I, f t \is real} ->
-  \big[min/x0]_(t <- r | P t) f t \is real.
-Proof.
-by move=> x0r Pr; elim/big_rec : _ => // i x Pi xr; rewrite min_real ?Pr.
-Qed.
+  x0 \is real -> {in P, forall i : I, f i \is real} ->
+  \big[min/x0]_(i <- r | P i) f i \is real.
+Proof. exact/big_real/min_real. Qed.
 
 Lemma real_neqr_lt : {in real &, forall x y, (x != y) = (x < y) || (y < x)}.
 Proof. by move=> * /=; case: real_ltgtP. Qed.
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index c90bc53..cdc181c 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -2973,17 +2973,17 @@ 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_minl z : {in >=< z &, forall x y, min x y >=< z}.
+Proof. by move=> x y 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_minr z : {in >=<%O z &, forall x y, z >=< min x y}.
+Proof. by move=> x y 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_maxl z : {in >=< z &, forall x y, max x y >=< z}.
+Proof. by move=> x y 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.
+Lemma comparable_maxr z : {in >=<%O z &, forall x y, z >=< max x y}.
+Proof. by move=> x y cmp_xz cmp_yz; rewrite /max; case: ifP. Qed.
 
 Section Comparable2.
 Variables (z x y : T) (cmp_xy : x >=< y).
@@ -3165,7 +3165,7 @@ Lemma comparable_minACA x y z 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.
+by rewrite inE comparable_sym.
 Qed.
 
 Lemma comparable_maxACA x y z t :
@@ -3174,7 +3174,7 @@ Lemma comparable_maxACA x y z 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.
+by rewrite inE comparable_sym.
 Qed.
 
 Lemma comparable_max_minr x y z : x >=< y -> x >=< z -> y >=< z ->
@@ -3226,22 +3226,23 @@ Lemma nmono_in_leif (A : {pred T}) (f : T -> T) C :
   {in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)}.
 Proof. by move=> mf x y Ax Ay; rewrite /leif !eq_le !mf. Qed.
 
-Lemma nmono_leif (f : T -> T) C :
-    {mono f : x y /~ x <= y} ->
+Lemma nmono_leif (f : T -> T) C : {mono f : x y /~ x <= y} ->
   forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C).
 Proof. by move=> mf x y; rewrite /leif !eq_le !mf. Qed.
 
-Section comparable_big.
-Variables op : T -> T -> T.
-Hypothesis op_comparable : forall z, {in >=< z &, forall x y, op x y >=< z}.
+Lemma comparable_bigl x x0 op I (P : pred I) F (s : seq I) :
+  {in >=< x &, forall y z, op y z >=< x} -> x0 >=< x ->
+  {in P, forall i, F i >=< x} -> \big[op/x0]_(i <- s | P i) F i >=< x.
+Proof. by move=> *; elim/big_ind : _. Qed.
 
-Lemma comparable_big x x0 I (P : pred I) F (s : seq I) :
-  x0 >=< x -> {in P, forall t, F t >=< x} ->
-  \big[op/x0]_(i <- s | P i) F i >=< x.
-Proof. by move=> ? ?; elim/big_ind : _ => // y z; exact: op_comparable. Qed.
-End comparable_big.
+Lemma comparable_bigr x x0 op I (P : pred I) F (s : seq I) :
+  {in >=<%O x &, forall y z, x >=< op y z} -> x >=< x0 ->
+  {in P, forall i, x >=< F i} -> x >=< \big[op/x0]_(i <- s | P i) F i.
+Proof. by move=> *; elim/big_ind : _. Qed.
 
 End POrderTheory.
+Hint Resolve comparable_minr comparable_minl : core.
+Hint Resolve comparable_maxr comparable_maxl : core.
 
 Section ContraTheory.
 Context {disp1 disp2 : unit} {T1 : porderType disp1} {T2 : porderType disp2}.