From d2c1665a138622519c3e72e2c4a54b82ff04f602 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Mon, 8 Jan 2024 13:36:27 +0100 Subject: [PATCH] Redefine \min and \max in function_scope --- classical/mathcomp_extra.v | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 0873e2ba2..e01a9795b 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -15,8 +15,6 @@ From mathcomp Require Import finset interval. (******************************************************************************) (* This files contains lemmas and definitions missing from MathComp. *) (* *) -(* f \max g := fun x => Num.max (f x) (g x) *) -(* f \min g := fun x => Num.min (f x) (g x) *) (* oflit f := Some \o f *) (* pred_oapp T D := [pred x | oapp (mem D) false x] *) (* f \* g := fun x => f x * g x *) @@ -39,10 +37,12 @@ Unset Printing Implicit Defensive. Reserved Notation "f \* g" (at level 40, left associativity). Reserved Notation "f \- g" (at level 50, left associativity). Reserved Notation "\- f" (at level 35, f at level 35). -Reserved Notation "f \max g" (at level 50, left associativity). Number Notation positive Pos.of_num_int Pos.to_num_uint : AC_scope. +Notation "f \min g" := (Order.min_fun f g) : function_scope. +Notation "f \max g" := (Order.max_fun f g) : function_scope. + Lemma all_sig2_cond {I : Type} {T : Type} (D : pred I) (P Q : I -> T -> Prop) : T -> (forall x : I, D x -> {y : T | P x y & Q x y}) -> @@ -305,10 +305,6 @@ Qed. Lemma eqbLR (b1 b2 : bool) : b1 = b2 -> b1 -> b2. Proof. by move->. Qed. -Definition max_fun T (R : numDomainType) (f g : T -> R) x := Num.max (f x) (g x). -Notation "f \max g" := (max_fun f g) : ring_scope. -Arguments max_fun {T R} _ _ _ /. - Lemma gtr_opp (R : numDomainType) (r : R) : (0 < r)%R -> (- r < r)%R. Proof. by move=> n0; rewrite -subr_lt0 -opprD oppr_lt0 addr_gt0. Qed. @@ -831,12 +827,6 @@ rewrite horner_poly !big_ord_recr !big_ord0/= !Monoid.simpm/= expr1. by rewrite -mulrA -expr2 addrC addrA addrAC. Qed. -Reserved Notation "f \min g" (at level 50, left associativity). - -Definition min_fun T (R : numDomainType) (f g : T -> R) x := Num.min (f x) (g x). -Notation "f \min g" := (min_fun f g) : ring_scope. -Arguments min_fun {T R} _ _ _ /. - (* NB: Coq 8.17.0 generalizes dependent_choice from Set to Type making the following lemma redundant *) Section dependent_choice_Type.