upd to MathComp 2.3.0

affeldt-aist · Dec 19, 2024 · fe0d6de · fe0d6de
1 parent 1469b90
commit fe0d6de
Show file tree

Hide file tree

Showing 9 changed files with 22 additions and 15 deletions.
diff --git a/ecc_classic/alternant.v b/ecc_classic/alternant.v
@@ -54,7 +54,8 @@ Section injection_into_extension_field.
 
 Variables (F0 : finFieldType) (F1 : fieldExtType F0).
 
-Definition ext_inj : {rmorphism F0 -> F1} := @GRing.in_alg F1.
+Definition ext_inj : {rmorphism F0 -> F1} :=
+ [the {rmorphism F0 -> F1} of @GRing.in_alg _ _].
 
 Definition ext_inj_tmp : {rmorphism F0 -> (FinFieldExtType F1)} := ext_inj.
 

diff --git a/ecc_classic/repcode.v b/ecc_classic/repcode.v
@@ -57,7 +57,7 @@ rewrite (_ : tuple_of_row _ =
     [tuple of map (fun x => F2_of_bool (x != a%R)) (tuple_of_row v)]); last first.
   apply eq_from_tnth => i.
   rewrite tnth_mktuple tnth_map tnth_mktuple !mxE.
-  by case/F2P : a; case: F2P => //; rewrite subrr.
+  by case/F2P : a; case: F2P => //; rewrite ?subrr ?subr0 ?sub0r ?oppr_char2.
 rewrite {1}/num_occ count_map /preim.
 apply eq_count => /= x.
 rewrite !inE.

diff --git a/information_theory/source_coding_vl_converse.v b/information_theory/source_coding_vl_converse.v
@@ -829,7 +829,7 @@ apply: (@leR_trans (x + ln alp)).
   apply: (@ltR_trans (exp x - 1)); last exact: proj1 (floorP _).
   rewrite subR_gt0 -exp_0; exact: exp_increasing.
 apply: (@leR_trans (2 * x - (eps * INR n * ln 2))).
-  rewrite double /Rminus -addRA leR_add2l addR_opp leR_subr_addr (mulRC eps).
+  rewrite -Rplus_diag /Rminus -addRA leR_add2l addR_opp leR_subr_addr (mulRC eps).
   apply: (@leR_trans (IZR (ceil (ln alp + n%:R * eps * ln 2)))); first exact: proj1 (ceilP _).
   rewrite -INR_Zabs_nat; first exact/le_INR/leP/leq_maxl.
   apply: le_IZR.

diff --git a/information_theory/types.v b/information_theory/types.v
@@ -244,15 +244,15 @@ refine (Some (@type.mkType _ _ (fdist_of_ffun (proj2_sig f)) (sval f) (fdist_of_
 Defined.
 
 Definition type_enum A n := pmap (@type_enum_f A n)
-  (enum [finType of {f : {ffun A -> 'I_n.+1} | (\sum_(a in A) f a)%nat == n}]).
+  (enum [the finType of {f : {ffun A -> 'I_n.+1} | (\sum_(a in A) f a)%nat == n}]).
 
 Lemma type_enumP A n : finite_axiom (@type_enum A n).
 Proof.
 destruct n.
   case=> d t H /=; by move: (no_0_type H).
 case=> d t H /=.
 move: (ffun_of_fdist H) => H'.
-have : Finite.axiom (enum [finType of { f : {ffun A -> 'I_n.+2} | (\sum_(a in A) f a)%nat == n.+1}]).
+have : Finite.axiom (enum [the finType of { f : {ffun A -> 'I_n.+2} | (\sum_(a in A) f a)%nat == n.+1}]).
   rewrite enumT; by apply enumP.
 move/(_ (@exist {ffun A -> 'I_n.+2} (fun f => \sum_(a in A) f a == n.+1)%nat t H')) => <-.
 rewrite /type_enum /= /type_enum_f /= count_map.
@@ -286,7 +286,7 @@ Lemma type_card_neq0 n : 0 < #|A| -> 0 < #|P_ n.+1(A)|.
 Proof.
 case/card_gt0P => a _.
 apply/card_gt0P.
-have [f Hf] : [finType of {f : {ffun A -> 'I_n.+2} | \sum_(a in A) f a == n.+1}].
+have [f Hf] : [the finType of {f : {ffun A -> 'I_n.+2} | \sum_(a in A) f a == n.+1}].
   exists [ffun a1 => if pred1 a a1 then Ordinal (ltnSn n.+1) else Ordinal (ltn0Sn n.+1)].
   rewrite (bigD1 a) //= big1; first by rewrite ffunE eqxx addn0.
   move=> p /negbTE Hp; by rewrite ffunE Hp.

diff --git a/lib/f2.v b/lib/f2.v
@@ -52,7 +52,9 @@ Lemma expr2_char2 x : x ^+ 2 = x.
 Proof. by case/F2P : x; rewrite ?expr0n ?expr1n. Qed.
 
 Lemma F2_of_bool_addr x y : x + (y == 0) = ((x + y) == 0).
-Proof. case/F2P : x y; case/F2P => //=; by rewrite ?addr0 ?addrr_char2. Qed.
+Proof.
+by case/F2P : x y; case/F2P => //=; by rewrite ?(addr0,add0r,addrr_char2).
+Qed.
 
 Lemma F2_of_bool_0_inv b : F2_of_bool b = 0 -> b = false.
 Proof. by case: b. Qed.
@@ -73,7 +75,9 @@ Lemma bool_of_F2_add_xor x y :
 Proof. move: x y; by case/F2P; case/F2P. Qed.
 
 Lemma morph_F2_of_bool : {morph F2_of_bool : x y / x (+) y >-> (x + y) : 'F_2}.
-Proof. rewrite /F2_of_bool; case; case => //=; by rewrite addrr_char2. Qed.
+Proof.
+by rewrite /F2_of_bool; case; case => //=; rewrite ?(addr0,add0r,addrr_char2).
+Qed.
 
 Lemma morph_bool_of_F2 : {morph bool_of_F2 : x y / (x + y) : 'F_2 >-> x (+) y}.
 Proof. move=> x y /=; by rewrite bool_of_F2_add_xor. Qed.

diff --git a/lib/ssralg_ext.v b/lib/ssralg_ext.v
@@ -33,7 +33,8 @@ Import Prenex Implicits.
 Import GRing.Theory.
 Local Open Scope ring_scope.
 
-Notation "x '``_' i" := (x ord0 i) (at level 9) : vec_ext_scope.
+Notation "u '``_' i" := (u ord0 i) (at level 3,
+  i at level 2, left associativity, format "u '``_' i") : vec_ext_scope.
 Reserved Notation "v `[ i := x ]" (at level 20).
 Reserved Notation "t \# V" (at level 55, V at next level).
 

diff --git a/probability/bayes.v b/probability/bayes.v
@@ -108,14 +108,14 @@ Section univ_types.
 Variable n : nat.
 Variable types : 'I_n -> eqType.
 Definition univ_types : eqType :=
-  [eqType of {dffun forall i, types i}].
+  [the eqType of {dffun forall i, types i}].
 
 Section prod_types.
 (* sets of indices *)
 Variable I : {set 'I_n}.
 
 Definition prod_types :=
-  [eqType of
+  [the eqType of
    {dffun forall i : 'I_n, if i \in I then types i else unit}].
 
 Lemma prod_types_app i (A B : prod_types) : A = B -> A i = B i.
@@ -746,7 +746,8 @@ split.
   rewrite negb_imply /vals => /andP [Hif].
   case /boolP: (i \in g) => Hig.
     (* B and C are incompatible *)
-    by move: (Hfg i); rewrite inE Hif Hig /= (set_vals_hd vals0) // => ->.
+    move: (Hfg i); rewrite inE Hif Hig /= => /eqP <-.
+    by rewrite (set_vals_hd vals0) // eqxx.
   case /boolP: (i \in e) => Hie;
     last by rewrite set_vals_tl // set_vals_tl // eqxx.
   (* A and B are incompatible *)

diff --git a/probability/proba.v b/probability/proba.v
@@ -551,7 +551,7 @@ Notation "`Pr[ X = a ]" := (pr_eq X a) : proba_scope.
 Global Hint Resolve pr_eq_ge0 : core.
 
 Section random_variable_order.
-Variables (U : finType) (d : unit) (T : porderType d) (P : R.-fdist U).
+Context (U : finType) d (T : porderType d) (P : R.-fdist U).
 Variables (X : {RV P -> T}).
 
 Definition pr_geq (X : {RV P -> T}) r := Pr P [set x | (X x >= r)%O ].

diff --git a/robust/weightedmean.v b/robust/weightedmean.v
@@ -125,7 +125,7 @@ Lemma wpmulr_rgt0 (R : numDomainType) (x y : R) : 0 <= x -> 0 < x * y -> 0 < y.
 Proof. rewrite mulrC; exact: wpmulr_lgt0. Qed.
 
 (* eqType version of order.bigmax_le *)
-Lemma bigmax_le' (disp : unit) (T : porderType disp) (I : eqType) (r : seq I) (f : I -> T)
+Lemma bigmax_le' disp (T : porderType disp) (I : eqType) (r : seq I) (f : I -> T)
     (x0 x : T) (PP : pred I) :
   (x0 <= x)%O ->
   (forall i : I, i \in r -> PP i -> (f i <= x)%O) ->
@@ -135,7 +135,7 @@ move=> x0x cond; rewrite big_seq_cond bigmax_le // => ? /andP [? ?]; exact: cond
 Qed.
 
 (* seq version of order.bigmax_leP *)
-Lemma bigmax_leP_seq (disp : unit) (T : orderType disp) (I : eqType) (r : seq I) (F : I -> T)
+Lemma bigmax_leP_seq disp (T : orderType disp) (I : eqType) (r : seq I) (F : I -> T)
     (x m : T) (PP : pred I) :
 reflect ((x <= m)%O /\ (forall i : I, i \in r -> PP i -> (F i <= m)%O))
   (\big[Order.max/x]_(i <- r | PP i) F i <= m)%O.