From 1e13b1ba6e769a3ee80990056ae439d400c1d068 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 1 May 2025 00:18:30 +0900 Subject: [PATCH] rm warnings --- theories/function_spaces.v | 43 ++++++++++--------- .../lebesgue_integral_definition.v | 3 +- theories/realfun.v | 1 - theories/topology_theory/matrix_topology.v | 7 --- theories/topology_theory/num_topology.v | 8 ++-- 5 files changed, 27 insertions(+), 35 deletions(-) diff --git a/theories/function_spaces.v b/theories/function_spaces.v index e340cb5c9a..4d9cd02ab6 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -109,7 +109,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Obligation Tactic := idtac. +Local Obligation Tactic := idtac. Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope classical_set_scope. @@ -152,13 +152,13 @@ HB.instance Definition _ (U : Type) (T : U -> uniformType) := Uniform.copy (forall x : U, T x) (prod_topology T). HB.instance Definition _ (U T : topologicalType) := - Topological.copy - (continuousType U T) + Topological.copy + (continuousType U T) (weak_topology (id : continuousType U T -> (U -> T))). HB.instance Definition _ (U : topologicalType) (T : uniformType) := - Uniform.copy - (continuousType U T) + Uniform.copy + (continuousType U T) (weak_topology (id : continuousType U T -> (U -> T))). End ArrowAsProduct. @@ -222,9 +222,9 @@ Lemma tychonoff (I : eqType) (T : I -> topologicalType) (forall i, compact (A i)) -> compact [set f : forall i, T i | forall i, A i (f i)]. Proof. -case: (pselect ([set f : forall i, T i | forall i, A i (f i)] == set0)). - move/eqP => -> _; exact: compact0. -case/negP/set0P=> a0 Aa0 Aco; rewrite compact_ultra => F FU FA. +have [-> _|] := eqVneq [set f : forall i, T i | forall i, A i (f i)] set0. + exact: compact0. +case/set0P => a0 Aa0 Aco; rewrite compact_ultra => F FU FA. set subst_coord := fun (i : I) (pi : T i) (f : forall x : I, T x) (j : I) => if eqP is ReflectT e then ecast i (T i) (esym e) pi else f j. have subst_coordT i pi f : subst_coord i pi f i = pi. @@ -244,12 +244,12 @@ have pFA i : pF i (A i). move=> Aipi; have [f Af] := filter_ex FA. exists (subst_coord i pi f); last exact: subst_coordT. move=> j; have [<-{j}|] := eqVneq i j; first by rewrite subst_coordT. - by move=> /subst_coordN ->; apply: Af. + by move=> /subst_coordN ->; exact: Af. have cvpFA i : A i `&` [set p | pF i --> p] !=set0. by rewrite -ultra_cvg_clusterE; apply: Aco. exists (fun i => xget (a0 i) (A i `&` [set p | pF i --> p])). split=> [i|]; first by have /(xgetPex (a0 i)) [] := cvpFA i. -apply/cvg_sup => i; apply/cvg_image=> //. +apply/cvg_sup => i; apply/cvg_image=> //. by have /(xgetPex (a0 i)) [] := cvpFA i. Qed. @@ -423,11 +423,9 @@ Qed. End product_embeddings. -Global Instance prod_topology_filter (U : Type) (T : U -> ptopologicalType) (f : prod_topology T) : - ProperFilter (nbhs f). -Proof. -exact: nbhs_pfilter. -Qed. +Global Instance prod_topology_filter (U : Type) (T : U -> ptopologicalType) + (f : prod_topology T) : ProperFilter (nbhs f). +Proof. exact: nbhs_pfilter. Qed. End product_spaces. @@ -514,8 +512,11 @@ Unshelve. all: by end_near. Qed. HB.instance Definition _ := Uniform_isComplete.Build (arrow_uniform_type T U) fun_complete. -HB.instance Definition _ (R : numFieldType) := - Uniform_isComplete.Build (arrow_uniform_type T U) cauchy_cvg. +(*HB.instance Definition _ (R : numFieldType) := + Uniform_isComplete.Build (arrow_uniform_type T U) cauchy_cvg.*) +(* NB: commented out because +Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] +*) End fun_Complete. @@ -554,13 +555,13 @@ HB.instance Definition _ (U : choiceType) (R : numFieldType) PseudoMetric.copy (U -> V) (arrow_uniform_type U V). HB.instance Definition _ (U : topologicalType) (T : uniformType) := - Uniform.copy - (continuousType U T) + Uniform.copy + (continuousType U T) (weak_topology (id : continuousType U T -> (U -> T))). -HB.instance Definition _ (U : topologicalType) (R : realType) +HB.instance Definition _ (U : topologicalType) (R : realType) (T : pseudoMetricType R) := - PseudoMetric.on + PseudoMetric.on (weak_topology (id : continuousType U T -> (U -> T))). End ArrowAsUniformType. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index b9fbb69180..572c789f4d 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -65,8 +65,7 @@ Proof. by []. Qed. End simple_fun_raw_integral. -#[global] Hint Extern 0 (is_true (0 <= (_ : {measure set _ -> \bar _}) _)%E) => - solve [apply: measure_ge0] : core. +#[global] Hint Extern 0 (is_true (0 <= _)) => solve [apply: measure_ge0] : core. Section sintegral_lemmas. Context d (T : sigmaRingType d) (R : realType). diff --git a/theories/realfun.v b/theories/realfun.v index c0b85b131f..23ca76c590 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -38,7 +38,6 @@ From mathcomp Require Import normedtype derive sequences real_interval. (* total_variation a b f == the sup over all variations of f from a to b *) (* neg_tv a f x == the decreasing component of f *) (* pos_tv a f x == the increasing component of f *) -(* *) (* ``` *) (* *) (* Limit superior and inferior for functions: *) diff --git a/theories/topology_theory/matrix_topology.v b/theories/topology_theory/matrix_topology.v index 7c7de95ffb..22a51d9d69 100644 --- a/theories/topology_theory/matrix_topology.v +++ b/theories/topology_theory/matrix_topology.v @@ -53,13 +53,6 @@ HB.instance Definition _ := Nbhs_isNbhsTopological.Build 'M[T]_(m, n) End matrix_Topology. -Section matrix_PointedTopology. -Variables (m n : nat) (T : pointedType). -Implicit Types M : 'M[T]_(m, n). -HB.instance Definition _ := Pointed.on 'M[T]_(m, n). - -End matrix_PointedTopology. - Section matrix_Uniform. Local Open Scope relation_scope. Variables (m n : nat) (T : uniformType). diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index 8521246fd5..df8f42623f 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -109,12 +109,12 @@ by apply: contra_not_neq AsupA => <-. Qed. Lemma right_bounded_interior (R : realType) (X : set R) : - has_ubound X -> X^° `<=` [set r | r < sup X]. + has_ubound X -> X° `<=` [set r | r < sup X]. Proof. move=> uX r Xr; rewrite /mkset ltNge; apply/negP. rewrite le_eqVlt => /orP[/eqP supXr|]; last first. by apply/negP; rewrite -leNgt sup_ubound//; exact: interior_subset. -suff : ~ X^° (sup X) by rewrite supXr. +suff : ~ X° (sup X) by rewrite supXr. case/nbhs_ballP => _/posnumP[e] supXeX. have [f XsupXf] : exists f : {posnum R}, X (sup X + f%:num). exists (e%:num / 2)%:pos; apply supXeX; rewrite /ball /= opprD addNKr normrN. @@ -124,12 +124,12 @@ by apply/negP; rewrite -ltNge; rewrite ltrDl. Qed. Lemma left_bounded_interior (R : realType) (X : set R) : - has_lbound X -> X^° `<=` [set r | inf X < r]. + has_lbound X -> X° `<=` [set r | inf X < r]. Proof. move=> lX r Xr; rewrite /mkset ltNge; apply/negP. rewrite le_eqVlt => /orP[/eqP rinfX|]; last first. by apply/negP; rewrite -leNgt inf_lbound//; exact: interior_subset. -suff : ~ X^° (inf X) by rewrite -rinfX. +suff : ~ X° (inf X) by rewrite -rinfX. case/nbhs_ballP => _/posnumP[e] supXeX. have [f XsupXf] : exists f : {posnum R}, X (inf X - f%:num). exists (e%:num / 2)%:pos; apply supXeX; rewrite /ball /= opprB addrC subrK.