From 4217f37d88da59de60152626bfec74404fa8c8f1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 19 Dec 2024 17:49:35 +0900 Subject: [PATCH] upd fo MathComp 2.3.0 --- ecc_classic/alternant.v | 3 ++- ecc_classic/repcode.v | 2 +- information_theory/source_coding_vl_converse.v | 2 +- information_theory/types.v | 6 +++--- lib/f2.v | 8 ++++++-- lib/ssralg_ext.v | 3 ++- probability/bayes.v | 7 ++++--- probability/proba.v | 2 +- robust/weightedmean.v | 4 ++-- 9 files changed, 22 insertions(+), 15 deletions(-) diff --git a/ecc_classic/alternant.v b/ecc_classic/alternant.v index eafe69b0..11677b73 100644 --- 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 index a27c796f..9a9b636d 100644 --- 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 index 3d82477f..098d91bc 100644 --- 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 index c8b2c9d0..29cd2e03 100644 --- a/information_theory/types.v +++ b/information_theory/types.v @@ -244,7 +244,7 @@ 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. @@ -252,7 +252,7 @@ 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 index 68a9cc24..9753bd33 100644 --- 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 index c6b5920a..7280d23c 100644 --- 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 index 1ec195f9..f0d11776 100644 --- 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 index 70f9b18e..390cccf4 100644 --- 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 index 75e978bb..754c8bef 100644 --- 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.