From 3b6ce62f00e5224306564d62f577270954828dc0 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 23 Apr 2024 18:42:03 +0200 Subject: [PATCH] [WIP] Adapt to math-comp/math-comp#1213 --- classical/mathcomp_extra.v | 19 +++++++++++++++++++ theories/ereal.v | 4 ++-- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index b081c77b2..c8322b7d5 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -281,6 +281,25 @@ Proof. by move=> x y ? ?; rewrite -[in LHS](@invrK _ y) ltf_pV2// posrE invr_gt0. Qed. +(* cf. math-comp/math-comp#1213 *) +Disable Notation "\0" : ring_scope. +Disable Notation "f \+ g" : ring_scope. +Disable Notation "f \- g" : ring_scope. +Disable Notation "\- f" : ring_scope. +Disable Notation "a \*: f" : ring_scope. +Disable Notation "x \*o f" : ring_scope. +Disable Notation "x \o* f" : ring_scope. +Disable Notation "f \* g" : ring_scope. + +Notation "\0" := (GRing.null_fun _) : function_scope. +Notation "f \+ g" := (GRing.add_fun f g) : function_scope. +Notation "f \- g" := (GRing.sub_fun f g) : function_scope. +Notation "\- f" := (GRing.opp_fun f) : function_scope. +Notation "a \*: f" := (GRing.scale_fun a f) : function_scope. +Notation "x \*o f" := (GRing.mull_fun x f) : function_scope. +Notation "x \o* f" := (GRing.mulr_fun x f) : function_scope. +Notation "f \* g" := (GRing.mul_fun f g) : function_scope. + (**********************) (* not yet backported *) (**********************) diff --git a/theories/ereal.v b/theories/ereal.v index da591ceb3..b45868954 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -111,12 +111,12 @@ Proof. by move=> mh; apply/funext => t /=; rewrite mh. Qed. Lemma compreN T (h : R -> \bar R) (f : T -> R) : {morph h : x / (- x)%R >-> (- x)%E} -> - h \o (\- f)%R = \- (h \o f)%E. + h \o (\- f) = \- (h \o f)%E. Proof. by move=> mh; apply/funext => t /=; rewrite mh. Qed. Lemma compreBr T (h : R -> \bar R) (f g : T -> R) : {morph h : x y / (x - y)%R >-> (x - y)%E} -> - h \o (f \- g)%R = ((h \o f) \- (h \o g))%E. + h \o (f \- g) = ((h \o f) \- (h \o g))%E. Proof. by move=> mh; apply/funext => t /=; rewrite mh. Qed. Lemma compre_scale T (h : R -> \bar R) (f : T -> R) k :