update w.r.t. mathcomp master (distinction latticeType /

distrLatticeType)

theories/Rstruct.v

@@ -254,7 +254,8 @@ move=> x y; case: (Rle_lt_dec x y) => [/RleP -> //|/Rlt_le/RleP ->];
   by rewrite orbT.
 Qed.
 
-Canonical R_latticeType := DistrLatticeType R R_total.
+Canonical R_latticeType := LatticeType R R_total.
+Canonical R_distrLatticeType := DistrLatticeType R R_total.
 Canonical R_orderType := OrderType R R_total.
 Canonical R_realDomainType := [realDomainType of R].
 Canonical R_realFieldType := [realFieldType of R].

theories/altreals/distr.v

@@ -277,7 +277,7 @@ have ->: (size s = \sum_(i <- undup s) count_mem i s)%N.
   by rewrite Monoid.iteropE iter_addn addn0 mul1n.
 rewrite [X in (_<=X)%N](bigID (mem J)) /= -ltnS -addSn.
 rewrite ltn_addr //= ltnS -big_filter -[X in (_<=X)%N]big_filter.
-rewrite leq_eqVlt; apply/orP; left; apply/eqP/eq_big_perm.
+rewrite leq_eqVlt; apply/orP; left; apply/eqP/perm_big.
 apply/uniq_perm_eq; rewrite ?filter_uniq ?undup_uniq //.
 by move=> x; rewrite !mem_filter mem_undup andbC.
 Qed.

theories/altreals/realsum.v

@@ -374,8 +374,8 @@ rewrite /psum (asboolT (summable_fin f)) (@max_sup _ S).
   apply/ubP=> y /imsetbP[J ->]; apply/(big_fset_subset (F := \`|_|)).
     by move=> i; rewrite normr_ge0.
   by move=> j jJ; apply/in_imfset.
-rewrite /S -(big_map val xpredT \`|f|); apply/eq_big_perm.
-rewrite /index_enum -!enumT; apply/(perm_eq_trans _ enum_fsetT).
+rewrite /S -(big_map val xpredT \`|f|); apply/perm_big.
+rewrite /index_enum -!enumT; apply/(perm_trans _ enum_fsetT).
 apply/uniq_perm_eq; rewrite ?map_inj_uniq ?enum_uniq //=.
   by apply/val_inj. by rewrite -enumT enum_uniq.
 move=> i /=; rewrite mem_enum in_imfset //; apply/mapP.
@@ -893,7 +893,7 @@ move=> eq_r ler; set s := RHS; have h J: uniq J -> \sum_(x <- J) `|S x| <= s.
     by rewrite normr_eq0 => /ler.
   rewrite add0r {}/s -big_filter; set s := filter _ _.
   rewrite [X in _<=X](bigID (ssrbool.mem J)) /=.
-  rewrite (eq_big_perm [seq x <- r | x \in J]) /=.
+  rewrite (perm_big [seq x <- r | x \in J]) /=.
     apply/uniq_perm_eq; rewrite ?filter_uniq // => x.
     by rewrite !mem_filter andbC.
   by rewrite big_filter ler_addl sumr_ge0.
@@ -933,7 +933,7 @@ have uqpJ: uniq (pmap h' [seq j | j <- J & S j != 0]).
 exists (pmap h' [seq j | j <- J & S j != 0]) => //.
 apply/eqP; rewrite -(big_map h predT \`|S|) (bigID [pred j | S j == 0]) /=.
 rewrite big1 ?add0r => [i /eqP->|]; first by rewrite normr0.
-rewrite -big_filter; apply/eq_big_perm/uniq_perm_eq.
+rewrite -big_filter; apply/perm_big/uniq_perm_eq.
 + by rewrite filter_uniq.
 + rewrite map_inj_in_uniq // !map_id => y1 y2 h1 h2.
   move/(congr1 h'); rewrite !hP ?PS //; last by case.

theories/altreals/xfinmap.v

@@ -5,7 +5,7 @@
 
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect all_algebra.
-From mathcomp Require Export finmap.
+From mathcomp Require Export finmap bigop.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -83,7 +83,7 @@ Lemma big_seq_fset_cond (T : choiceType) (s : seq T) P F : uniq s ->
     \big[*%M/1]_(x : [fset x in s] | P (val x)) F (val x)
   = \big[*%M/1]_(x <- s | P x) F x.
 Proof.
-move=> eq_s; rewrite big_fset_seq_cond; apply/eq_big_perm.
+move=> eq_s; rewrite big_fset_seq_cond; apply/perm_big.
 by apply/uniq_perm_eq=> //= x; rewrite in_fset.
 Qed.
 
@@ -107,7 +107,7 @@ Lemma big_fsetU (A B : {fset T}) F : [disjoint A & B] ->
     op (\big[op/idx]_(j : A) F (val j))
        (\big[op/idx]_(j : B) F (val j)).
 Proof.
-move=> dj_AB; rewrite !big_fset_seq -big_cat; apply/eq_big_perm.
+move=> dj_AB; rewrite !big_fset_seq -big_cat; apply/perm_big.
 apply/uniq_perm_eq=> //.
 + rewrite cat_uniq ?uniq_fset_keys !(andbT, andTb); apply/hasPn => x /=.
   by apply/fdisjointP; rewrite fdisjoint_sym.
@@ -126,7 +126,7 @@ Proof.
 move=> ge0_F le_IJ; rewrite !big_fset_seq /=.
 rewrite [X in _<=X](bigID [pred j : T | j \in I]) /=.
 rewrite ler_paddr ?sumr_ge0 // -[X in _<=X]big_filter.
-rewrite le_eqVlt; apply/orP; left; apply/eqP/eq_big_perm.
+rewrite le_eqVlt; apply/orP; left; apply/eqP/perm_big.
 apply/uniq_perm_eq; rewrite ?filter_uniq //; last move=> i.
 rewrite mem_filter; case/boolP: (_ \in _) => //=.
 by move/le_IJ => ->.
@@ -136,7 +136,7 @@ Lemma big_nat_mkfset (F : nat -> R) n :
   \sum_(0 <= i < n) F i =
     \sum_(i : [fset x in (iota 0 n)]) F (val i).
 Proof.
-rewrite -(big_map val xpredT) /=; apply/eq_big_perm.
+rewrite -(big_map val xpredT) /=; apply/perm_big.
 apply/uniq_perm_eq; rewrite ?iota_uniq //.
   rewrite map_inj_uniq /=; last apply/val_inj.
   by rewrite /index_enum -enumT enum_uniq.

theories/ereal.v

@@ -214,9 +214,12 @@ Lemma le_total_ereal : total (@le_ereal R).
 Proof. by case=> [?||][?||] //=; exact: le_total. Qed.
 
 Definition ereal_latticeMixin :=
-  DistrLatticeMixin min_erealC max_erealC min_erealA max_erealA
-                    joinKI_ereal meetKU_ereal leEmeet_ereal meetUl_ereal.
-Canonical ereal_latticeType := DistrLatticeType {ereal R} ereal_latticeMixin.
+  LatticeMixin min_erealC max_erealC min_erealA max_erealA
+                    joinKI_ereal meetKU_ereal leEmeet_ereal.
+Canonical ereal_latticeType := LatticeType {ereal R} ereal_latticeMixin.
+Definition ereal_distrLatticeMixin := DistrLatticeMixin meetUl_ereal.
+Canonical ereal_distrLatticeType :=
+  DistrLatticeType {ereal R} ereal_distrLatticeMixin.
 Canonical ereal_orderType := OrderType {ereal R} le_total_ereal.
 
 End ERealOrder_realDomainType.

theories/posnum.v

@@ -87,7 +87,8 @@ Canonical posnum_porderType := POrderType ring_display {posnum R} posnum_porderM
 Lemma posnum_le_total : totalPOrderMixin [porderType of {posnum R}].
 Proof. by move=> x y; apply/real_comparable; apply/gtr0_real/posnum_gt0. Qed.
 
-Canonical posnum_latticeType := DistrLatticeType {posnum R} posnum_le_total.
+Canonical posnum_latticeType := LatticeType {posnum R} posnum_le_total.
+Canonical posnum_distrLatticeType := DistrLatticeType {posnum R} posnum_le_total.
 Canonical posnum_orderType := OrderType {posnum R} posnum_le_total.
 
 End Order.

theories/prodnormedzmodule.v

@@ -49,7 +49,8 @@ Canonical nngnum_porderType :=
 Lemma nngnum_le_total : totalPOrderMixin [porderType of {nonneg R}].
 Proof. by move=> x y; apply/real_comparable; apply/ger0_real. Qed.
 
-Canonical nngnum_latticeType := DistrLatticeType {nonneg R} nngnum_le_total.
+Canonical nngnum_latticeType := LatticeType {nonneg R} nngnum_le_total.
+Canonical nngnum_distrLatticeType := DistrLatticeType {nonneg R} nngnum_le_total.
 Canonical nngnum_orderType := OrderType {nonneg R} nngnum_le_total.
 
 End Order.

theories/reals.v

@@ -115,7 +115,8 @@ Definition pack b0 (m0 : mixin_of (@Num.ArchimedeanField.Pack T b0)) :=
 Definition eqType := @Equality.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
 Definition porderType := @Order.POrder.Pack ring_display cT xclass.
-Definition latticeType := @Order.DistrLattice.Pack ring_display cT xclass.
+Definition latticeType := @Order.Lattice.Pack ring_display cT xclass.
+Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass.
 Definition orderType := @Order.Total.Pack ring_display cT xclass.
 Definition zmodType := @GRing.Zmodule.Pack cT xclass.
 Definition ringType := @GRing.Ring.Pack cT xclass.
@@ -147,8 +148,10 @@ Coercion choiceType : type >-> Choice.type.
 Canonical choiceType.
 Coercion porderType : type >-> Order.POrder.type.
 Canonical porderType.
-Coercion latticeType : type >-> Order.DistrLattice.type.
+Coercion latticeType : type >-> Order.Lattice.type.
 Canonical latticeType.
+Coercion distrLatticeType : type >-> Order.DistrLattice.type.
+Canonical distrLatticeType.
 Coercion orderType : type >-> Order.Total.type.
 Canonical orderType.
 Coercion zmodType : type >-> GRing.Zmodule.type.