From 0e6f9ebe54c6601d499c56819807411a1eb3232b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Jun 2025 09:54:26 +0200 Subject: [PATCH] adapt to rocq-prover/rocq#20707 --- analysis_stdlib/showcase/uniform_bigO.v | 2 +- classical/classical_sets.v | 2 +- classical/contra.v | 2 +- classical/functions.v | 2 +- reals/constructive_ereal.v | 6 +++--- theories/convex.v | 4 ++-- theories/derive.v | 5 +++-- theories/ftc.v | 6 +++--- theories/function_spaces.v | 4 ++-- theories/lebesgue_integral_theory/lebesgue_integrable.v | 4 ++-- theories/measure.v | 2 +- theories/normedtype_theory/normed_module.v | 2 +- theories/normedtype_theory/num_normedtype.v | 4 ++-- theories/probability.v | 2 +- theories/sequences.v | 2 +- theories/topology_theory/num_topology.v | 2 +- 16 files changed, 26 insertions(+), 25 deletions(-) diff --git a/analysis_stdlib/showcase/uniform_bigO.v b/analysis_stdlib/showcase/uniform_bigO.v index 73d1bc7728..38e10e310f 100644 --- a/analysis_stdlib/showcase/uniform_bigO.v +++ b/analysis_stdlib/showcase/uniform_bigO.v @@ -53,7 +53,7 @@ wlog lex12 : x / (`|x.1| <= `|x.2|). by rewrite addrC [`|_|]maxC (ler_norm (x.2, x.1)). rewrite [`|_|]max_r // -[X in X * _]ger0_norm // -normrM. rewrite -sqrtr_sqr ler_wsqrtr // exprMn sqr_sqrtr // mulr_natl mulr2n lerD2r. -rewrite -[_ ^+ 2]ger0_norm ?sqr_ge0 // -[X in _ <=X]ger0_norm ?sqr_ge0 //. +rewrite -[leLHS]ger0_norm ?sqr_ge0 // -[leRHS]ger0_norm ?sqr_ge0 //. by rewrite !normrX lerXn2r // nnegrE normr_ge0. Qed. diff --git a/classical/classical_sets.v b/classical/classical_sets.v index a4ef934c72..44ff437757 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2808,7 +2808,7 @@ apply/trivIsetP => i j Di Dj ij. rewrite {}s12 {s2}; have [si|si] := ltnP i (size s); last first. by rewrite (nth_default set0) ?size_map// set0I. rewrite (nth_map O) //; have [sj|sj] := ltnP j (size s); last first. - by rewrite (nth_default set0) ?size_map// setI0. + by rewrite setIC (nth_default set0) ?size_map// set0I. have nth_mem k : k < size s -> nth O s k \in iota 0 (size s1). by move=> ?; rewrite -(perm_mem ss1) mem_nth. rewrite (nth_map O)// ts1 ?(nth_uniq,(perm_uniq ss1),iota_uniq)//; apply/s1D. diff --git a/classical/contra.v b/classical/contra.v index 807f6bb94a..0a9e1aa0d6 100644 --- a/classical/contra.v +++ b/classical/contra.v @@ -510,7 +510,7 @@ Proof. by move: b => [] [] /= <-; exact/propext. Qed. Canonical false_neq P b := BoolNeqRHS (@false_neqP P b). Local Fact eqType_neqP (T : eqType) (x y : T) : (x <> y) = (x != y). -Proof. by rewrite (reflect_eq eqP) (reflect_eq negP). Qed. +Proof. by rewrite [in LHS](reflect_eq eqP) (reflect_eq negP). Qed. Canonical eqType_neq (T : eqType) x y := @NeqRHS (x != y) T x (Wrap y) (eqType_neqP x y). Local Fact eq_op_posP (T : eqType) x y : (x == y :> T : Prop) = (x = y). diff --git a/classical/functions.v b/classical/functions.v index bf13ef3e57..4215676d16 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -2455,7 +2455,7 @@ End set_bij_lemmas. Lemma bij_II_D1 T n (A : set T) (f : nat -> T) : set_bij `I_n.+1 A f -> set_bij `I_n (A `\ f n) f. Proof. -rewrite IIS -image_set1; apply: bij_sub_setUll. +rewrite IIS -[[set f n]]image_set1; apply: bij_sub_setUll. by apply/disj_setPS => i [/= /[swap]->]; rewrite ltnn. Qed. diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index b17b229537..62d1e593df 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -820,7 +820,7 @@ Proof. exact: raddfMn. Qed. Lemma prodEFin T s (P : pred T) (f : T -> R) : \prod_(i <- s | P i) (f i)%:E = (\prod_(i <- s | P i) f i)%:E. -Proof. by elim/big_ind2 : _ => // _ x _ y -> ->; rewrite EFinM. Qed. +Proof. by elim/big_ind2 : _ => // ? x ? y -> ->; rewrite EFinM. Qed. Lemma sumEFin I s P (F : I -> R) : \sum_(i <- s | P i) (F i)%:E = (\sum_(i <- s | P i) F i)%:E. @@ -916,7 +916,7 @@ Lemma adde_defNN x y : - x +? - y = x +? y. Proof. by rewrite adde_defN oppeK. Qed. Lemma oppe_eq0 x : (- x == 0)%E = (x == 0)%E. -Proof. by rewrite -(can_eq oppeK) oppe0. Qed. +Proof. by rewrite -[RHS](can_eq oppeK) oppe0. Qed. Lemma oppeD x y : x +? y -> - (x + y) = - x - y. Proof. by move: x y => [x| |] [y| |] //= _; rewrite opprD. Qed. @@ -2483,7 +2483,7 @@ move: x => [x|_|//]. move=> [y| |] [z| |]//; first by rewrite !lee_fin// ler_pM2r. - by move=> _; rewrite mulr_infty gtr0_sg// mul1e leey. - by move=> _; rewrite mulr_infty gtr0_sg// mul1e leNye. - - by move=> _; rewrite 2!mulr_infty gtr0_sg// 2!mul1e. + - by move=> _; rewrite mulNyr mulyr gtr0_sg// 2!mul1e. move=> [y| |] [z| |]//. - rewrite lee_fin => yz. have [z0|z0|] := ltgtP 0%R z. diff --git a/theories/convex.v b/theories/convex.v index 4894d15738..40a81aedc3 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -336,9 +336,9 @@ have LfE : L x - f x = have {Hc1 Hc2} -> : L x - f x = (b - x) * (x - a) * (c2 - c1) / (b - a) * (('D_1 f c2 - 'D_1 f c1) / (c2 - c1)). rewrite LfE Hc2 Hc1. - rewrite -(mulrC (b - x)) mulrA -mulrBr. + rewrite -(mulrC (b - x)) [in LHS]mulrA -mulrBr. rewrite (mulrC ('D_1 f c2 - _)) ![in RHS]mulrA; congr *%R. - rewrite -2!mulrA; congr *%R. +rewrite -2![RHS]mulrA; congr *%R. by rewrite mulrCA divff ?mulr1// subr_eq0 gt_eqF. rewrite {}h mulr_ge0//; last first. rewrite DDf_ge0//; apply/andP; split. diff --git a/theories/derive.v b/theories/derive.v index 6ccc738962..419c54179a 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -542,7 +542,8 @@ exists df; split=> //; apply: eqaddoEx => z. rewrite (hdf _ dxf) !addrA lim_id // /(_ \o _) /= subrK [f _ + _]addrC addrK. rewrite -addrA -[LHS]addr0; congr (_ + _). apply/eqP; rewrite eq_sym addrC addr_eq0 oppox; apply/eqP. -by rewrite littleo_center0 (comp_centerK x id) -[- _ in RHS](comp_centerK x). +rewrite [in LHS]littleo_center0 (comp_centerK x id). +by rewrite -[- _ in RHS](comp_centerK x). Qed. Lemma diff_cst (V W : normedModType R) a x : ('d (cst a) x : V -> W) = 0. @@ -1910,7 +1911,7 @@ have Dhx : D° (h + x). by near: h; apply: dnbhs0_lt; exact: mulr_gt0. by rewrite normrM ger0_norm// mulr_gt0// normr_gt0. apply: ball_sym; rewrite /ball/= addrK. - by rewrite normrM ger0_norm// ltr_pMl ?normr_gt0// ltr1n. + by rewrite normrM (@ger0_norm _ 2)// ltr_pMl ?normr_gt0// ltr1n. move: h0; rewrite neq_lt => /orP[h0|h0]. - rewrite nmulr_rle0 ?invr_lt0// subr_ge0 ltW//. by apply: decrf; rewrite ?in_itv ?andbT ?gtrDr// inE; exact: interior_subset. diff --git a/theories/ftc.v b/theories/ftc.v index 4e400f5fbc..9cd8670664 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1031,7 +1031,7 @@ Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l. Proof. have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK. -by rewrite (eq_cvg -oo _ f_opp) fmap_comp ninftyN. +by rewrite (eq_cvg -oo _ f_opp) [in X in X <-> _]fmap_comp ninftyN. Qed. (* PR in progress *) @@ -1040,7 +1040,7 @@ Lemma cvgy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) f x @[x --> +oo] --> l <-> (f \o -%R) x @[x --> -oo] --> l. Proof. have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK. -by rewrite (eq_cvg +oo _ f_opp) fmap_comp ninfty. +by rewrite (eq_cvg +oo _ f_opp) [in X in X <-> _]fmap_comp ninfty. Qed. Section integration_by_substitution. @@ -1606,7 +1606,7 @@ rewrite (@increasing_ge0_integration_by_substitutiony (\- (F \o -%R))%R); last 8 apply: dFcompN. rewrite ltrNl. by near: z; exact: nbhs_right_gt. - rewrite fctE derive1_comp; last 2 first. + rewrite fctE [LHS]derive1_comp; last 2 first. exact: derivable_id. apply: dFN; rewrite ltrNl. by near: z; exact: nbhs_right_gt. diff --git a/theories/function_spaces.v b/theories/function_spaces.v index 1029195f9b..8be463b539 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -707,8 +707,8 @@ Lemma uniform_set1 F (f : U -> V) (x : U) : Filter F -> {uniform [set x], F --> f} = (g x @[g --> F] --> f x). Proof. move=> FF; rewrite propeqE; split. - move=> + W => /(_ [set t | W (t x)]) +; rewrite -nbhs_entourageE. - rewrite uniform_nbhs => + [Q entQ subW]. + move=> + W => /(_ [set t | W (t x)]) +. + rewrite -[in X in _ -> X]nbhs_entourageE uniform_nbhs => + [Q entQ subW]. by apply; exists Q; split => // h Qf; exact/subW/xsectionP/Qf. move=> Ff W; rewrite uniform_nbhs => [[E] [entE subW]]. apply: (filterS subW); move/(nbhs_entourage (f x))/Ff: entE => //=; near_simpl. diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index d147e9c45d..9541850c83 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -772,8 +772,8 @@ Lemma integral_pushforward : measurable D -> \int[mu]_(x in phi @^-1` D) (f \o phi) x. Proof. move=> mD. -rewrite integralE. -under [X in X - _]eq_integral do rewrite funepos_comp. +rewrite [RHS]integralE. +under [X in X - _]eq_integral do rewrite funepos_comp/=. under [X in _ - X]eq_integral do rewrite funeneg_comp. rewrite -[X in _ = X - _]ge0_integral_pushforward//; last first. exact/measurable_funepos/measurable_funTS. diff --git a/theories/measure.v b/theories/measure.v index 0082423969..0ff89b1626 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -5439,7 +5439,7 @@ move=> /(_ F') /=. have -> : F' Y = F (f @^-1` Y) by rewrite /F' /image_set_system /= setTI. move=> /[swap] bigF; apply; split; first exact: sigma_algebra_image. move=> A; rewrite /= {}/F' /image_set_system /= setTI. -set bign := (X in X A) => bignA. +set bign := (X in X A -> _) => bignA. apply: bigF; rewrite big_ord_recl /=; right. set bign1 := (X in X (_ @^-1` _)). have -> : bign1 = preimage_set_system [set: n.+1.-tuple T] f bign. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 7e4e29a10d..7270947475 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -810,7 +810,7 @@ Proof. by move=> /cvg_ex[l fl]; apply: (cvgP (- l)); exact: cvgeN. Qed. Lemma is_cvgeNE f : cvg (\- f @ F) = cvg (f @ F). Proof. rewrite propeqE; split=> /cvgeNP/cvgP//. -by under eq_is_cvg do rewrite oppeK. +by under [X in X -> _]eq_is_cvg do rewrite oppeK. Qed. Lemma mule_continuous (r : R) : continuous (mule r%:E). diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v index 2614461ead..0ac8720f61 100644 --- a/theories/normedtype_theory/num_normedtype.v +++ b/theories/normedtype_theory/num_normedtype.v @@ -533,7 +533,7 @@ Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l. Proof. have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK. -by rewrite (eq_cvg -oo _ f_opp) fmap_comp ninftyN. +by rewrite (eq_cvg -oo _ f_opp) [in X in X <-> _]fmap_comp ninftyN. Qed. #[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `cvgNy_compNP`")] Notation cvgyNP := cvgNy_compNP (only parsing). @@ -543,7 +543,7 @@ Lemma cvgy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) f x @[x --> +oo] --> l <-> (f \o -%R) x @[x --> -oo] --> l. Proof. have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK. -by rewrite (eq_cvg +oo _ f_opp) fmap_comp ninfty. +by rewrite (eq_cvg +oo _ f_opp) [in X in X <-> _]fmap_comp ninfty. Qed. Section monotonic_itv_bigcup. diff --git a/theories/probability.v b/theories/probability.v index 94e68d97c3..b5bcf58e6f 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1592,7 +1592,7 @@ Let integral_normal_fun : sigma != 0 -> (\int[mu]_x (normal_fun x)%:E)%E = normal_peak^-1%:E. Proof. move=> s0; rewrite -integral_gaussFF'//; apply: eq_integral => /= x _. -rewrite F'E !fctE/= EFinM -muleA -EFinM mulVf ?mulr1. +rewrite F'E !fctE/= EFinM -muleA -EFinM mulVf ?mulr1 ?mule1. by rewrite normal_gauss_fun. by rewrite gt_eqF// sqrtr_gt0 pmulrn_lgt0// exprn_even_gt0. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index 08efc491c0..d4bfe00040 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -834,7 +834,7 @@ case => [|n]. rewrite /arithmetic_mean/= invr1 mul1r !seriesEnat/=. by rewrite big_nat1 subrr big_geq. rewrite /arithmetic_mean /= seriesEnat /= big_nat_recl //=. -under eq_bigr do rewrite eq_sum_telescope. +under eq_bigr do rewrite [u_ _]eq_sum_telescope. rewrite big_split /= big_const_nat iter_addr addr0 addrA -mulrS mulrDr. rewrite -(mulr_natl (u_ O)) mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r opprD addrA. rewrite eq_sum_telescope (addrC (u_ O)) addrK. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index 7a213364c3..28d54db18e 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -212,7 +212,7 @@ Qed. Lemma nearN {R : numFieldType} (x : R) (P : R -> Prop) : (\forall y \near - x, P y) <-> \near x, P (- x). -Proof. by rewrite -near_simpl nbhsN. Qed. +Proof. by rewrite -[X in X <-> _]near_simpl nbhsN. Qed. Lemma openN {R : numFieldType} (A : set R) : open A -> open [set - x | x in A]. Proof.