From bab1cb082460ac483cf2c1a9ed55bdf46654241f Mon Sep 17 00:00:00 2001 From: zstone1 Date: Tue, 1 Oct 2024 23:39:11 -0400 Subject: [PATCH] separating filters (#1324) * separating_filter * fixes - duplicated Reserved Notations - duplicates in doc - doc formatting * updating changelog * review (wip) - remove unused notation - update changelog - get rid of duplicate identifiers (ending with an apostrophe) * fix changelog * rm toc from doc * mv lemmas down the hier --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 129 ++- _CoqProject | 1 + classical/Make | 1 + classical/all_classical.v | 1 + classical/boolp.v | 66 +- classical/filter.v | 1604 +++++++++++++++++++++++++++++++++ classical/mathcomp_extra.v | 23 + theories/ereal.v | 10 +- theories/normedtype.v | 22 +- theories/topology.v | 1742 +----------------------------------- 10 files changed, 1860 insertions(+), 1739 deletions(-) create mode 100644 classical/filter.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0a99e0909..4c785bf7a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -16,8 +16,12 @@ - in `realfun.v`: + lemmas `cvg_pinftyP`, `cvg_ninftyP` +- in `filter.v` (new file): + + lemma `in_nearW` + - in `topology.v`: - + lemmas `in_nearW`, `open_in_nearW` + + lemma `open_in_nearW` + - in `classical_sets.v`: + lemma `not_setD1` @@ -48,6 +52,123 @@ + lemma `lt0_funenegM` renamed to `le0_funenegM` and hypothesis weakened from strict to large inequality +- `theories/topology.v` split into `classical/filter.v` and `theories/topology.v` + +- moved from `topology.v` to `filter.v` + + definition `set_system`, coercion `set_system_to_set` + + mixin `isFiltered`, structures `Filtered`, `PointedFiltered` + (with resp. types `filteredType` and `pfilteredType`) + + mixin `selfFiltered` + + factory `hasNbhs` + + structures `Nbhs`, `PointedNbhs` + (with resp. types `nbhsType`, `pnbhsType`) + + definitions `filter_from`, `filter_prod` + + definitions `prop_near1`, `prop_near2` + + notations `{near _, _}`, `\forall _ \near _, _`, `near _, _`, + `{near _ & _, _}`, `\forall _ \near _ & _, _`, `\forall _ & _ \near _, _`, + `\near _ & _, _` + + lemmas `nearE`, `eq_near`, `nbhs_filterE` + + module `NbhsFilter` (with definition `nbhs_simpl`) + + definition `cvg_to`, notation ```_ `=>` _``` + + lemmas `cvg_refl`, `cvg_trans`, notation `_ --> _` + + definitions `type_of_filter`, `lim_in`, `lim` + + notations `[lim _ in _]`, `[cvg _ in _]`, `cvg` + + definition `eventually`, notation `\oo` + + lemmas `cvg_prod`, `cvg_in_ex`, `cvg_ex`, `cvg_inP`, `cvgP`, `cvg_in_toP`, + `cvg_toP`, `dvg_inP`, `dvgP`, `cvg_inNpoint`, `cvgNpoint` + + lemmas `nbhs_nearE`, `near_nbhs`, `near2_curry`, `near2_pair`, `filter_of_nearI` + + definition `near2E` + + module `NearNbhs` (with (re)definition `near_simpl` and ltac `near_simpl`) + + lemma `near_swap` + + classes `Filter` + + lemmas `filter_setT`, `filterP_strong` + + structure `filter_on` + + definition `filter_class` + + coercion `filter_filter'` + + structure `pfilter_on` + + definition `pfilter_class` + + canonical `pfilter_filter_on` + + coercion `pfilter_filter_on` + + definiton `PFilterType` + + instances `filter_on_Filter`, `pfilter_on_ProperFilter` + + lemma `nbhs_filter_onE`, `near_filter_onE` + + definition and canonical `trivial_filter_on` + + lemmas `filter_nbhsT`, `nearT`, `filter_not_empty_ex` + + lemma `filter_ex_subproof`, definition `filter_ex` + + lemma `filter_getP` + + record `in_filter` + + module type `in_filter`, module `PropInFilter`, notation `prop_of`, definition `prop_ofE`, + notation `_ \is_near _`, definition `is_nearE` + + lemma `prop_ofP` + + definition `in_filterT` + + canonical `in_filterI` + + lemma `filter_near_of` + + fact `near_key` + + lemmas `mark_near`, `near_acc`, `near_skip_subproof` + + tactic notations `near=>`, `near:`, `near do _` + + ltacs `just_discharge_near`, `near_skip`, `under_near`, `end_near`, `done` + + lemmas `have_near`, `near`, `nearW`, `filterE`, `filter_app`, `filter_app2`, + `filter_app3`, `filterS2`, `filterS3`, `filter_const`, `in_filter_from`, + `near_andP`, `nearP_dep`, `filter2P`, `filter_ex2`, `filter_fromP`, `filter_fromTP`, + `filter_from_filter`, `filter_fromT_filter`, `filter_from_proper`, `filter_bigI`, + `filter_forall`, `filter_imply` + + definition `fmap` + + lemma `fmapE` + + notations `_ @[_ --> _]`, `_ @[_ \oo]`, `_ @ _`, `limn`, `cvgn` + + instances `fmap_filter`, `fmap_proper_filter` + + definition `fmapi`, notations `_ `@[_ --> _]`, `_ `@ _` + + lemma `fmapiE` + + instances `fmapi_filter`. `fmapi_proper_filter` + + lemmas `cvg_id`, `fmap_comp`, `appfilter`, `cvg_app`, `cvgi_app`, `cvg_comp`, + `cvgi_comp`, `near_eq_cvg`, `eq_cvg`, `eq_is_cvg_in`, `eq_is_cvg`, `neari_eq_loc`, + `cvg_near_const` + + definition `continuous_at`, notation `continuous` + + lemma `near_fun` + + definition `globally`, lemma `globally0`, instances `globally_filter`, `globally_properfilter` + + definition `frechet_filter`, instances `frechet_properfilter`, `frechet_properfilter_nat` + + definition `at_point`, instance `at_point_filter` + + instances `filter_prod_filter`, `filter_prod_proper`, canonical `prod_filter_on` + + lemmas `filter_prod1`, `filter_prod2` + + definition `in_filter_prod` + + lemmas `near_pair`, `cvg_cst`, `cvg_snd`, `near_map`, `near_map2`, `near_mapi`, + `filter_pair_set`, `filter_pair_near_of` + + module export `NearMap` + + lemmas `filterN`, `cvg_pair`, `cvg_comp2` + + definition `cvg_to_comp_2` + + definition `within`, lemmas `near_withinE`, `withinT`, `near_withinT`, `cvg_within`, + `withinET`, instance `within_filter`, canonical `within_filter_on`, + lemma `filter_bigI_within` + + definition `subset_filter`, instance `subset_filter_filter`, lemma `subset_filter_proper` + + definition `powerset_filter_from`, instance `powerset_filter_from_filter` + + lemmas `near_small_set`, `small_set_sub`, `near_powerset_filter_fromP`, + `powerset_filter_fromP`, `near_powerset_map`, `near_powerset_map_monoE` + + definitions `principal_filter`, `principal_filter_type` + + lemmas `principal_filterP`, `principal_filter_proper` + + class `UltraFilter`, lemma `ultraFilterLemma` + + lemmas `filter_image`, `proper_image`, `principal_filter_ultra`, `in_ultra_setVsetC`, + `ultra_image` + + instance `smallest_filter_filter` + + fixpoint `filterI_iter` + + lemmas `filterI_iter_sub`, `filterI_iterE` + + definition `finI_from` + + lemmas `finI_from_cover`, `finI_from1`, `finI_from_countable`, `finI_fromI`, + `filterI_iter_finI`, `filterI_iter_finI` + + definition `finI` + + lemmas `finI_filter`, `filter_finI`, `meets_globallyl`, `meets_globallyr`, + `meetsxx`, `proper_meetsxx` + +- changed when moved from `topology.v` to `filter.v` + + `Build_ProperFilter` -> `Build_ProperFilter_ex` + + `ProperFilter'` -> `ProperFilter` + + remove notation `ProperFilter` + +- moved from `topology.v` to `mathcomp_extra.v`: + + lemma `and_prop_in` + + lemmas `mem_inc_segment`, `mem_inc_segment` + +- moved from `topology.v` to `boolp.v`: + + lemmas `bigmax_geP`, `bigmax_gtP`, `bigmin_leP`, `bigmin_ltP` + ### Renamed ### Generalized @@ -64,6 +185,12 @@ ### Removed +- in `topology.v`: + + notation `[filteredType _ of _]` + + definition `fmap_proper_filter'` + + definition `filter_map_proper_filter'` + + definition `filter_prod_proper'` + ### Infrastructure ### Misc diff --git a/_CoqProject b/_CoqProject index a9546dd37..3ef7b7c49 100644 --- a/_CoqProject +++ b/_CoqProject @@ -19,6 +19,7 @@ classical/cardinality.v classical/fsbigop.v classical/set_interval.v classical/classical_orders.v +classical/filter.v theories/all_analysis.v theories/constructive_ereal.v theories/ereal.v diff --git a/classical/Make b/classical/Make index 0883e93c1..45c406b11 100644 --- a/classical/Make +++ b/classical/Make @@ -17,4 +17,5 @@ cardinality.v fsbigop.v set_interval.v classical_orders.v +filter.v all_classical.v diff --git a/classical/all_classical.v b/classical/all_classical.v index d42c70908..b70e54f61 100644 --- a/classical/all_classical.v +++ b/classical/all_classical.v @@ -7,3 +7,4 @@ From mathcomp Require Export cardinality. From mathcomp Require Export fsbigop. From mathcomp Require Export set_interval. From mathcomp Require Export classical_orders. +From mathcomp Require Export filter. diff --git a/classical/boolp.v b/classical/boolp.v index feb9aeefb..ab36ee72c 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -51,9 +51,16 @@ From mathcomp Require Import mathcomp_extra. (* See also the lemmas Peq and eqPchoice. *) (* ``` *) (* *) -(* Functions into a porderType (resp. latticeType) are equipped with *) -(* a porderType (resp. latticeType), (f <= g)%O when f x <= g x for all x, *) -(* see lemma lefP. *) +(* Functions onto a porderType (resp. latticeType) are equipped with *) +(* a porderType (resp. latticeType), so that the generic notation (_ <= _)%O *) +(* (resp. `&`, `|`) from `order.v` can be used. *) +(* ``` *) +(* FunOrder.lef f g == pointwise large inequality between two functions *) +(* FunOrder.ltf f g == pointwise strict inequality between two functions *) +(* FunLattice.meetf f g == pointwise meet between two functions *) +(* FunLattice.joinf f g == pointwise join between two functions *) +(* ``` *) +(* *) (******************************************************************************) Set Implicit Arguments. @@ -784,6 +791,57 @@ apply: (iffP idP)=> [/asboolPn NP x|NP]. by apply/asboolP=> -[x Px Qx]; have /not_andP := NP x; exact. Qed. +Section bigmaxmin. +Local Notation max := Order.max. +Local Notation min := Order.min. +Local Open Scope order_scope. +Variables (d : Order.disp_t) (T : orderType d). +Variables (x : T) (I : finType) (P : pred I) (m : T) (F : I -> T). + +Import Order.TTheory. + +Lemma bigmax_geP : reflect (m <= x \/ exists2 i, P i & m <= F i) + (m <= \big[max/x]_(i | P i) F i). +Proof. +apply: (iffP idP) => [|[mx|[i Pi mFi]]]. +- rewrite leNgt => /bigmax_ltP /not_andP[/negP|]; first by rewrite -leNgt; left. + by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -leNgt; right; exists i. +- by rewrite bigmax_idl le_max mx. +- by rewrite (bigmaxD1 i)// le_max mFi. +Qed. + +Lemma bigmax_gtP : reflect (m < x \/ exists2 i, P i & m < F i) + (m < \big[max/x]_(i | P i) F i). +Proof. +apply: (iffP idP) => [|[mx|[i Pi mFi]]]. +- rewrite ltNge => /bigmax_leP /not_andP[/negP|]; first by rewrite -ltNge; left. + by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -ltNge; right; exists i. +- by rewrite bigmax_idl lt_max mx. +- by rewrite (bigmaxD1 i)// lt_max mFi. +Qed. + +Lemma bigmin_leP : reflect (x <= m \/ exists2 i, P i & F i <= m) + (\big[min/x]_(i | P i) F i <= m). +Proof. +apply: (iffP idP) => [|[xm|[i Pi Fim]]]. +- rewrite leNgt => /bigmin_gtP /not_andP[/negP|]; first by rewrite -leNgt; left. + by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -leNgt; right; exists i. +- by rewrite bigmin_idl ge_min xm. +- by rewrite (bigminD1 i)// ge_min Fim. +Qed. + +Lemma bigmin_ltP : reflect (x < m \/ exists2 i, P i & F i < m) + (\big[min/x]_(i | P i) F i < m). +Proof. +apply: (iffP idP) => [|[xm|[i Pi Fim]]]. +- rewrite ltNge => /bigmin_geP /not_andP[/negP|]; first by rewrite -ltNge; left. + by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -ltNge; right; exists i. +- by rewrite bigmin_idl gt_min xm. +- by rewrite (bigminD1 _ _ _ Pi) gt_min Fim. +Qed. + +End bigmaxmin. + Module FunOrder. Section FunOrder. Import Order.TTheory. @@ -875,7 +933,7 @@ Export FunOrder.Exports. Lemma lefP (aT : Type) d (T : porderType d) (f g : aT -> T) : reflect (forall x, (f x <= g x)%O) (f <= g)%O. -Proof. by apply: (iffP idP) => [fg|fg]; [exact/asboolP | apply/asboolP]. Qed. +Proof. by apply: (iffP idP) => [fg|fg]; [exact/asboolP | exact/asboolP]. Qed. Lemma meetfE (aT : Type) d (T : latticeType d) (f g : aT -> T) x : ((f `&` g) x = f x `&` g x)%O. diff --git a/classical/filter.v b/classical/filter.v new file mode 100644 index 000000000..b69519887 --- /dev/null +++ b/classical/filter.v @@ -0,0 +1,1604 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. +From mathcomp Require Import archimedean. +From mathcomp Require Import boolp classical_sets functions wochoice. +From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval. + +(**md**************************************************************************) +(* # Filters *) +(* *) +(* The theory of (powerset) filters and tools for manipulating them. *) +(* This file introduces convergence for filters. It also provides the *) +(* interface of filtered types for associating a "canonical filter" to each *) +(* element. And lastly it provides typeclass instances for verifying when *) +(* a (set_system T) is really a filter in T, as a Filter or Properfilter. *) +(* *) +(* ## Structure of filter *) +(* ``` *) +(* filteredType U == interface type for types whose *) +(* elements represent sets of sets on U *) +(* These sets are intended to be filters *) +(* on U but this is not enforced yet. *) +(* The HB class is called Filtered. *) +(* It extends Pointed. *) +(* nbhs p == set of sets associated to p (in a *) +(* filtered type) *) +(* pfilteredType U == a pointed and filtered type *) +(* hasNbhs == factory for filteredType *) +(* ``` *) +(* *) +(* We endow several standard types with the structure of filter, e.g.: *) +(* - products `(X1 * X2)%type` *) +(* - matrices `'M[X]_(m, n)` *) +(* - natural numbers `nat` *) +(* *) +(* ## Theory of filters *) +(* ``` *) +(* filter_from D B == set of the supersets of the elements *) +(* of the family of sets B whose indices *) +(* are in the domain D *) +(* This is a filter if (B_i)_(i in D) *) +(* forms a filter base. *) +(* filter_prod F G == product of the filters F and G *) +(* F `=>` G <-> G is included in F *) +(* F and G are sets of sets. *) +(* F --> G <-> the canonical filter associated to G *) +(* is included in the canonical filter *) +(* associated to F *) +(* lim F == limit of the canonical filter *) +(* associated with F if there is such a *) +(* limit, i.e., an element l such that *) +(* the canonical filter associated to l *) +(* is a subset of F *) +(* [lim F in T] == limit of the canonical filter *) +(* associated to F in T where T has type *) +(* filteredType U *) +(* [cvg F in T] <-> the canonical filter associated to F *) +(* converges in T *) +(* cvg F <-> same as [cvg F in T] where T is *) +(* inferred from the type of the *) +(* canonical filter associated to F *) +(* Filter F == type class proving that the set of *) +(* sets F is a filter *) +(* ProperFilter F == type class proving that the set of *) +(* sets F is a proper filter *) +(* UltraFilter F == type class proving that the set of *) +(* sets F is an ultrafilter *) +(* filter_on T == interface type for sets of sets on T *) +(* that are filters *) +(* FilterType F FF == packs the set of sets F with the proof *) +(* FF of Filter F to build a filter_on T *) +(* structure *) +(* pfilter_on T == interface type for sets of sets on T *) +(* that are proper filters *) +(* PFilterPack F FF == packs the set of sets F with the proof *) +(* FF of ProperFilter F to build a *) +(* pfilter_on T structure *) +(* fmap f F == image of the filter F by the function *) +(* f *) +(* E @[x --> F] == image of the canonical filter *) +(* associated to F by the function *) +(* (fun x => E) *) +(* f @ F == image of the canonical filter *) +(* associated to F by the function f *) +(* fmapi f F == image of the filter F by the relation *) +(* f *) +(* E `@[x --> F] == image of the canonical filter *) +(* associated to F by the relation *) +(* (fun x => E) *) +(* f `@ F == image of the canonical filter *) +(* associated to F by the relation f *) +(* globally A == filter of the sets containing A *) +(* @frechet_filter T := [set S : set T | finite_set (~` S)] *) +(* a.k.a. cofinite filter *) +(* at_point a == filter of the sets containing a *) +(* within D F == restriction of the filter F to the *) +(* domain D *) +(* principal_filter x == filter containing every superset of x *) +(* principal_filter_type == alias for choice types with principal *) +(* filters *) +(* subset_filter F D == similar to within D F, but with *) +(* dependent types *) +(* powerset_filter_from F == the filter of downward closed subsets *) +(* of F. *) +(* Enables use of near notation to pick *) +(* suitably small members of F *) +(* in_filter F == interface type for the sets that *) +(* belong to the set of sets F *) +(* InFilter FP == packs a set P with a proof of F P to *) +(* build a in_filter F structure *) +(* ``` *) +(* *) +(* ## Near notations and tactics *) +(* The purpose of the near notations and tactics is to make the manipulation *) +(* of filters easier. Instead of proving $F\; G$, one can prove $G\; x$ for *) +(* $x$ "near F", i.e., for x such that H x for H arbitrarily precise as long *) +(* as $F\; H$. The near tactics allow for a delayed introduction of $H$: *) +(* $H$ is introduced as an existential variable and progressively *) +(* instantiated during the proof process. *) +(* *) +(* ### Notations *) +(* ``` *) +(* {near F, P} == the property P holds near the *) +(* canonical filter associated to F *) +(* P must have the form forall x, Q x. *) +(* Equivalent to F Q. *) +(* \forall x \near F, P x <-> F (fun x => P x). *) +(* \near x, P x := \forall y \near x, P y. *) +(* {near F & G, P} == same as {near H, P}, where H is the *) +(* product of the filters F and G *) +(* \forall x \near F & y \near G, P x y := {near F & G, forall x y, P x y} *) +(* \forall x & y \near F, P x y == same as before, with G = F *) +(* \near x & y, P x y := \forall z \near x & t \near y, P x y *) +(* x \is_near F == x belongs to a set P : in_filter F *) +(* ``` *) +(* *) +(* ### Tactics *) +(* - near=> x introduces x: *) +(* On the goal \forall x \near F, G x, introduces the variable x and an *) +(* "existential", and an unaccessible hypothesis ?H x and asks the user to *) +(* prove (G x) in this context. *) +(* Under the hood, it delays the proof of F ?H and waits for near: x. *) +(* Also exists under the form near=> x y. *) +(* - near: x discharges x: *) +(* On the goal H_i x, and where x \is_near F, it asks the user to prove *) +(* that (\forall x \near F, H_i x), provided that H_i x does not depend on *) +(* variables introduced after x. *) +(* Under the hood, it refines by intersection the existential variable ?H *) +(* attached to x, computes the intersection with F, and asks the user to *) +(* prove F H_i, right now. *) +(* - end_near should be used to close remaining existentials trivially. *) +(* - near F => x poses a variable near F, where F is a proper filter *) +(* It adds to the context a variable x that \is_near F, i.e., one may *) +(* assume H x for any H in F. This new variable x can be dealt with using *) +(* near: x, as for variables introduced by near=>. *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(* Making sure that [Program] does not automatically introduce *) +Obligation Tactic := idtac. + +Import Order.TTheory GRing.Theory Num.Theory. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Reserved Notation "{ 'near' x , P }" (at level 0, format "{ 'near' x , P }"). +Reserved Notation "'\forall' x '\near' x_0 , P" + (at level 200, x name, P at level 200, + format "'\forall' x '\near' x_0 , P"). +Reserved Notation "'\near' x , P" + (at level 200, x at level 99, P at level 200, + format "'\near' x , P", only parsing). +Reserved Notation "{ 'near' x & y , P }" + (at level 0, format "{ 'near' x & y , P }"). +Reserved Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P" + (at level 200, x name, y name, P at level 200, + format "'\forall' x '\near' x_0 & y '\near' y_0 , P"). +Reserved Notation "'\forall' x & y '\near' z , P" + (at level 200, x name, y name, P at level 200, + format "'\forall' x & y '\near' z , P"). +Reserved Notation "'\near' x & y , P" + (at level 200, x, y at level 99, P at level 200, + format "'\near' x & y , P", only parsing). +(*Reserved Notation "[ 'filter' 'of' x ]" (format "[ 'filter' 'of' x ]").*) +Reserved Notation "F `=>` G" (at level 70, format "F `=>` G"). +Reserved Notation "F --> G" (at level 70, format "F --> G"). +Reserved Notation "[ 'lim' F 'in' T ]" (format "[ 'lim' F 'in' T ]"). +Reserved Notation "[ 'cvg' F 'in' T ]" (format "[ 'cvg' F 'in' T ]"). +Reserved Notation "x \is_near F" (at level 10, format "x \is_near F"). +Reserved Notation "E @[ x --> F ]" + (at level 60, x name, format "E @[ x --> F ]"). +Reserved Notation "E @[ x \oo ]" + (at level 60, x name, format "E @[ x \oo ]"). +Reserved Notation "f @ F" (at level 60, format "f @ F"). +Reserved Notation "E `@[ x --> F ]" + (at level 60, x name, format "E `@[ x --> F ]"). +Reserved Notation "f `@ F" (at level 60, format "f `@ F"). + +Definition set_system U := set (set U). +Identity Coercion set_system_to_set : set_system >-> set. + +HB.mixin Record isFiltered U T := { + nbhs : T -> set_system U +}. + +#[short(type="filteredType")] +HB.structure Definition Filtered (U : Type) := {T of Choice T & isFiltered U T}. + +#[short(type="pfilteredType")] +HB.structure Definition PointedFiltered (U : Type) := {T of Pointed T & isFiltered U T}. +Arguments nbhs {_ _} _ _ : simpl never. + +HB.instance Definition _ T := Equality.on (set_system T). +HB.instance Definition _ T := Choice.on (set_system T). +HB.instance Definition _ T := Pointed.on (set_system T). +HB.instance Definition _ T := isFiltered.Build T (set_system T) id. + +Arguments nbhs {_ _} _ _ : simpl never. + +HB.mixin Record selfFiltered T := {}. + +HB.factory Record hasNbhs T := { nbhs : T -> set_system T }. +HB.builders Context T of hasNbhs T. + HB.instance Definition _ := isFiltered.Build T T nbhs. + HB.instance Definition _ := selfFiltered.Build T. +HB.end. + +#[short(type="nbhsType")] +HB.structure Definition Nbhs := {T of Choice T & hasNbhs T}. + +#[short(type="pnbhsType")] +HB.structure Definition PointedNbhs := {T of Pointed T & hasNbhs T}. + +Definition filter_from {I T : Type} (D : set I) (B : I -> set T) : + set_system T := [set P | exists2 i, D i & B i `<=` P]. + +(* the canonical filter on matrices on X is the product of the canonical filter + on X *) +HB.instance Definition _ m n X (Z : filteredType X) := + isFiltered.Build 'M[X]_(m, n) 'M[Z]_(m, n) (fun mx => filter_from + [set P | forall i j, nbhs (mx i j) (P i j)] + (fun P => [set my : 'M[X]_(m, n) | forall i j, P i j (my i j)])). + +HB.instance Definition _ m n (X : nbhsType) := selfFiltered.Build 'M[X]_(m, n). + +Definition filter_prod {T U : Type} + (F : set_system T) (G : set_system U) : set_system (T * U) := + filter_from (fun P => F P.1 /\ G P.2) (fun P => P.1 `*` P.2). + +Section Near. + +Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). +Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). +Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). +Local Notation ph := (phantom _). + +Definition prop_near1 {X} {fX : filteredType X} (x : fX) + P (phP : ph {all1 P}) := nbhs x P. + +Definition prop_near2 {X X'} {fX : filteredType X} {fX' : filteredType X'} + (x : fX) (x' : fX') := fun P of ph {all2 P} => + filter_prod (nbhs x) (nbhs x') (fun x => P x.1 x.2). + +End Near. + +Notation "{ 'near' x , P }" := (@prop_near1 _ _ x _ (inPhantom P)) : type_scope. +Notation "'\forall' x '\near' x_0 , P" := {near x_0, forall x, P} : type_scope. +Notation "'\near' x , P" := (\forall x \near x, P) : type_scope. +Notation "{ 'near' x & y , P }" := + (@prop_near2 _ _ _ _ x y _ (inPhantom P)) : type_scope. +Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P" := + {near x_0 & y_0, forall x y, P} : type_scope. +Notation "'\forall' x & y '\near' z , P" := + {near z & z, forall x y, P} : type_scope. +Notation "'\near' x & y , P" := (\forall x \near x & y \near y, P) : type_scope. +Arguments prop_near1 : simpl never. +Arguments prop_near2 : simpl never. + +Lemma nearE {T} {F : set_system T} (P : set T) : + (\forall x \near F, P x) = F P. +Proof. by []. Qed. + +Lemma eq_near {T} {F : set_system T} (P Q : set T) : + (forall x, P x <-> Q x) -> + (\forall x \near F, P x) = (\forall x \near F, Q x). +Proof. by move=> /predeqP ->. Qed. + +Lemma nbhs_filterE {T : Type} (F : set_system T) : nbhs F = F. +Proof. by []. Qed. + +Module Export NbhsFilter. +Definition nbhs_simpl := (@nbhs_filterE). +End NbhsFilter. + +Definition cvg_to {T : Type} (F G : set_system T) := G `<=` F. +Notation "F `=>` G" := (cvg_to F G) : classical_set_scope. + +Lemma cvg_refl T (F : set_system T) : F `=>` F. Proof. exact. Qed. +Arguments cvg_refl {T F}. +#[global] Hint Resolve cvg_refl : core. + +Lemma cvg_trans T (G F H : set_system T) : + (F `=>` G) -> (G `=>` H) -> (F `=>` H). +Proof. by move=> FG GH P /GH /FG. Qed. + +Notation "F --> G" := (cvg_to (nbhs F) (nbhs G)) : classical_set_scope. +Definition type_of_filter {T} (F : set_system T) := T. + +Definition lim_in {U : Type} (T : pfilteredType U) := + fun F : set_system U => get (fun l : T => F --> l). +Notation "[ 'lim' F 'in' T ]" := (@lim_in _ T (nbhs F)) : classical_set_scope. +Definition lim {T : pnbhsType} (F : set_system T) := [lim F in T]. +Notation "[ 'cvg' F 'in' T ]" := (F --> [lim F in T]) : classical_set_scope. +Notation cvg F := (F --> lim F). + +(* :TODO: ultimately nat could be replaced by any lattice *) +Definition eventually := filter_from setT (fun N => [set n | (N <= n)%N]). +Notation "'\oo'" := eventually : classical_set_scope. + +Section FilteredTheory. + +HB.instance Definition _ X1 X2 (Z1 : filteredType X1) (Z2 : filteredType X2) := + isFiltered.Build (X1 * X2)%type (Z1 * Z2)%type + (fun x => filter_prod (nbhs x.1) (nbhs x.2)). + +HB.instance Definition _ (X1 X2 : nbhsType) := + selfFiltered.Build (X1 * X2)%type. + +Lemma cvg_prod T {U U' V V' : filteredType T} (x : U) (l : U') (y : V) (k : V') : + x --> l -> y --> k -> (x, y) --> (l, k). +Proof. +move=> xl yk X [[X1 X2] /= [HX1 HX2] H]; exists (X1, X2) => //=. +split; [exact: xl | exact: yk]. +Qed. + +Lemma cvg_in_ex {U : Type} (T : pfilteredType U) (F : set_system U) : + [cvg F in T] <-> (exists l : T, F --> l). +Proof. by split=> [cvg|/getPex//]; exists [lim F in T]. Qed. + +Lemma cvg_ex (T : pnbhsType) (F : set_system T) : + cvg F <-> (exists l : T, F --> l). +Proof. exact: cvg_in_ex. Qed. + +Lemma cvg_inP {U : Type} (T : pfilteredType U) (F : set_system U) (l : T) : + F --> l -> [cvg F in T]. +Proof. by move=> Fl; apply/cvg_in_ex; exists l. Qed. + +Lemma cvgP (T : pnbhsType) (F : set_system T) (l : T) : F --> l -> cvg F. +Proof. exact: cvg_inP. Qed. + +Lemma cvg_in_toP {U : Type} (T : pfilteredType U) (F : set_system U) (l : T) : + [cvg F in T] -> [lim F in T] = l -> F --> l. +Proof. by move=> /[swap]->. Qed. + +Lemma cvg_toP (T : pnbhsType) (F : set_system T) (l : T) : + cvg F -> lim F = l -> F --> l. +Proof. exact: cvg_in_toP. Qed. + +Lemma dvg_inP {U : Type} (T : pfilteredType U) (F : set_system U) : + ~ [cvg F in T] -> [lim F in T] = point. +Proof. by rewrite /lim_in /=; case xgetP. Qed. + +Lemma dvgP (T : pnbhsType) (F : set_system T) : ~ cvg F -> lim F = point. +Proof. exact: dvg_inP. Qed. + +Lemma cvg_inNpoint {U} (T : pfilteredType U) (F : set_system U) : + [lim F in T] != point -> [cvg F in T]. +Proof. by apply: contra_neqP; apply: dvg_inP. Qed. + +Lemma cvgNpoint (T : pnbhsType) (F : set_system T) : lim F != point -> cvg F. +Proof. exact: cvg_inNpoint. Qed. + +End FilteredTheory. +Arguments cvg_inP {U T F} l. +Arguments dvg_inP {U} T {F}. +Arguments cvgP {T F} l. +Arguments dvgP {T F}. + +Lemma nbhs_nearE {U} {T : filteredType U} (x : T) (P : set U) : + nbhs x P = \near x, P x. +Proof. by []. Qed. + +Lemma near_nbhs {U} {T : filteredType U} (x : T) (P : set U) : + (\forall x \near nbhs x, P x) = \near x, P x. +Proof. by []. Qed. + +Lemma near2_curry {U V} (F : set_system U) (G : set_system V) (P : U -> set V) : + {near F & G, forall x y, P x y} = {near (F, G), forall x, P x.1 x.2}. +Proof. by []. Qed. + +Lemma near2_pair {U V} (F : set_system U) (G : set_system V) (P : set (U * V)) : + {near F & G, forall x y, P (x, y)} = {near (F, G), forall x, P x}. +Proof. by symmetry; congr (nbhs _); rewrite predeqE => -[]. Qed. + +Definition near2E := (@near2_curry, @near2_pair). + +Lemma filter_of_nearI (X : Type) (fX : filteredType X) + (x : fX) : forall P, + nbhs x P = @prop_near1 X fX x P (inPhantom (forall x, P x)). +Proof. by []. Qed. + +Module Export NearNbhs. +Definition near_simpl := (@near_nbhs, @nbhs_nearE, filter_of_nearI). +Ltac near_simpl := rewrite ?near_simpl. +End NearNbhs. + +Lemma near_swap {U V} (F : set_system U) (G : set_system V) (P : U -> set V) : + (\forall x \near F & y \near G, P x y) = (\forall y \near G & x \near F, P x y). +Proof. +rewrite propeqE; split => -[[/=A B] [FA FB] ABP]; +by exists (B, A) => // -[x y] [/=Bx Ay]; apply: (ABP (y, x)). +Qed. + +(** Filters *) + +Class Filter {T : Type} (F : set_system T) := { + filterT : F setT ; + filterI : forall P Q : set T, F P -> F Q -> F (P `&` Q) ; + filterS : forall P Q : set T, P `<=` Q -> F P -> F Q +}. +Global Hint Mode Filter - ! : typeclass_instances. + +Class ProperFilter {T : Type} (F : set_system T) := { + filter_not_empty : not (F (fun _ => False)) ; + filter_filter : Filter F +}. +(* TODO: Reuse :> above and remove the following line and the coercion below + after 8.21 is the minimum required version for Coq *) +Global Existing Instance filter_filter. +Global Hint Mode ProperFilter - ! : typeclass_instances. +Arguments filter_not_empty {T} F {_}. + +Lemma filter_setT (T' : Type) : Filter [set: set T']. +Proof. by constructor. Qed. + +Lemma filterP_strong T (F : set_system T) {FF : Filter F} (P : set T) : + (exists Q : set T, exists FQ : F Q, forall x : T, Q x -> P x) <-> F P. +Proof. +split; last by exists P. +by move=> [Q [FQ QP]]; apply: (filterS QP). +Qed. + +Structure filter_on T := FilterType { + filter :> set_system T; + _ : Filter filter +}. +Definition filter_class T (F : filter_on T) : Filter F := + let: FilterType _ class := F in class. +Arguments FilterType {T} _ _. +#[global] Existing Instance filter_class. +(* Typeclasses Opaque filter. *) +Coercion filter_filter : ProperFilter >-> Filter. + +Structure pfilter_on T := PFilterPack { + pfilter :> (T -> Prop) -> Prop; + _ : ProperFilter pfilter +}. +Definition pfilter_class T (F : pfilter_on T) : ProperFilter F := + let: PFilterPack _ class := F in class. +Arguments PFilterPack {T} _ _. +#[global] Existing Instance pfilter_class. +(* Typeclasses Opaque pfilter. *) +Canonical pfilter_filter_on T (F : pfilter_on T) := + FilterType F (pfilter_class F). +Coercion pfilter_filter_on : pfilter_on >-> filter_on. +Definition PFilterType {T} (F : (T -> Prop) -> Prop) + {fF : Filter F} (fN0 : not (F set0)) := + PFilterPack F (Build_ProperFilter fN0 fF). +Arguments PFilterType {T} F {fF} fN0. + +HB.instance Definition _ T := gen_eqMixin (filter_on T). +HB.instance Definition _ T := gen_choiceMixin (filter_on T). +HB.instance Definition _ T := isPointed.Build (filter_on T) + (FilterType _ (filter_setT T)). +HB.instance Definition _ T := isFiltered.Build T (filter_on T) (@filter T). + +Global Instance filter_on_Filter T (F : filter_on T) : Filter F. +Proof. by case: F. Qed. +Global Instance pfilter_on_ProperFilter T (F : pfilter_on T) : ProperFilter F. +Proof. by case: F. Qed. + +Lemma nbhs_filter_onE T (F : filter_on T) : nbhs F = nbhs (filter F). +Proof. by []. Qed. +Definition nbhs_simpl := (@nbhs_simpl, @nbhs_filter_onE). + +Lemma near_filter_onE T (F : filter_on T) (P : set T) : + (\forall x \near F, P x) = \forall x \near filter F, P x. +Proof. by []. Qed. +Definition near_simpl := (@near_simpl, @near_filter_onE). + +Program Definition trivial_filter_on T := FilterType [set setT : set T] _. +Next Obligation. +split=> // [_ _ -> ->|Q R sQR QT]; first by rewrite setIT. +by move; rewrite eqEsubset; split => // ? _; apply/sQR; rewrite QT. +Qed. +Canonical trivial_filter_on. + +Lemma filter_nbhsT {T : Type} (F : set_system T) : + Filter F -> nbhs F setT. +Proof. by move=> FF; apply: filterT. Qed. +#[global] Hint Resolve filter_nbhsT : core. + +Lemma nearT {T : Type} (F : set_system T) : Filter F -> \near F, True. +Proof. by move=> FF; apply: filterT. Qed. +#[global] Hint Resolve nearT : core. + +Lemma filter_not_empty_ex {T : Type} (F : set_system T) : + (forall P, F P -> exists x, P x) -> ~ F set0. +Proof. by move=> /(_ set0) ex /ex []. Qed. + +Definition Build_ProperFilter_ex {T : Type} (F : set_system T) + (filter_ex : forall P, F P -> exists x, P x) + (FF : Filter F) := + Build_ProperFilter (filter_not_empty_ex filter_ex) FF. + +Lemma filter_ex_subproof {T : Type} (F : set_system T) : + ~ F set0 -> (forall P, F P -> exists x, P x). +Proof. +move=> NFset0 P FP; apply: contra_notP NFset0 => nex; suff <- : P = set0 by []. +by rewrite funeqE => x; rewrite propeqE; split=> // Px; apply: nex; exists x. +Qed. + +Definition filter_ex {T : Type} (F : set_system T) {FF : ProperFilter F} := + filter_ex_subproof (filter_not_empty F). +Arguments filter_ex {T F FF _}. + +Lemma filter_getP {T : pointedType} (F : set_system T) {FF : ProperFilter F} + (P : set T) : F P -> P (get P). +Proof. by move=> /filter_ex /getPex. Qed. + +(* Near Tactic *) + +Record in_filter T (F : set_system T) := InFilter { + prop_in_filter_proj : T -> Prop; + prop_in_filterP_proj : F prop_in_filter_proj +}. +(* add ball x e as a canonical instance of nbhs x *) + +Module Type PropInFilterSig. +Axiom t : forall (T : Type) (F : set_system T), in_filter F -> T -> Prop. +Axiom tE : t = prop_in_filter_proj. +End PropInFilterSig. +Module PropInFilter : PropInFilterSig. +Definition t := prop_in_filter_proj. +Lemma tE : t = prop_in_filter_proj. Proof. by []. Qed. +End PropInFilter. +(* Coercion PropInFilter.t : in_filter >-> Funclass. *) +Notation prop_of := PropInFilter.t. +Definition prop_ofE := PropInFilter.tE. +Notation "x \is_near F" := (@PropInFilter.t _ F _ x). +Definition is_nearE := prop_ofE. + +Lemma prop_ofP T F (iF : @in_filter T F) : F (prop_of iF). +Proof. by rewrite prop_ofE; apply: prop_in_filterP_proj. Qed. + +Definition in_filterT T F (FF : Filter F) : @in_filter T F := + InFilter (filterT). +Canonical in_filterI T F (FF : Filter F) (P Q : @in_filter T F) := + InFilter (filterI (prop_in_filterP_proj P) (prop_in_filterP_proj Q)). + +Lemma filter_near_of T F (P : @in_filter T F) (Q : set T) : Filter F -> + (forall x, prop_of P x -> Q x) -> F Q. +Proof. +by move: P => [P FP] FF /=; rewrite prop_ofE /= => /filterS; apply. +Qed. + +Fact near_key : unit. Proof. exact. Qed. + +Lemma mark_near (P : Prop) : locked_with near_key P -> P. +Proof. by rewrite unlock. Qed. + +Lemma near_acc T F (P : @in_filter T F) (Q : set T) (FF : Filter F) + (FQ : \forall x \near F, Q x) : + locked_with near_key (forall x, prop_of (in_filterI FF P (InFilter FQ)) x -> Q x). +Proof. by rewrite unlock => x /=; rewrite !prop_ofE /= => -[Px]. Qed. + +Lemma near_skip_subproof T F (P Q : @in_filter T F) (G : set T) (FF : Filter F) : + locked_with near_key (forall x, prop_of P x -> G x) -> + locked_with near_key (forall x, prop_of (in_filterI FF P Q) x -> G x). +Proof. +rewrite !unlock => FG x /=; rewrite !prop_ofE /= => -[Px Qx]. +by have /= := FG x; apply; rewrite prop_ofE. +Qed. + +Tactic Notation "near=>" ident(x) := apply: filter_near_of => x ?. + +Ltac just_discharge_near x := + tryif match goal with Hx : x \is_near _ |- _ => move: (x) (Hx); apply: mark_near end + then idtac else fail "the variable" x "is not a ""near"" variable". +Ltac near_skip := + match goal with |- locked_with near_key (forall _, @PropInFilter.t _ _ ?P _ -> _) => + tryif is_evar P then fail "nothing to skip" else apply: near_skip_subproof end. + +Tactic Notation "near:" ident(x) := + just_discharge_near x; + tryif do ![apply: near_acc; first shelve|near_skip] + then idtac + else fail "the goal depends on variables introduced after" x. + +Ltac under_near i tac := near=> i; tac; near: i. +Tactic Notation "near=>" ident(i) "do" tactic3(tac) := under_near i ltac:(tac). +Tactic Notation "near=>" ident(i) "do" "[" tactic4(tac) "]" := near=> i do tac. +Tactic Notation "near" "do" tactic3(tac) := + let i := fresh "i" in under_near i ltac:(tac). +Tactic Notation "near" "do" "[" tactic4(tac) "]" := near do tac. + +Ltac end_near := do ?exact: in_filterT. + +Ltac done := + trivial; hnf; intros; solve + [ do ![solve [trivial | apply: sym_equal; trivial] + | discriminate | contradiction | split] + | match goal with H : ~ _ |- _ => solve [case H; trivial] end + | match goal with |- ?x \is_near _ => near: x; apply: prop_ofP end ]. + +Lemma have_near (U : Type) (fT : filteredType U) (x : fT) (P : Prop) : + ProperFilter (nbhs x) -> (\forall x \near x, P) -> P. +Proof. by move=> FF nP; have [] := @filter_ex _ _ FF (fun=> P). Qed. +Arguments have_near {U fT} x. + +Tactic Notation "near" constr(F) "=>" ident(x) := + apply: (have_near F); near=> x. + +Lemma near T (F : set_system T) P (FP : F P) (x : T) + (Px : prop_of (InFilter FP) x) : P x. +Proof. by move: Px; rewrite prop_ofE. Qed. +Arguments near {T F P} FP x Px. + +Lemma nearW {T : Type} {F : set_system T} (P : T -> Prop) : + Filter F -> (forall x, P x) -> (\forall x \near F, P x). +Proof. by move=> FF FP; apply: filterS filterT. Qed. + +Lemma filterE {T : Type} {F : set_system T} : + Filter F -> forall P : set T, (forall x, P x) -> F P. +Proof. by move=> [FT _ +] P fP => /(_ setT); apply. Qed. + +Lemma filter_app (T : Type) (F : set_system T) : + Filter F -> forall P Q : set T, F (fun x => P x -> Q x) -> F P -> F Q. +Proof. by move=> FF P Q subPQ FP; near=> x do suff: P x. +Unshelve. all: by end_near. Qed. + +Lemma filter_app2 (T : Type) (F : set_system T) : + Filter F -> forall P Q R : set T, F (fun x => P x -> Q x -> R x) -> + F P -> F Q -> F R. +Proof. by move=> ???? PQR FP; apply: filter_app; apply: filter_app FP. Qed. + +Lemma filter_app3 (T : Type) (F : set_system T) : + Filter F -> forall P Q R S : set T, F (fun x => P x -> Q x -> R x -> S x) -> + F P -> F Q -> F R -> F S. +Proof. by move=> ????? PQR FP; apply: filter_app2; apply: filter_app FP. Qed. + +Lemma filterS2 (T : Type) (F : set_system T) : + Filter F -> forall P Q R : set T, (forall x, P x -> Q x -> R x) -> + F P -> F Q -> F R. +Proof. by move=> ? ? ? ? ?; apply: filter_app2; apply: filterE. Qed. + +Lemma filterS3 (T : Type) (F : set_system T) : + Filter F -> forall P Q R S : set T, (forall x, P x -> Q x -> R x -> S x) -> + F P -> F Q -> F R -> F S. +Proof. by move=> ? ? ? ? ? ?; apply: filter_app3; apply: filterE. Qed. + +Lemma filter_const {T : Type} {F} {FF: @ProperFilter T F} (P : Prop) : + F (fun=> P) -> P. +Proof. by move=> FP; case: (filter_ex FP). Qed. + +Lemma in_filter_from {I T : Type} (D : set I) (B : I -> set T) (i : I) : + D i -> filter_from D B (B i). +Proof. by exists i. Qed. + +Lemma in_nearW {T : Type} (F : set_system T) (P : T -> Prop) (S : set T) : + Filter F -> F S -> {in S, forall x, P x} -> \near F, P F. +Proof. +move=> FF FS SP; rewrite -nbhs_nearE. +by apply: (@filterS _ F _ S) => // x /mem_set /SP. +Qed. + +Lemma near_andP {T : Type} F (b1 b2 : T -> Prop) : Filter F -> + (\forall x \near F, b1 x /\ b2 x) <-> + (\forall x \near F, b1 x) /\ (\forall x \near F, b2 x). +Proof. +move=> FF; split=> [H|[H1 H2]]; first by split; apply: filterS H => ? []. +by apply: filterS2 H1 H2. +Qed. + +Lemma nearP_dep {T U} {F : set_system T} {G : set_system U} + {FF : Filter F} {FG : Filter G} (P : T -> U -> Prop) : + (\forall x \near F & y \near G, P x y) -> + \forall x \near F, \forall y \near G, P x y. +Proof. +move=> [[Q R] [/=FQ GR]] QRP. +by apply: filterS FQ => x Q1x; apply: filterS GR => y Q2y; apply: (QRP (_, _)). +Qed. + +Lemma filter2P T U (F : set_system T) (G : set_system U) + {FF : Filter F} {FG : Filter G} (P : set (T * U)) : + (exists2 Q : set T * set U, F Q.1 /\ G Q.2 + & forall (x : T) (y : U), Q.1 x -> Q.2 y -> P (x, y)) + <-> \forall x \near (F, G), P x. +Proof. +split=> [][[A B] /=[FA GB] ABP]; exists (A, B) => //=. + by move=> [a b] [/=Aa Bb]; apply: ABP. +by move=> a b Aa Bb; apply: (ABP (_, _)). +Qed. + +Lemma filter_ex2 {T U : Type} (F : set_system T) (G : set_system U) + {FF : ProperFilter F} {FG : ProperFilter G} (P : set T) (Q : set U) : + F P -> G Q -> exists x : T, exists2 y : U, P x & Q y. +Proof. by move=> /filter_ex [x Px] /filter_ex [y Qy]; exists x, y. Qed. +Arguments filter_ex2 {T U F G FF FG _ _}. + +Lemma filter_fromP {I T : Type} (D : set I) (B : I -> set T) (F : set_system T) : + Filter F -> F `=>` filter_from D B <-> forall i, D i -> F (B i). +Proof. +split; first by move=> FB i ?; apply/FB/in_filter_from. +by move=> FB P [i Di BjP]; apply: (filterS BjP); apply: FB. +Qed. + +Lemma filter_fromTP {I T : Type} (B : I -> set T) (F : set_system T) : + Filter F -> F `=>` filter_from setT B <-> forall i, F (B i). +Proof. by move=> FF; rewrite filter_fromP; split=> [P i|P i _]; apply: P. Qed. + +Lemma filter_from_filter {I T : Type} (D : set I) (B : I -> set T) : + (exists i : I, D i) -> + (forall i j, D i -> D j -> exists2 k, D k & B k `<=` B i `&` B j) -> + Filter (filter_from D B). +Proof. +move=> [i0 Di0] Binter; constructor; first by exists i0. + move=> P Q [i Di BiP] [j Dj BjQ]; have [k Dk BkPQ]:= Binter _ _ Di Dj. + by exists k => // x /BkPQ [/BiP ? /BjQ]. +by move=> P Q subPQ [i Di BiP]; exists i => //; apply: subset_trans subPQ. +Qed. + +Lemma filter_fromT_filter {I T : Type} (B : I -> set T) : + (exists _ : I, True) -> + (forall i j, exists k, B k `<=` B i `&` B j) -> + Filter (filter_from setT B). +Proof. +move=> [i0 _] BI; apply: filter_from_filter; first by exists i0. +by move=> i j _ _; have [k] := BI i j; exists k. +Qed. + +Lemma filter_from_proper {I T : Type} (D : set I) (B : I -> set T) : + Filter (filter_from D B) -> + (forall i, D i -> B i !=set0) -> + ProperFilter (filter_from D B). +Proof. +move=> FF BN0; apply: Build_ProperFilter_ex => P [i Di BiP]. +by have [x Bix] := BN0 _ Di; exists x; apply: BiP. +Qed. + +Lemma filter_bigI T (I : choiceType) (D : {fset I}) (f : I -> set T) + (F : set_system T) : + Filter F -> (forall i, i \in D -> F (f i)) -> + F (\bigcap_(i in [set` D]) f i). +Proof. +move=> FF FfD. +suff: F [set p | forall i, i \in enum_fset D -> f i p] by []. +have {FfD} : forall i, i \in enum_fset D -> F (f i) by move=> ? /FfD. +elim: (enum_fset D) => [|i s ihs] FfD; first exact: filterS filterT. +apply: (@filterS _ _ _ (f i `&` [set p | forall i, i \in s -> f i p])). + by move=> p [fip fsp] j; rewrite inE => /orP [/eqP->|] //; apply: fsp. +apply: filterI; first by apply: FfD; rewrite inE eq_refl. +by apply: ihs => j sj; apply: FfD; rewrite inE sj orbC. +Qed. + +Lemma filter_forall T (I : finType) (f : I -> set T) (F : set_system T) : + Filter F -> (forall i : I, \forall x \near F, f i x) -> + \forall x \near F, forall i, f i x. +Proof. +move=> FF fIF; apply: filterS (@filter_bigI T I [fset x in I]%fset f F FF _). + by move=> x fIx i; have := fIx i; rewrite /= inE/=; apply. +by move=> i; rewrite inE/= => _; apply: (fIF i). +Qed. + +Lemma filter_imply [T : Type] [P : Prop] [f : set T] [F : set_system T] : + Filter F -> (P -> \near F, f F) -> \near F, P -> f F. +Proof. +move=> ? PF; near do move=> /asboolP. +by case: asboolP=> [/PF|_]; by [apply: filterS|apply: nearW]. +Unshelve. all: by end_near. Qed. + +(** Limits expressed with filters *) + +Definition fmap {T U : Type} (f : T -> U) (F : set_system T) : set_system U := + [set P | F (f @^-1` P)]. +Arguments fmap _ _ _ _ _ /. + +Lemma fmapE {U V : Type} (f : U -> V) + (F : set_system U) (P : set V) : fmap f F P = F (f @^-1` P). +Proof. by []. Qed. + +Notation "E @[ x --> F ]" := + (fmap (fun x => E) (nbhs F)) : classical_set_scope. +Notation "E @[ x \oo ]" := + (fmap (fun x => E) \oo) : classical_set_scope. +Notation "f @ F" := (fmap f (nbhs F)) : classical_set_scope. + +Notation limn F := (lim (F @ \oo)). +Notation cvgn F := (cvg (F @ \oo)). + +Global Instance fmap_filter T U (f : T -> U) (F : set_system T) : + Filter F -> Filter (f @ F). +Proof. +move=> FF; constructor => [|P Q|P Q PQ]; rewrite ?fmapE //=. +- exact: filterT. +- exact: filterI. +- by apply: filterS=> ?/PQ. +Qed. +(*Typeclasses Opaque fmap.*) + +Global Instance fmap_proper_filter T U (f : T -> U) (F : set_system T) : + ProperFilter F -> ProperFilter (f @ F). +Proof. +by move=> FF; apply: Build_ProperFilter; rewrite fmapE; apply: filter_not_empty. +Qed. + +Definition fmapi {T U : Type} (f : T -> set U) (F : set_system T) : + set_system _ := + [set P | \forall x \near F, exists y, f x y /\ P y]. + +Notation "E `@[ x --> F ]" := + (fmapi (fun x => E) (nbhs F)) : classical_set_scope. +Notation "f `@ F" := (fmapi f (nbhs F)) : classical_set_scope. + +Lemma fmapiE {U V : Type} (f : U -> set V) + (F : set_system U) (P : set V) : + fmapi f F P = \forall x \near F, exists y, f x y /\ P y. +Proof. by []. Qed. + +Global Instance fmapi_filter T U (f : T -> set U) (F : set_system T) : + {near F, is_totalfun f} -> Filter F -> Filter (f `@ F). +Proof. +move=> f_totalfun FF; rewrite /fmapi; apply: Build_Filter. +- by apply: filterS f_totalfun => x [[y Hy] H]; exists y. +- move=> /= P Q FP FQ; near=> x. + have [//|y [fxy Py]] := near FP x. + have [//|z [fxz Qz]] := near FQ x. + have [//|_ fx_prop] := near f_totalfun x. + by exists y; split => //; split => //; rewrite [y](fx_prop _ z). +- move=> /= P Q subPQ FP; near=> x. + by have [//|y [fxy /subPQ Qy]] := near FP x; exists y. +Unshelve. all: by end_near. Qed. + +#[global] Typeclasses Opaque fmapi. + +Global Instance fmapi_proper_filter + T U (f : T -> U -> Prop) (F : set_system T) : + {near F, is_totalfun f} -> + ProperFilter F -> ProperFilter (f `@ F). +Proof. +move=> f_totalfun FF; apply: Build_ProperFilter_ex. + by move=> P; rewrite /fmapi/= => /filter_ex [x [y [??]]]; exists y. +exact: fmapi_filter. +Qed. + +Lemma cvg_id T (F : set_system T) : x @[x --> F] --> F. +Proof. exact. Qed. +Arguments cvg_id {T F}. + +Lemma fmap_comp {A B C} (f : B -> C) (g : A -> B) F: + Filter F -> (f \o g)%FUN @ F = f @ (g @ F). +Proof. by []. Qed. + +Lemma appfilter U V (f : U -> V) (F : set_system U) : + f @ F = [set P : set _ | \forall x \near F, P (f x)]. +Proof. by []. Qed. + +Lemma cvg_app U V (F G : set_system U) (f : U -> V) : + F --> G -> f @ F --> f @ G. +Proof. by move=> FG P /=; exact: FG. Qed. +Arguments cvg_app {U V F G} _. + +Lemma cvgi_app U V (F G : set_system U) (f : U -> set V) : + F --> G -> f `@ F --> f `@ G. +Proof. by move=> FG P /=; exact: FG. Qed. + +Lemma cvg_comp T U V (f : T -> U) (g : U -> V) + (F : set_system T) (G : set_system U) (H : set_system V) : + f @ F `=>` G -> g @ G `=>` H -> g \o f @ F `=>` H. +Proof. by move=> fFG gGH; apply: cvg_trans gGH => P /fFG. Qed. + +Lemma cvgi_comp T U V (f : T -> U) (g : U -> set V) + (F : set_system T) (G : set_system U) (H : set_system V) : + f @ F `=>` G -> g `@ G `=>` H -> g \o f `@ F `=>` H. +Proof. by move=> fFG gGH; apply: cvg_trans gGH => P /fFG. Qed. + +Lemma near_eq_cvg {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) : + {near F, f =1 g} -> g @ F `=>` f @ F. +Proof. by move=> eq_fg P /=; apply: filterS2 eq_fg => x /= <-. Qed. + +Lemma eq_cvg (T T' : Type) (F : set_system T) (f g : T -> T') (x : set_system T') : + f =1 g -> (f @ F --> x) = (g @ F --> x). +Proof. by move=> /funext->. Qed. + +Lemma eq_is_cvg_in (T T' : Type) (fT : pfilteredType T') (F : set_system T) (f g : T -> T') : + f =1 g -> [cvg (f @ F) in fT] = [cvg (g @ F) in fT]. +Proof. by move=> /funext->. Qed. + +Lemma eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') : + f =1 g -> cvg (f @ F) = cvg (g @ F). +Proof. by move=> /funext->. Qed. + +Lemma neari_eq_loc {T U} {F : set_system T} {FF : Filter F} (f g : T -> set U) : + {near F, f =2 g} -> g `@ F `=>` f `@ F. +Proof. +move=> eq_fg P /=; apply: filterS2 eq_fg => x eq_fg [y [fxy Py]]. +by exists y; rewrite -eq_fg. +Qed. + +Lemma cvg_near_const (T U : Type) (f : T -> U) (F : set_system T) (G : set_system U) : + Filter F -> ProperFilter G -> + (\forall y \near G, \forall x \near F, f x = y) -> f @ F --> G. +Proof. +move=> FF FG fFG P /= GP; rewrite !near_simpl; apply: (have_near G). +by apply: filter_app fFG; near do apply: filterS => x /= ->. +Unshelve. all: by end_near. Qed. + +Definition continuous_at (T U : nbhsType) (x : T) (f : T -> U) := + (f%function @ x --> f%function x). +Notation continuous f := (forall x, continuous_at x f). + +Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) : + {for x, continuous f} -> + (\forall y \near f x, P y) -> (\near x, P (f x)). +Proof. exact. Qed. +Arguments near_fun {T T'} f x. + +(* globally filter *) + +Definition globally {T : Type} (A : set T) : set_system T := + [set P : set T | forall x, A x -> P x]. +Arguments globally {T} A _ /. + +Lemma globally0 {T : Type} (A : set T) : globally set0 A. Proof. by []. Qed. + +Global Instance globally_filter {T : Type} (A : set T) : + Filter (globally A). +Proof. +constructor => //= P Q; last by move=> PQ AP x /AP /PQ. +by move=> AP AQ x Ax; split; [apply: AP|apply: AQ]. +Qed. + +Global Instance globally_properfilter {T : Type} (A : set T) a : + (A a) -> ProperFilter (globally A). +Proof. by move=> Aa; apply: Build_ProperFilter => /(_ a). Qed. + +(** Specific filters *) + +Section frechet_filter. +Variable T : Type. + +Definition frechet_filter := [set S : set T | finite_set (~` S)]. + +Global Instance frechet_properfilter : infinite_set [set: T] -> + ProperFilter frechet_filter. +Proof. +move=> infT; rewrite /frechet_filter. +constructor; first by rewrite /= setC0; exact: infT. +constructor; first by rewrite /= setCT. +- by move=> ? ?; rewrite /= setCI finite_setU. +- by move=> P Q PQ; exact/sub_finite_set/subsetC. +Qed. + +End frechet_filter. + +Global Instance frechet_properfilter_nat : ProperFilter (@frechet_filter nat). +Proof. by apply: frechet_properfilter; exact: infinite_nat. Qed. + +Section at_point. + +Context {T : Type}. + +Definition at_point (a : T) (P : set T) : Prop := P a. + +Global Instance at_point_filter (a : T) : ProperFilter (at_point a). +Proof. by constructor=> //; constructor=> // P Q subPQ /subPQ. Qed. +Typeclasses Opaque at_point. + +End at_point. + +(** Filters for pairs *) + +Global Instance filter_prod_filter T U (F : set_system T) (G : set_system U) : + Filter F -> Filter G -> Filter (filter_prod F G). +Proof. +move=> FF FG; apply: filter_from_filter. + by exists (setT, setT); split; apply: filterT. +move=> [P Q] [P' Q'] /= [FP GQ] [FP' GQ']. +exists (P `&` P', Q `&` Q') => /=; first by split; apply: filterI. +by move=> [x y] [/= [??] []]. +Qed. + +Canonical prod_filter_on T U (F : filter_on T) (G : filter_on U) := + FilterType (filter_prod F G) (filter_prod_filter _ _). + +Global Instance filter_prod_proper {T1 T2 : Type} + {F : (T1 -> Prop) -> Prop} {G : (T2 -> Prop) -> Prop} + {FF : ProperFilter F} {FG : ProperFilter G} : + ProperFilter (filter_prod F G). +Proof. +apply: filter_from_proper => -[A B] [/=FA GB]. +by have [[x ?] [y ?]] := (filter_ex FA, filter_ex GB); exists (x, y). +Qed. + +Lemma filter_prod1 {T U} {F : set_system T} {G : set_system U} + {FG : Filter G} (P : set T) : + (\forall x \near F, P x) -> \forall x \near F & _ \near G, P x. +Proof. +move=> FP; exists (P, setT)=> //= [|[?? []//]]. +by split=> //; apply: filterT. +Qed. + +Lemma filter_prod2 {T U} {F : set_system T} {G : set_system U} + {FF : Filter F} (P : set U) : + (\forall y \near G, P y) -> \forall _ \near F & y \near G, P y. +Proof. +move=> FP; exists (setT, P)=> //= [|[?? []//]]. +by split=> //; apply: filterT. +Qed. + +Program Definition in_filter_prod {T U} {F : set_system T} {G : set_system U} + (P : in_filter F) (Q : in_filter G) : in_filter (filter_prod F G) := + @InFilter _ _ (fun x => prop_of P x.1 /\ prop_of Q x.2) _. +Next Obligation. +move=> T U F G P Q. +by exists (prop_of P, prop_of Q) => //=; split; apply: prop_ofP. +Qed. + +Lemma near_pair {T U} {F : set_system T} {G : set_system U} + {FF : Filter F} {FG : Filter G} + (P : in_filter F) (Q : in_filter G) x : + prop_of P x.1 -> prop_of Q x.2 -> prop_of (in_filter_prod P Q) x. +Proof. by case: x=> x y; do ?rewrite prop_ofE /=; split. Qed. + +Lemma cvg_fst {T U F G} {FG : Filter G} : + (@fst T U) @ filter_prod F G --> F. +Proof. by move=> P; apply: filter_prod1. Qed. + +Lemma cvg_snd {T U F G} {FF : Filter F} : + (@snd T U) @ filter_prod F G --> G. +Proof. by move=> P; apply: filter_prod2. Qed. + +Lemma near_map {T U} (f : T -> U) (F : set_system T) (P : set U) : + (\forall y \near f @ F, P y) = (\forall x \near F, P (f x)). +Proof. by []. Qed. + +Lemma near_map2 {T T' U U'} (f : T -> U) (g : T' -> U') + (F : set_system T) (G : set_system T') (P : U -> set U') : + Filter F -> Filter G -> + (\forall y \near f @ F & y' \near g @ G, P y y') = + (\forall x \near F & x' \near G , P (f x) (g x')). +Proof. +move=> FF FG; rewrite propeqE; split=> -[[A B] /= [fFA fGB] ABP]. + exists (f @^-1` A, g @^-1` B) => //= -[x y /=] xyAB. + by apply: (ABP (_, _)); apply: xyAB. +exists (f @` A, g @` B) => //=; last first. + by move=> -_ [/= [x Ax <-] [x' Bx' <-]]; apply: (ABP (_, _)). +rewrite !nbhs_simpl /fmap /=; split. + by apply: filterS fFA=> x Ax; exists x. +by apply: filterS fGB => x Bx; exists x. +Qed. + +Lemma near_mapi {T U} (f : T -> set U) (F : set_system T) (P : set U) : + (\forall y \near f `@ F, P y) = (\forall x \near F, exists y, f x y /\ P y). +Proof. by []. Qed. + +Lemma filter_pair_set (T T' : Type) (F : set_system T) (F' : set_system T') : + Filter F -> Filter F' -> + forall (P : set T) (P' : set T') (Q : set (T * T')), + (forall x x', P x -> P' x' -> Q (x, x')) -> F P /\ F' P' -> + filter_prod F F' Q. +Proof. +by move=> FF FF' P P' Q PQ [FP FP']; + near=> x do [have := PQ x.1 x.2; rewrite -surjective_pairing; apply]; + [apply: cvg_fst | apply: cvg_snd]. +Unshelve. all: by end_near. Qed. + +Lemma filter_pair_near_of (T T' : Type) (F : set_system T) (F' : set_system T') : + Filter F -> Filter F' -> + forall (P : @in_filter T F) (P' : @in_filter T' F') (Q : set (T * T')), + (forall x x', prop_of P x -> prop_of P' x' -> Q (x, x')) -> + filter_prod F F' Q. +Proof. +move=> FF FF' [P FP] [P' FP'] Q PQ; rewrite prop_ofE in FP FP' PQ. +by exists (P, P') => //= -[t t'] [] /=; exact: PQ. +Qed. + +Tactic Notation "near=>" ident(x) ident(y) := + (apply: filter_pair_near_of => x y ? ?). +Tactic Notation "near" constr(F) "=>" ident(x) ident(y) := + apply: (have_near F); near=> x y. + +Module Export NearMap. +Definition near_simpl := (@near_simpl, @near_map, @near_mapi, @near_map2). +Ltac near_simpl := rewrite ?near_simpl. +End NearMap. + +Lemma filterN {R : numDomainType} (P : pred R) (F : set_system R) : + (\forall x \near - x @[x --> F], (P \o -%R) x) = \forall x \near F, P x. +Proof. by rewrite near_simpl/= !nearE; under eq_fun do rewrite opprK. Qed. + +Lemma cvg_pair {T U V F} {G : set_system U} {H : set_system V} + {FF : Filter F} {FG : Filter G} {FH : Filter H} (f : T -> U) (g : T -> V) : + f @ F --> G -> g @ F --> H -> + (f x, g x) @[x --> F] --> (G, H). +Proof. +move=> fFG gFH P; rewrite !near_simpl => -[[A B] /=[GA HB] ABP]; near=> x. +by apply: (ABP (_, _)); split=> //=; near: x; [apply: fFG|apply: gFH]. +Unshelve. all: by end_near. Qed. + +Lemma cvg_comp2 {T U V W} + {F : set_system T} {G : set_system U} {H : set_system V} {I : set_system W} + {FF : Filter F} {FG : Filter G} {FH : Filter H} + (f : T -> U) (g : T -> V) (h : U -> V -> W) : + f @ F --> G -> g @ F --> H -> + h (fst x) (snd x) @[x --> (G, H)] --> I -> + h (f x) (g x) @[x --> F] --> I. +Proof. by move=> fFG gFH hGHI P /= IP; apply: cvg_pair (hGHI _ IP). Qed. +Arguments cvg_comp2 {T U V W F G H I FF FG FH f g h} _ _ _. +Definition cvg_to_comp_2 := @cvg_comp2. + +(* Lemma cvgi_comp_2 {T U V W} *) +(* {F : set_system T} {G : set_system U} {H : set_system V} {I : set_system W} *) +(* {FF : Filter F} *) +(* (f : T -> U) (g : T -> V) (h : U -> V -> set W) : *) +(* f @ F --> G -> g @ F --> H -> *) +(* h (fst x) (snd x) `@[x --> (G, H)] --> I -> *) +(* h (f x) (g x) `@[x --> F] --> I. *) +(* Proof. *) +(* intros Cf Cg Ch. *) +(* change (fun x => h (f x) (g x)) with (fun x => h (fst (f x, g x)) (snd (f x, g x))). *) +(* apply: cvgi_comp Ch. *) +(* now apply cvg_pair. *) +(* Qed. *) + +(** Restriction of a filter to a domain *) + +Section within. +Context {T : Type}. +Implicit Types (D : set T) (F : set_system T). + +Definition within D F : set_system T := [set P | {near F, D `<=` P}]. +Arguments within : simpl never. + +Lemma near_withinE D F (P : set T) : + (\forall x \near within D F, P x) = {near F, D `<=` P}. +Proof. by []. Qed. + +Lemma withinT F D : Filter F -> within D F D. +Proof. by move=> FF; rewrite /within/=; apply: filterE. Qed. + +Lemma near_withinT F D : Filter F -> \forall x \near within D F, D x. +Proof. exact: withinT. Qed. + +Lemma cvg_within {F} {FF : Filter F} D : within D F --> F. +Proof. by move=> P; apply: filterS. Qed. + +Lemma withinET {F} {FF : Filter F} : within setT F = F. +Proof. +rewrite eqEsubset /within; split => X //=; +by apply: filter_app => //=; apply: nearW => // x; apply. +Qed. + +End within. + +Global Instance within_filter T D F : Filter F -> Filter (@within T D F). +Proof. +move=> FF; rewrite /within; constructor => /=. +- by apply: filterE. +- by move=> P Q; apply: filterS2 => x DP DQ Dx; split; [apply: DP|apply: DQ]. +- by move=> P Q subPQ; apply: filterS => x DP /DP /subPQ. +Qed. + +#[global] Typeclasses Opaque within. + +Canonical within_filter_on T D (F : filter_on T) := + FilterType (within D F) (within_filter _ _). + +Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) + (F : set (set T)) (P : set T) : + Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) -> + F ([set j | P j -> (\bigcap_(i in [set` D]) f i) j]). +Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed. + +Definition subset_filter {T} (F : set_system T) (D : set T) := + [set P : set {x | D x} | F [set x | forall Dx : D x, P (exist _ x Dx)]]. +Arguments subset_filter {T} F D _. + +Global Instance subset_filter_filter T F (D : set T) : + Filter F -> Filter (subset_filter F D). +Proof. +move=> FF; constructor; rewrite /subset_filter/=. +- exact: filterE. +- by move=> P Q; apply: filterS2=> x PD QD Dx; split. +- by move=> P Q subPQ; apply: filterS => R PD Dx; apply: subPQ. +Qed. +#[global] Typeclasses Opaque subset_filter. + +Lemma subset_filter_proper {T F} {FF : Filter F} (D : set T) : + (forall P, F P -> ~ ~ exists x, D x /\ P x) -> + ProperFilter (subset_filter F D). +Proof. +move=> DAP; apply: Build_ProperFilter; rewrite /subset_filter => subFD. +by have /(_ subFD) := DAP (~` D); apply => -[x [dx /(_ dx)]]. +Qed. + +(* For using near on sets in a filter *) +Section NearSet. +Context {Y : Type}. +Context (F : set_system Y) (PF : ProperFilter F). + +Definition powerset_filter_from : set_system (set Y) := filter_from + [set M | [/\ M `<=` F, + (forall E1 E2, M E1 -> F E2 -> E2 `<=` E1 -> M E2) & M !=set0 ] ] + id. + +Global Instance powerset_filter_from_filter : ProperFilter powerset_filter_from. +Proof. +split. + rewrite (_ : xpredp0 = set0); last by rewrite eqEsubset; split. + by move=> [W [_ _ [N +]]]; rewrite subset0 => /[swap] ->; apply. +apply: filter_from_filter. + by exists F; split => //; exists setT; exact: filterT. +move=> M N /= [entM subM [M0 MM0]] [entN subN [N0 NN0]]. +exists [set E | exists P Q, [/\ M P, N Q & E = P `&` Q] ]; first split. +- by move=> ? [? [? [? ? ->]]]; apply: filterI; [exact: entM | exact: entN]. +- move=> ? E2 [P [Q [MP MQ ->]]] entE2 E2subPQ; exists E2, E2. + split; last by rewrite setIid. + + by apply: (subM _ _ MP) => // ? /E2subPQ []. + + by apply: (subN _ _ MQ) => // ? /E2subPQ []. +- by exists (M0 `&` N0), M0, N0. +- move=> E /= [P [Q [MP MQ ->]]]; have entPQ : F (P `&` Q). + by apply: filterI; [exact: entM | exact: entN]. + by split; [apply: (subM _ _ MP) | apply: (subN _ _ MQ)] => // ? []. +Qed. + +Lemma near_small_set : \forall E \near powerset_filter_from, F E. +Proof. by exists F => //; split => //; exists setT; exact: filterT. Qed. + +Lemma small_set_sub (E : set Y) : F E -> + \forall E' \near powerset_filter_from, E' `<=` E. +Proof. +move=> entE; exists [set E' | F E' /\ E' `<=` E]; last by move=> ? []. +split; [by move=> E' [] | | by exists E; split]. +by move=> E1 E2 [] ? subE ? ?; split => //; exact: subset_trans subE. +Qed. + +Lemma near_powerset_filter_fromP (P : set Y -> Prop) : + (forall A B, A `<=` B -> P B -> P A) -> + (\forall U \near powerset_filter_from, P U) <-> exists2 U, F U & P U. +Proof. +move=> Psub; split=> [[M [FM ? [U MU]]] MsubP|[U FU PU]]. + by exists U; [exact: FM | exact: MsubP]. +exists [set V | F V /\ V `<=` U]; last by move=> V [_] /Psub; exact. +split=> [E [] //| |]; last by exists U; split. +by move=> E1 E2 [F1 E1U F2 E2subE1]; split => //; exact: subset_trans E1U. +Qed. + +Lemma powerset_filter_fromP C : + F C -> powerset_filter_from [set W | F W /\ W `<=` C]. +Proof. +move=> FC; exists [set W | F W /\ W `<=` C] => //; split; first by move=> ? []. + by move=> A B [_ AC] FB /subset_trans/(_ AC). +by exists C; split. +Qed. + +End NearSet. + +Lemma near_powerset_map {T U : Type} (f : T -> U) (F : set_system T) + (P : set U -> Prop) : + ProperFilter F -> + (\forall y \near powerset_filter_from (f x @[x --> F]), P y) -> + (\forall y \near powerset_filter_from F, P (f @` y)). +Proof. +move=> FF [] G /= [Gf Gs [D GD GP]]. +have PpF : ProperFilter (powerset_filter_from F). + exact: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD. +near=> M; apply: GP; apply: (Gs D) => //. + apply: filterS; first exact: preimage_image. + exact: (near (near_small_set _) M). +have : M `<=` f @^-1` D by exact: (near (small_set_sub FfD) M). +by move/image_subset/subset_trans; apply; exact: image_preimage_subset. +Unshelve. all: by end_near. Qed. + +Lemma near_powerset_map_monoE {T U : Type} (f : T -> U) (F : set_system T) + (P : set U -> Prop) : + (forall X Y, X `<=` Y -> P Y -> P X) -> + ProperFilter F -> + (\forall y \near powerset_filter_from F, P (f @` y)) = + (\forall y \near powerset_filter_from (f x @[x --> F]), P y). +Proof. +move=> Pmono FF; rewrite propeqE; split; last exact: near_powerset_map. +case=> G /= [Gf Gs [D GD GP]]. +have PpF : ProperFilter (powerset_filter_from (f x @[x-->F])). + exact: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD; have ffiD : fmap f F (f@` D). + by rewrite /fmap /=; apply: filterS; first exact: preimage_image. +near=> M; have FfM : fmap f F M by exact: (near (near_small_set _) M). +apply: (@Pmono _ (f @` D)); first exact: (near (small_set_sub ffiD) M). +exact: GP. +Unshelve. all: by end_near. Qed. + +Section PrincipalFilters. + +Definition principal_filter {X : Type} (x : X) : set_system X := + globally [set x]. + +(** we introducing an alias for pointed types with principal filters *) +Definition principal_filter_type (P : Type) : Type := P. +HB.instance Definition _ (P : choiceType) := + Choice.copy (principal_filter_type P) P. +HB.instance Definition _ (P : pointedType) := + Pointed.on (principal_filter_type P). +HB.instance Definition _ (P : choiceType) := + hasNbhs.Build (principal_filter_type P) principal_filter. +HB.instance Definition _ (P : pointedType) := + Filtered.on (principal_filter_type P). + +Lemma principal_filterP {X} (x : X) (W : set X) : principal_filter x W <-> W x. +Proof. by split=> [|? ? ->]; [exact|]. Qed. + +Lemma principal_filter_proper {X} (x : X) : ProperFilter (principal_filter x). +Proof. exact: globally_properfilter. Qed. + +HB.instance Definition _ := hasNbhs.Build bool principal_filter. + +End PrincipalFilters. + +Section UltraFilters. + +Class UltraFilter T (F : set_system T) := { + #[global] ultra_proper :: ProperFilter F ; + max_filter : forall G : set_system T, ProperFilter G -> F `<=` G -> G = F +}. + +Lemma ultraFilterLemma T (F : set_system T) : + ProperFilter F -> exists G, UltraFilter G /\ F `<=` G. +Proof. +move=> FF. +set filter_preordset := ({G : set_system T & ProperFilter G /\ F `<=` G}). +set preorder := + fun G1 G2 : {classic filter_preordset} => `[< projT1 G1 `<=` projT1 G2 >]. +suff [G Gmax] : exists G : {classic filter_preordset}, premaximal preorder G. + have [GF sFG] := projT2 G; exists (projT1 G); split; last exact: sFG. + split; [exact: GF|move=> H HF sGH]. + have sFH : F `<=` H by apply: subset_trans sGH. + have sHG : preorder (existT _ H (conj HF sFH)) G. + by move/asboolP in sGH; exact: (Gmax (existT _ H (conj HF sFH)) sGH). + by rewrite predeqE => A; split; [move/asboolP : sHG; exact|exact: sGH]. +have sFF : F `<=` F by []. +apply: (ZL_preorder (existT _ F (conj FF sFF))). +- by move=> t; exact/asboolP. +- move=> r s t; rewrite /preorder => /asboolP sr /asboolP st. + exact/asboolP/(subset_trans _ st). +- move=> A Atot; have [[G AG] | A0] := pselect (A !=set0); last first. + exists (existT _ F (conj FF sFF)) => G AG. + by have /asboolP := A0; rewrite asbool_neg => /forallp_asboolPn /(_ G). + have [GF sFG] := projT2 G. + suff UAF : ProperFilter (\bigcup_(H in A) projT1 H). + have sFUA : F `<=` \bigcup_(H in A) projT1 H. + by move=> B FB; exists G => //; exact: sFG. + exists (existT _ (\bigcup_(H in A) projT1 H) (conj UAF sFUA)) => H AH. + by apply/asboolP => B HB /=; exists H. + apply: Build_ProperFilter_ex. + by move=> B [H AH HB]; have [HF _] := projT2 H; exact: (@filter_ex _ _ HF). + split; first by exists G => //; apply: filterT. + + move=> B C [HB AHB HBB] [HC AHC HCC]; have [sHBC|sHCB] := Atot _ _ AHB AHC. + * exists HC => //; have [HCF _] := projT2 HC; apply: filterI HCC. + by move/asboolP : sHBC; exact. + * exists HB => //; have [HBF _] := projT2 HB; apply: filterI HBB _. + by move/asboolP : sHCB; exact. + + move=> B C SBC [H AH HB]; exists H => //; have [HF _] := projT2 H. + exact: filterS HB. +Qed. + +Lemma filter_image (T U : Type) (f : T -> U) (F : set_system T) : + Filter F -> f @` setT = setT -> Filter [set f @` A | A in F]. +Proof. +move=> FF fsurj; split. +- by exists setT => //; apply: filterT. +- move=> _ _ [A FA <-] [B FB <-]. + exists (f @^-1` (f @` A `&` f @` B)); last by rewrite image_preimage. + have sAB : A `&` B `<=` f @^-1` (f @` A `&` f @` B). + by move=> x [Ax Bx]; split; exists x. + by apply: filterS sAB _; apply: filterI. +- move=> A B sAB [C FC fC_eqA]. + exists (f @^-1` B); last by rewrite image_preimage. + by apply: filterS FC => p Cp; apply: sAB; rewrite -fC_eqA; exists p. +Qed. + +Lemma proper_image (T U : Type) (f : T -> U) (F : set_system T) : + ProperFilter F -> f @` setT = setT -> ProperFilter [set f @` A | A in F]. +Proof. +move=> FF fsurj; apply: Build_ProperFilter_ex; last exact: filter_image. +by move=> _ [A FA <-]; have /filter_ex [p Ap] := FA; exists (f p); exists p. +Qed. + +Lemma principal_filter_ultra {T : Type} (x : T) : + UltraFilter (principal_filter x). +Proof. +split=> [|G [G0 xG] FG]; first exact: principal_filter_proper. +rewrite eqEsubset; split => // U GU; apply/principal_filterP. +have /(filterI GU): G [set x] by exact/FG/principal_filterP. +by rewrite setIC set1I; case: ifPn => // /[!inE]. +Qed. + +Lemma in_ultra_setVsetC T (F : set_system T) (A : set T) : + UltraFilter F -> F A \/ F (~` A). +Proof. +move=> FU; case: (pselect (F (~` A))) => [|nFnA]; first by right. +left; suff : ProperFilter (filter_from (F `|` [set A `&` B | B in F]) id). + move=> /max_filter <-; last by move=> B FB; exists B => //; left. + by exists A => //; right; exists setT; [apply: filterT|rewrite setIT]. +apply: filter_from_proper; last first. + move=> B [|[C FC <-]]; first exact: filter_ex. + apply: contrapT => /asboolP; rewrite asbool_neg => /forallp_asboolPn AC0. + by apply: nFnA; apply: filterS FC => p Cp Ap; apply: (AC0 p). +apply: filter_from_filter. + by exists A; right; exists setT; [apply: filterT|rewrite setIT]. +move=> B C [FB|[DB FDB <-]]. + move=> [FC|[DC FDC <-]]; first by exists (B `&` C)=> //; left; apply: filterI. + exists (A `&` (B `&` DC)); last by rewrite setICA. + by right; exists (B `&` DC) => //; apply: filterI. +move=> [FC|[DC FDC <-]]. + exists (A `&` (DB `&` C)); last by rewrite setIA. + by right; exists (DB `&` C) => //; apply: filterI. +exists (A `&` (DB `&` DC)); last by move=> ??; rewrite setIACA setIid. +by right; exists (DB `&` DC) => //; apply: filterI. +Qed. + +Lemma ultra_image (T U : Type) (f : T -> U) (F : set_system T) : + UltraFilter F -> f @` setT = setT -> UltraFilter [set f @` A | A in F]. +Proof. +move=> FU fsurj; split; first exact: proper_image. +move=> G GF sfFG; rewrite predeqE => A; split; last exact: sfFG. +move=> GA; exists (f @^-1` A); last by rewrite image_preimage. +have [//|FnAf] := in_ultra_setVsetC (f @^-1` A) FU. +have : G (f @` (~` (f @^-1` A))) by apply: sfFG; exists (~` (f @^-1` A)). +suff : ~ G (f @` (~` (f @^-1` A))) by []. +rewrite preimage_setC image_preimage // => GnA. +by have /filter_ex [? []] : G (A `&` (~` A)) by apply: filterI. +Qed. + +End UltraFilters. + +Section filter_supremums. + +Global Instance smallest_filter_filter {T : Type} (F : set (set T)) : + Filter (smallest Filter F). +Proof. +split. +- by move=> G [? _]; apply: filterT. +- by move=> ? ? sFP sFQ ? [? ?]; apply: filterI; [apply: sFP | apply: sFQ]. +- by move=> ? ? /filterS + sFP ? [? ?]; apply; apply: sFP. +Qed. + +Fixpoint filterI_iter {T : Type} (F : set (set T)) (n : nat) := + if n is m.+1 + then [set P `&` Q | + P in filterI_iter F m & Q in filterI_iter F m] + else setT |` F. + +Lemma filterI_iter_sub {T : Type} (F : set (set T)) : + {homo filterI_iter F : i j / (i <= j)%N >-> i `<=` j}. +Proof. +move=> + j; elim: j; first by move=> i; rewrite leqn0 => /eqP ->. +move=> j IH i; rewrite leq_eqVlt => /predU1P[->//|]. +by move=> /IH/subset_trans; apply=> A ?; do 2 exists A => //; rewrite setIid. +Qed. + +Lemma filterI_iterE {T : Type} (F : set (set T)) : + smallest Filter F = filter_from (\bigcup_n (filterI_iter F n)) id. +Proof. +rewrite eqEsubset; split. + apply: smallest_sub => //; first last. + by move=> A FA; exists A => //; exists O => //; right. + apply: filter_from_filter; first by exists setT; exists O => //; left. + move=> P Q [i _ sFP] [j _ sFQ]; exists (P `&` Q) => //. + exists (maxn i j).+1 => //=; exists P. + by apply: filterI_iter_sub; first exact: leq_maxl. + by exists Q => //; apply: filterI_iter_sub; first exact: leq_maxr. +move=> + [+ [n _]]; elim: n => [A B|n IH/= A B]. + move=> [-> /[!(@subTset T)] ->|]; first exact: filterT. + by move=> FB /filterS; apply; apply: sub_gen_smallest. +move=> [P sFP] [Q sFQ] PQB /filterS; apply; rewrite -PQB. +by apply: (filterI _ _); [exact: (IH _ _ sFP)|exact: (IH _ _ sFQ)]. +Qed. + +Definition finI_from (I : choiceType) T (D : set I) (f : I -> set T) := + [set \bigcap_(i in [set` D']) f i | + D' in [set A : {fset I} | {subset A <= D}]]. + +Lemma finI_from_cover (I : choiceType) T (D : set I) (f : I -> set T) : + \bigcup_(A in finI_from D f) A = setT. +Proof. +rewrite predeqE => t; split=> // _; exists setT => //. +by exists fset0 => //; rewrite set_fset0 bigcap_set0. +Qed. + +Lemma finI_from1 (I : choiceType) T (D : set I) (f : I -> set T) i : + D i -> finI_from D f (f i). +Proof. +move=> Di; exists [fset i]%fset; first by move=> ?; rewrite !inE => /eqP ->. +by rewrite bigcap_fset big_seq_fset1. +Qed. + +Lemma finI_from_countable (I : pointedType) T (D : set I) (f : I -> set T) : + countable D -> countable (finI_from D f). +Proof. +move=> ?; apply: (card_le_trans (card_image_le _ _)). +exact: fset_subset_countable. +Qed. + +Lemma finI_fromI {I : choiceType} T D (f : I -> set T) A B : + finI_from D f A -> finI_from D f B -> finI_from D f (A `&` B) . +Proof. +case=> N ND <- [M MD <-]; exists (N `|` M)%fset. + by move=> ?; rewrite inE => /orP[/ND | /MD]. +by rewrite -bigcap_setU set_fsetU. +Qed. + +Lemma filterI_iter_finI {I : choiceType} T D (f : I -> set T) : + finI_from D f = \bigcup_n (filterI_iter (f @` D) n). +Proof. +rewrite eqEsubset; split. + move=> A [N /= + <-]; have /finite_setP[n] := finite_fset N; elim: n N. + move=> ?; rewrite II0 card_eq0 => /eqP -> _; rewrite bigcap_set0. + by exists O => //; left. + move=> n IH N /eq_cardSP[x Ax + ND]; rewrite -set_fsetD1 => Nxn. + have NxD : {subset (N `\ x)%fset <= D}. + by move=> ?; rewrite ?inE => /andP [_ /ND /set_mem]. + have [r _ xr] := IH _ Nxn NxD; exists r.+1 => //; exists (f x). + apply: (@filterI_iter_sub _ _ O) => //; right; exists x => //. + by rewrite -inE; apply: ND. + exists (\bigcap_(i in [set` (N `\ x)%fset]) f i) => //. + by rewrite -bigcap_setU1 set_fsetD1 setD1K. +move=> A [n _]; elim: n A. + move=> a [-> |[i Di <-]]; [exists fset0 | exists [fset i]%fset] => //. + - by rewrite set_fset0 bigcap_set0. + - by move=> ?; rewrite !inE => /eqP ->. + - by rewrite set_fset1 bigcap_set1. +by move=> n IH A /= [B snB [C snC <-]]; apply: finI_fromI; apply: IH. +Qed. + +Lemma smallest_filter_finI {T : choiceType} (D : set T) f : + filter_from (finI_from D f) id = smallest (@Filter T) (f @` D). +Proof. by rewrite filterI_iter_finI filterI_iterE. Qed. + +End filter_supremums. + +Definition finI (I : choiceType) T (D : set I) (f : I -> set T) := + forall D' : {fset I}, {subset D' <= D} -> + \bigcap_(i in [set i | i \in D']) f i !=set0. + +Lemma finI_filter (I : choiceType) T (D : set I) (f : I -> set T) : + finI D f -> ProperFilter (filter_from (finI_from D f) id). +Proof. +move=> finIf; apply: (filter_from_proper (filter_from_filter _ _)). +- by exists setT; exists fset0 => //; rewrite predeqE. +- move=> A B [DA sDA IfA] [DB sDB IfB]; exists (A `&` B) => //. + exists (DA `|` DB)%fset. + by move=> ?; rewrite inE => /orP [/sDA|/sDB]. + rewrite -IfA -IfB predeqE => p; split=> [Ifp|[IfAp IfBp] i]. + by split=> i Di; apply: Ifp; rewrite /= inE Di // orbC. + by rewrite /= inE => /orP []; [apply: IfAp|apply: IfBp]. +- by move=> _ [?? <-]; apply: finIf. +Qed. + +Lemma filter_finI (T : choiceType) (F : set_system T) (D : set_system T) + (f : set T -> set T) : + ProperFilter F -> (forall A, D A -> F (f A)) -> finI D f. +Proof. +move=> FF sDFf D' sD; apply: (@filter_ex _ F); apply: filter_bigI. +by move=> A /sD; rewrite inE => /sDFf. +Qed. + +Lemma meets_globallyl T (A : set T) G : + globally A `#` G = forall B, G B -> A `&` B !=set0. +Proof. +rewrite propeqE; split => [/(_ _ _ (fun=> id))//|clA A' B sA]. +by move=> /clA; apply: subsetI_neq0. +Qed. + +Lemma meets_globallyr T F (B : set T) : + F `#` globally B = forall A, F A -> A `&` B !=set0. +Proof. +by rewrite meetsC meets_globallyl; under eq_forall do rewrite setIC. +Qed. + +Lemma meetsxx T (F : set_system T) (FF : Filter F) : F `#` F = ~ (F set0). +Proof. +rewrite propeqE; split => [FmF F0|]; first by have [x []] := FmF _ _ F0 F0. +move=> FN0 A B /filterI FAI {}/FAI FAB; apply/set0P/eqP => AB0. +by rewrite AB0 in FAB. +Qed. + +Lemma proper_meetsxx T (F : set_system T) (FF : ProperFilter F) : F `#` F. +Proof. by rewrite meetsxx; apply: filter_not_empty. Qed. diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 3d6f775f5..9b4f5ad37 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -482,3 +482,26 @@ Qed. End bijection_forall. +Lemma and_prop_in (T : Type) (p : mem_pred T) (P Q : T -> Prop) : + {in p, forall x, P x /\ Q x} <-> + {in p, forall x, P x} /\ {in p, forall x, Q x}. +Proof. +split=> [cnd|[cnd1 cnd2] x xin]; first by split=> x xin; case: (cnd x xin). +by split; [apply: cnd1 | apply: cnd2]. +Qed. + +Lemma mem_inc_segment d (T : porderType d) (a b : T) (f : T -> T) : + {in `[a, b] &, {mono f : x y / (x <= y)%O}} -> + {homo f : x / x \in `[a, b] >-> x \in `[f a, f b]}. +Proof. +move=> fle x xab; have leab : (a <= b)%O by rewrite (itvP xab). +by rewrite in_itv/= !fle ?(itvP xab). +Qed. + +Lemma mem_dec_segment d (T : porderType d) (a b : T) (f : T -> T) : + {in `[a, b] &, {mono f : x y /~ (x <= y)%O}} -> + {homo f : x / x \in `[a, b] >-> x \in `[f b, f a]}. +Proof. +move=> fge x xab; have leab : (a <= b)%O by rewrite (itvP xab). +by rewrite in_itv/= !fge ?(itvP xab). +Qed. diff --git a/theories/ereal.v b/theories/ereal.v index 51a643a27..b6109da43 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -682,10 +682,10 @@ Global Instance ereal_dnbhs_filter : Proof. case=> [x||]. - case: (Proper_dnbhs_numFieldType x) => x0 [//= xT xI xS]. - apply Build_ProperFilter' => //=; apply Build_Filter => //=. + apply Build_ProperFilter => //=; apply Build_Filter => //=. move=> P Q lP lQ; exact: xI. by move=> P Q PQ /xS; apply => y /PQ. -- apply Build_ProperFilter. +- apply Build_ProperFilter_ex. move=> P [x [xr xP]] //; exists (x + 1)%:E; apply xP => /=. by rewrite lte_fin ltrDl. split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]]. @@ -711,7 +711,7 @@ case=> [x||]. by apply/gtMQ; rewrite lte_fin (le_lt_trans _ MQx)// real_ler_normr ?lexx. * by move=> _; split; [apply/gtMP | apply/gtMQ]. + by exists M; split => // ? /gtM /sPQ. -- apply Build_ProperFilter. +- apply Build_ProperFilter_ex. + move=> P [M [Mr ltMP]]; exists (M - 1)%:E. by apply: ltMP; rewrite lte_fin gtrDl oppr_lt0. + split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]]. @@ -751,7 +751,7 @@ Global Instance ereal_nbhs_filter : forall x, ProperFilter (@ereal_nbhs R x). Proof. case=> [r| |]. - case: (ereal_dnbhs_filter r%:E) => r0 [//= nrT rI rS]. - apply: Build_ProperFilter => P /nbhs_ballP[r2 r20 rr2]. + apply: Build_ProperFilter_ex => P /nbhs_ballP[r2 r20 rr2]. by exists r%:E; exact/rr2/ballxx. - exact: (ereal_dnbhs_filter +oo). - exact: (ereal_dnbhs_filter -oo). @@ -762,7 +762,7 @@ End ereal_nbhs_instances. Section ereal_nbhs_infty. Context (R : numFieldType). -Implicit Type (r : R). +Implicit Type r : R. Lemma ereal_nbhs_pinfty_gt r : r \is Num.real -> \forall x \near +oo, r%:E < x. Proof. by exists r. Qed. diff --git a/theories/normedtype.v b/theories/normedtype.v index cb607cbb7..52f4ee754 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -331,7 +331,7 @@ Qed. Global Instance Proper_dnbhs_numFieldType (R : numFieldType) (x : R) : ProperFilter x^'. Proof. -apply: Build_ProperFilter => A /nbhs_ballP[_/posnumP[e] Ae]. +apply: Build_ProperFilter_ex => A /nbhs_ballP[_/posnumP[e] Ae]. exists (x + e%:num / 2); apply: Ae; last first. by rewrite eq_sym addrC -subr_eq subrr eq_sym. rewrite /ball /= opprD addrA subrr distrC subr0 ger0_norm //. @@ -372,7 +372,7 @@ Implicit Types r : R. Global Instance proper_pinfty_nbhs : ProperFilter (pinfty_nbhs R). Proof. -apply Build_ProperFilter. +apply Build_ProperFilter_ex. by move=> P [M [Mreal MP]]; exists (M + 1); apply MP; rewrite ltrDl. split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]]. - by exists 0. @@ -383,7 +383,7 @@ Qed. Global Instance proper_ninfty_nbhs : ProperFilter (ninfty_nbhs R). Proof. -apply Build_ProperFilter. +apply Build_ProperFilter_ex. move=> P [M [Mr ltMP]]; exists (M - 1). by apply: ltMP; rewrite gtrDl oppr_lt0. split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]]. @@ -1127,7 +1127,7 @@ eapply iff_trans; first exact: continuity_pt_nbhs. apply iff_sym. have FF : Filter (f @ x). by typeclasses eauto. - (*by apply fmap_filter; apply: @filter_filter' (locally_filter _).*) + (*by apply fmap_filter; apply: @filter_filter (locally_filter _).*) case: (@fcvg_ballP _ _ (f @ x) FF (f x)) => {FF}H1 H2. (* TODO: in need for lemmas and/or refactoring of already existing lemmas (ball vs. Rabs) *) split => [{H2} - /H1 {}H1 eps|{H1} H]. @@ -1276,17 +1276,17 @@ Local Notation "x ^'+" := (at_right x) : classical_set_scope. Global Instance at_right_proper_filter (x : R) : ProperFilter x^'+. Proof. -apply: Build_ProperFilter' => -[_/posnumP[d] /(_ (x + d%:num / 2))]. -apply; last (by rewrite ltrDl); rewrite /=. -rewrite opprD !addrA subrr add0r normrN normf_div !ger0_norm //. +apply: Build_ProperFilter => -[_/posnumP[d] /(_ (x + d%:num / 2))]. +apply; last by rewrite ltrDl. +rewrite /= opprD !addrA subrr add0r normrN normf_div !ger0_norm //. by rewrite ltr_pdivrMr // ltr_pMr // (_ : 1 = 1%:R) // ltr_nat. Qed. Global Instance at_left_proper_filter (x : R) : ProperFilter x^'-. Proof. -apply: Build_ProperFilter' => -[_ /posnumP[d] /(_ (x - d%:num / 2))]. -apply; last (by rewrite ltrBlDl ltrDr); rewrite /=. -rewrite opprD !addrA subrr add0r opprK normf_div !ger0_norm //. +apply: Build_ProperFilter => -[_ /posnumP[d] /(_ (x - d%:num / 2))]. +apply; last by rewrite ltrBlDl ltrDr. +rewrite /= opprD !addrA subrr add0r opprK normf_div !ger0_norm //. by rewrite ltr_pdivrMr // ltr_pMr // (_ : 1 = 1%:R) // ltr_nat. Qed. @@ -5006,7 +5006,7 @@ have [f [Af clGf]] : [set f | forall i, A i (f i)] `&` suff GF : ProperFilter G. apply: Aco; exists [set v : 'rV[T]_n.+1 | forall i, A i (v ord0 i)] => //. by rewrite predeqE => f; split => Af i; [have := Af i|]; rewrite row_simpl'. - apply Build_ProperFilter. + apply Build_ProperFilter_ex. move=> _ [C FC <-]; have /filter_ex [v Cv] := FC. by exists (v ord0); rewrite /= row_simpl. split. diff --git a/theories/topology.v b/theories/topology.v index 2c62a7556..c94d964a7 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -4,190 +4,15 @@ From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. From mathcomp Require Import archimedean. From mathcomp Require Import boolp classical_sets functions wochoice. From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval. -Require Import reals signed. +From mathcomp Require Import filter reals signed. +From mathcomp Require Export filter. (**md**************************************************************************) -(* # Filters and basic topological notions *) +(* # Basic topological notions *) (* *) -(* This file develops tools for the manipulation of filters and basic *) -(* topological notions. *) -(* *) -(* The development of topological notions builds on "filtered types". They *) -(* are types equipped with an interface that associates to each element a *) -(* set of sets, intended to represent a filter. The notions of limit and *) -(* convergence are defined for filtered types and in the documentation below *) -(* we call "canonical filter" of an element the set of sets associated to it *) -(* by the interface of filtered types. *) -(* *) -(* Table of contents of the documentation: *) -(* 1. Filters *) -(* - Structure of filter *) -(* - Theory of filters *) -(* - Near notations and tactics *) -(* + Notations *) -(* + Tactics *) -(* 2. Basic topological notions *) -(* - Mathematical structures *) -(* + Topology *) -(* + Uniform spaces *) -(* + Pseudometric spaces *) -(* + Complete uniform spaces *) -(* + Complete pseudometric spaces *) -(* + Subspaces of topological spaces *) -(* *) -(******************************************************************************) - -(**md**************************************************************************) -(* # 1. Filters *) -(* *) -(* ## Structure of filter *) -(* ``` *) -(* filteredType U == interface type for types whose *) -(* elements represent sets of sets on U *) -(* These sets are intended to be filters *) -(* on U but this is not enforced yet. *) -(* The HB class is called Filtered. *) -(* It extends Pointed. *) -(* nbhs p == set of sets associated to p (in a *) -(* filtered type) *) -(* pfilteredType U == a pointed and filtered type *) -(* hasNbhs == factory for filteredType *) -(* ``` *) -(* *) -(* We endow several standard types with the structure of filter, e.g.: *) -(* - products `(X1 * X2)%type` *) -(* - matrices `'M[X]_(m, n)` *) -(* - natural numbers `nat` *) -(* *) -(* ## Theory of filters *) -(* ``` *) -(* filter_from D B == set of the supersets of the elements *) -(* of the family of sets B whose indices *) -(* are in the domain D *) -(* This is a filter if (B_i)_(i in D) *) -(* forms a filter base. *) -(* filter_prod F G == product of the filters F and G *) -(* F `=>` G <-> G is included in F *) -(* F and G are sets of sets. *) -(* F --> G <-> the canonical filter associated to G *) -(* is included in the canonical filter *) -(* associated to F *) -(* lim F == limit of the canonical filter *) -(* associated with F if there is such a *) -(* limit, i.e., an element l such that *) -(* the canonical filter associated to l *) -(* is a subset of F *) -(* [lim F in T] == limit of the canonical filter *) -(* associated to F in T where T has type *) -(* filteredType U *) -(* [cvg F in T] <-> the canonical filter associated to F *) -(* converges in T *) -(* cvg F <-> same as [cvg F in T] where T is *) -(* inferred from the type of the *) -(* canonical filter associated to F *) -(* Filter F == type class proving that the set of *) -(* sets F is a filter *) -(* ProperFilter F == type class proving that the set of *) -(* sets F is a proper filter *) -(* UltraFilter F == type class proving that the set of *) -(* sets F is an ultrafilter *) -(* filter_on T == interface type for sets of sets on T *) -(* that are filters *) -(* FilterType F FF == packs the set of sets F with the proof *) -(* FF of Filter F to build a filter_on T *) -(* structure *) -(* pfilter_on T == interface type for sets of sets on T *) -(* that are proper filters *) -(* PFilterPack F FF == packs the set of sets F with the proof *) -(* FF of ProperFilter F to build a *) -(* pfilter_on T structure *) -(* fmap f F == image of the filter F by the function *) -(* f *) -(* E @[x --> F] == image of the canonical filter *) -(* associated to F by the function *) -(* (fun x => E) *) -(* f @ F == image of the canonical filter *) -(* associated to F by the function f *) -(* fmapi f F == image of the filter F by the relation *) -(* f *) -(* E `@[x --> F] == image of the canonical filter *) -(* associated to F by the relation *) -(* (fun x => E) *) -(* f `@ F == image of the canonical filter *) -(* associated to F by the relation f *) -(* globally A == filter of the sets containing A *) -(* @frechet_filter T := [set S : set T | finite_set (~` S)] *) -(* a.k.a. cofinite filter *) -(* at_point a == filter of the sets containing a *) -(* within D F == restriction of the filter F to the *) -(* domain D *) -(* principal_filter x == filter containing every superset of x *) -(* principal_filter_type == alias for choice types with principal *) -(* filters *) -(* subset_filter F D == similar to within D F, but with *) -(* dependent types *) -(* powerset_filter_from F == the filter of downward closed subsets *) -(* of F. *) -(* Enables use of near notation to pick *) -(* suitably small members of F *) -(* in_filter F == interface type for the sets that *) -(* belong to the set of sets F *) -(* InFilter FP == packs a set P with a proof of F P to *) -(* build a in_filter F structure *) -(* \oo == "eventually" filter on nat: set of *) -(* predicates on natural numbers that are *) -(* eventually true *) -(* clopen U == U is both open and closed *) -(* ``` *) -(* *) -(* ## Near notations and tactics *) -(* The purpose of the near notations and tactics is to make the manipulation *) -(* of filters easier. Instead of proving $F\; G$, one can prove $G\; x$ for *) -(* $x$ "near F", i.e., for x such that H x for H arbitrarily precise as long *) -(* as $F\; H$. The near tactics allow for a delayed introduction of $H$: *) -(* $H$ is introduced as an existential variable and progressively *) -(* instantiated during the proof process. *) -(* *) -(* ### Notations *) -(* ``` *) -(* {near F, P} == the property P holds near the *) -(* canonical filter associated to F *) -(* P must have the form forall x, Q x. *) -(* Equivalent to F Q. *) -(* \forall x \near F, P x <-> F (fun x => P x). *) -(* \near x, P x := \forall y \near x, P y. *) -(* {near F & G, P} == same as {near H, P}, where H is the *) -(* product of the filters F and G *) -(* \forall x \near F & y \near G, P x y := {near F & G, forall x y, P x y} *) -(* \forall x & y \near F, P x y == same as before, with G = F *) -(* \near x & y, P x y := \forall z \near x & t \near y, P x y *) -(* x \is_near F == x belongs to a set P : in_filter F *) -(* ``` *) -(* *) -(* ### Tactics *) -(* - near=> x introduces x: *) -(* On the goal \forall x \near F, G x, introduces the variable x and an *) -(* "existential", and an unaccessible hypothesis ?H x and asks the user to *) -(* prove (G x) in this context. *) -(* Under the hood, it delays the proof of F ?H and waits for near: x. *) -(* Also exists under the form near=> x y. *) -(* - near: x discharges x: *) -(* On the goal H_i x, and where x \is_near F, it asks the user to prove *) -(* that (\forall x \near F, H_i x), provided that H_i x does not depend on *) -(* variables introduced after x. *) -(* Under the hood, it refines by intersection the existential variable ?H *) -(* attached to x, computes the intersection with F, and asks the user to *) -(* prove F H_i, right now. *) -(* - end_near should be used to close remaining existentials trivially. *) -(* - near F => x poses a variable near F, where F is a proper filter *) -(* It adds to the context a variable x that \is_near F, i.e., one may *) -(* assume H x for any H in F. This new variable x can be dealt with using *) -(* near: x, as for variables introduced by near=>. *) -(* *) -(******************************************************************************) - -(**md**************************************************************************) -(* # 2. Basic topological notions *) +(* This file develops tools for the manipulation of basic topological *) +(* notions. The development of topological notions builds on "filtered types" *) +(* by extending the hierarchy. *) (* *) (* ## Mathematical structures *) (* ### Topology *) @@ -198,6 +23,8 @@ Require Import reals signed. (* ptopologicalType == a pointed topologicalType *) (* orderTopologicalType == a topology built from intervals *) (* open == set of open sets *) +(* closed == set of closed sets *) +(* clopen U == U is both open and closed *) (* open_nbhs p == set of open neighbourhoods of p *) (* basis B == a family of open sets that converges *) (* to each point *) @@ -232,12 +59,15 @@ Require Import reals signed. (* It builds the mixin for a topological *) (* space from a subbase of open sets b *) (* indexed on domain D *) -(* *) +(* ``` *) (* We endow several standard types with the structure of topology, e.g.: *) (* - products `(T * U)%type` *) (* - matrices `'M[T]_(m, n)` *) (* - natural numbers `nat` *) -(* *) +(* ``` *) +(* \oo == "eventually" filter on nat: set of *) +(* predicates on natural numbers that are *) +(* eventually true *) (* weak_topology f == weak topology by a function f : S -> T *) (* on S *) (* S must be a choiceType and T a *) @@ -398,43 +228,10 @@ Require Import reals signed. (* gauge.type is endowed with a pseudoMetricType *) (* normal_space X == X is normal (sometimes called T4) *) (* regular_space X == X is regular (sometimes called T3) *) - (* ``` *) (* *) (******************************************************************************) -Reserved Notation "{ 'near' x , P }" (at level 0, format "{ 'near' x , P }"). -Reserved Notation "'\forall' x '\near' x_0 , P" - (at level 200, x name, P at level 200, - format "'\forall' x '\near' x_0 , P"). -Reserved Notation "'\near' x , P" - (at level 200, x at level 99, P at level 200, - format "'\near' x , P", only parsing). -Reserved Notation "{ 'near' x & y , P }" - (at level 0, format "{ 'near' x & y , P }"). -Reserved Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P" - (at level 200, x name, y name, P at level 200, - format "'\forall' x '\near' x_0 & y '\near' y_0 , P"). -Reserved Notation "'\forall' x & y '\near' z , P" - (at level 200, x name, y name, P at level 200, - format "'\forall' x & y '\near' z , P"). -Reserved Notation "'\near' x & y , P" - (at level 200, x, y at level 99, P at level 200, - format "'\near' x & y , P", only parsing). -(*Reserved Notation "[ 'filter' 'of' x ]" (format "[ 'filter' 'of' x ]").*) -Reserved Notation "F `=>` G" (at level 70, format "F `=>` G"). -Reserved Notation "F --> G" (at level 70, format "F --> G"). -Reserved Notation "[ 'lim' F 'in' T ]" (format "[ 'lim' F 'in' T ]"). -Reserved Notation "[ 'cvg' F 'in' T ]" (format "[ 'cvg' F 'in' T ]"). -Reserved Notation "x \is_near F" (at level 10, format "x \is_near F"). -Reserved Notation "E @[ x --> F ]" - (at level 60, x name, format "E @[ x --> F ]"). -Reserved Notation "E @[ x \oo ]" - (at level 60, x name, format "E @[ x \oo ]"). -Reserved Notation "f @ F" (at level 60, format "f @ F"). -Reserved Notation "E `@[ x --> F ]" - (at level 60, x name, format "E `@[ x --> F ]"). -Reserved Notation "f `@ F" (at level 60, format "f `@ F"). Reserved Notation "A ^°" (at level 1, format "A ^°"). Reserved Notation "[ 'locally' P ]" (at level 0, format "[ 'locally' P ]"). Reserved Notation "x ^'" (at level 2, format "x ^'"). @@ -453,79 +250,6 @@ From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Section bigmaxmin. -Local Notation max := Order.max. -Local Notation min := Order.min. -Local Open Scope order_scope. -Variables (d : Order.disp_t) (T : orderType d). -Variables (x : T) (I : finType) (P : pred I) (m : T) (F : I -> T). - -Lemma bigmax_geP : reflect (m <= x \/ exists2 i, P i & m <= F i) - (m <= \big[max/x]_(i | P i) F i). -Proof. -apply: (iffP idP) => [|[mx|[i Pi mFi]]]. -- rewrite leNgt => /bigmax_ltP /not_andP[/negP|]; first by rewrite -leNgt; left. - by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -leNgt; right; exists i. -- by rewrite bigmax_idl le_max mx. -- by rewrite (bigmaxD1 i)// le_max mFi. -Qed. - -Lemma bigmax_gtP : reflect (m < x \/ exists2 i, P i & m < F i) - (m < \big[max/x]_(i | P i) F i). -Proof. -apply: (iffP idP) => [|[mx|[i Pi mFi]]]. -- rewrite ltNge => /bigmax_leP /not_andP[/negP|]; first by rewrite -ltNge; left. - by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -ltNge; right; exists i. -- by rewrite bigmax_idl lt_max mx. -- by rewrite (bigmaxD1 i)// lt_max mFi. -Qed. - -Lemma bigmin_leP : reflect (x <= m \/ exists2 i, P i & F i <= m) - (\big[min/x]_(i | P i) F i <= m). -Proof. -apply: (iffP idP) => [|[xm|[i Pi Fim]]]. -- rewrite leNgt => /bigmin_gtP /not_andP[/negP|]; first by rewrite -leNgt; left. - by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -leNgt; right; exists i. -- by rewrite bigmin_idl ge_min xm. -- by rewrite (bigminD1 i)// ge_min Fim. -Qed. - -Lemma bigmin_ltP : reflect (x < m \/ exists2 i, P i & F i < m) - (\big[min/x]_(i | P i) F i < m). -Proof. -apply: (iffP idP) => [|[xm|[i Pi Fim]]]. -- rewrite ltNge => /bigmin_geP /not_andP[/negP|]; first by rewrite -ltNge; left. - by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -ltNge; right; exists i. -- by rewrite bigmin_idl gt_min xm. -- by rewrite (bigminD1 _ _ _ Pi) gt_min Fim. -Qed. - -End bigmaxmin. - -Lemma and_prop_in (T : Type) (p : mem_pred T) (P Q : T -> Prop) : - {in p, forall x, P x /\ Q x} <-> - {in p, forall x, P x} /\ {in p, forall x, Q x}. -Proof. -split=> [cnd|[cnd1 cnd2] x xin]; first by split=> x xin; case: (cnd x xin). -by split; [apply: cnd1 | apply: cnd2]. -Qed. - -Lemma mem_inc_segment d (T : porderType d) (a b : T) (f : T -> T) : - {in `[a, b] &, {mono f : x y / (x <= y)%O}} -> - {homo f : x / x \in `[a, b] >-> x \in `[f a, f b]}. -Proof. -move=> fle x xab; have leab : (a <= b)%O by rewrite (itvP xab). -by rewrite in_itv/= !fle ?(itvP xab). -Qed. - -Lemma mem_dec_segment d (T : porderType d) (a b : T) (f : T -> T) : - {in `[a, b] &, {mono f : x y /~ (x <= y)%O}} -> - {homo f : x / x \in `[a, b] >-> x \in `[f b, f a]}. -Proof. -move=> fge x xab; have leab : (a <= b)%O by rewrite (itvP xab). -by rewrite in_itv/= !fge ?(itvP xab). -Qed. - Section Linear1. Context (R : ringType) (U : lmodType R) (V : zmodType) (s : R -> V -> V). HB.instance Definition _ := gen_eqMixin {linear U -> V | s}. @@ -537,1140 +261,6 @@ HB.instance Definition _ := isPointed.Build {linear U -> V | GRing.Scale.Law.sort s} \0. End Linear2. -Definition set_system U := set (set U). -Identity Coercion set_system_to_set : set_system >-> set. - -HB.mixin Record isFiltered U T := { - nbhs : T -> set_system U -}. - -#[short(type="filteredType")] -HB.structure Definition Filtered (U : Type) := {T of Choice T & isFiltered U T}. - -#[short(type="pfilteredType")] -HB.structure Definition PointedFiltered (U : Type) := {T of Pointed T & isFiltered U T}. -Arguments nbhs {_ _} _ _ : simpl never. - -Notation "[ 'filteredType' U 'of' T ]" := (Filtered.clone U T _) - (at level 0, format "[ 'filteredType' U 'of' T ]") : form_scope. - -HB.instance Definition _ T := Equality.on (set_system T). -HB.instance Definition _ T := Choice.on (set_system T). -HB.instance Definition _ T := Pointed.on (set_system T). -HB.instance Definition _ T := isFiltered.Build T (set_system T) id. - -Arguments nbhs {_ _} _ _ : simpl never. - -HB.mixin Record selfFiltered T := {}. - -HB.factory Record hasNbhs T := { nbhs : T -> set_system T }. -HB.builders Context T of hasNbhs T. - HB.instance Definition _ := isFiltered.Build T T nbhs. - HB.instance Definition _ := selfFiltered.Build T. -HB.end. - -#[short(type="nbhsType")] -HB.structure Definition Nbhs := {T of Choice T & hasNbhs T}. - -#[short(type="pnbhsType")] -HB.structure Definition PointedNbhs := {T of Pointed T & hasNbhs T}. - -Definition filter_from {I T : Type} (D : set I) (B : I -> set T) : - set_system T := [set P | exists2 i, D i & B i `<=` P]. - -(* the canonical filter on matrices on X is the product of the canonical filter - on X *) -HB.instance Definition _ m n X (Z : filteredType X) := - isFiltered.Build 'M[X]_(m, n) 'M[Z]_(m, n) (fun mx => filter_from - [set P | forall i j, nbhs (mx i j) (P i j)] - (fun P => [set my : 'M[X]_(m, n) | forall i j, P i j (my i j)])). - -HB.instance Definition _ m n (X : nbhsType) := selfFiltered.Build 'M[X]_(m, n). - -Definition filter_prod {T U : Type} - (F : set_system T) (G : set_system U) : set_system (T * U) := - filter_from (fun P => F P.1 /\ G P.2) (fun P => P.1 `*` P.2). - -Section Near. - -Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). -Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). -Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). -Local Notation ph := (phantom _). - -Definition prop_near1 {X} {fX : filteredType X} (x : fX) - P (phP : ph {all1 P}) := nbhs x P. - -Definition prop_near2 {X X'} {fX : filteredType X} {fX' : filteredType X'} - (x : fX) (x' : fX') := fun P of ph {all2 P} => - filter_prod (nbhs x) (nbhs x') (fun x => P x.1 x.2). - -End Near. - -Notation "{ 'near' x , P }" := (@prop_near1 _ _ x _ (inPhantom P)) : type_scope. -Notation "'\forall' x '\near' x_0 , P" := {near x_0, forall x, P} : type_scope. -Notation "'\near' x , P" := (\forall x \near x, P) : type_scope. -Notation "{ 'near' x & y , P }" := - (@prop_near2 _ _ _ _ x y _ (inPhantom P)) : type_scope. -Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P" := - {near x_0 & y_0, forall x y, P} : type_scope. -Notation "'\forall' x & y '\near' z , P" := - {near z & z, forall x y, P} : type_scope. -Notation "'\near' x & y , P" := (\forall x \near x & y \near y, P) : type_scope. -Arguments prop_near1 : simpl never. -Arguments prop_near2 : simpl never. - -Lemma nearE {T} {F : set_system T} (P : set T) : - (\forall x \near F, P x) = F P. -Proof. by []. Qed. - -Lemma eq_near {T} {F : set_system T} (P Q : set T) : - (forall x, P x <-> Q x) -> - (\forall x \near F, P x) = (\forall x \near F, Q x). -Proof. by move=> /predeqP ->. Qed. - -(* Definition filter_of X (fX : filteredType X) (x : fX) of phantom fX x := *) -(* nbhs x. *) -(* Notation "[ 'filter' 'of' x ]" := *) -(* (@filter_of _ _ _ (Phantom _ x)) : classical_set_scope. *) -(* Arguments filter_of _ _ _ _ _ /. *) - -Lemma nbhs_filterE {T : Type} (F : set_system T) : nbhs F = F. -Proof. by []. Qed. - -Module Export NbhsFilter. -Definition nbhs_simpl := (@nbhs_filterE). -End NbhsFilter. - -Definition cvg_to {T : Type} (F G : set_system T) := G `<=` F. -Notation "F `=>` G" := (cvg_to F G) : classical_set_scope. -Lemma cvg_refl T (F : set_system T) : F `=>` F. -Proof. exact. Qed. -Arguments cvg_refl {T F}. -#[global] Hint Resolve cvg_refl : core. - -Lemma cvg_trans T (G F H : set_system T) : - (F `=>` G) -> (G `=>` H) -> (F `=>` H). -Proof. by move=> FG GH P /GH /FG. Qed. - -Notation "F --> G" := (cvg_to (nbhs F) (nbhs G)) : classical_set_scope. -Definition type_of_filter {T} (F : set_system T) := T. - -Definition lim_in {U : Type} (T : pfilteredType U) := - fun F : set_system U => get (fun l : T => F --> l). -Notation "[ 'lim' F 'in' T ]" := (@lim_in _ T (nbhs F)) : classical_set_scope. -Definition lim {T : pnbhsType} (F : set_system T) := [lim F in T]. -Notation "[ 'cvg' F 'in' T ]" := (F --> [lim F in T]) : classical_set_scope. -Notation cvg F := (F --> lim F). - -(* :TODO: ultimately nat could be replaced by any lattice *) -Definition eventually := filter_from setT (fun N => [set n | (N <= n)%N]). -Notation "'\oo'" := eventually : classical_set_scope. - -Section FilteredTheory. - -HB.instance Definition _ X1 X2 (Z1 : filteredType X1) (Z2 : filteredType X2) := - isFiltered.Build (X1 * X2)%type (Z1 * Z2)%type - (fun x => filter_prod (nbhs x.1) (nbhs x.2)). - -HB.instance Definition _ (X1 X2 : nbhsType) := - selfFiltered.Build (X1 * X2)%type. - -Lemma cvg_prod T {U U' V V' : filteredType T} (x : U) (l : U') (y : V) (k : V') : - x --> l -> y --> k -> (x, y) --> (l, k). -Proof. -move=> xl yk X [[X1 X2] /= [HX1 HX2] H]; exists (X1, X2) => //=. -split; [exact: xl | exact: yk]. -Qed. - -Lemma cvg_in_ex {U : Type} (T : pfilteredType U) (F : set_system U) : - [cvg F in T] <-> (exists l : T, F --> l). -Proof. by split=> [cvg|/getPex//]; exists [lim F in T]. Qed. - -Lemma cvg_ex (T : pnbhsType) (F : set_system T) : - cvg F <-> (exists l : T, F --> l). -Proof. exact: cvg_in_ex. Qed. - -Lemma cvg_inP {U : Type} (T : pfilteredType U) (F : set_system U) (l : T) : - F --> l -> [cvg F in T]. -Proof. by move=> Fl; apply/cvg_in_ex; exists l. Qed. - -Lemma cvgP (T : pnbhsType) (F : set_system T) (l : T) : F --> l -> cvg F. -Proof. exact: cvg_inP. Qed. - -Lemma cvg_in_toP {U : Type} (T : pfilteredType U) (F : set_system U) (l : T) : - [cvg F in T] -> [lim F in T] = l -> F --> l. -Proof. by move=> /[swap]->. Qed. - -Lemma cvg_toP (T : pnbhsType) (F : set_system T) (l : T) : - cvg F -> lim F = l -> F --> l. -Proof. exact: cvg_in_toP. Qed. - -Lemma dvg_inP {U : Type} (T : pfilteredType U) (F : set_system U) : - ~ [cvg F in T] -> [lim F in T] = point. -Proof. by rewrite /lim_in /=; case xgetP. Qed. - -Lemma dvgP (T : pnbhsType) (F : set_system T) : ~ cvg F -> lim F = point. -Proof. exact: dvg_inP. Qed. - -Lemma cvg_inNpoint {U} (T : pfilteredType U) (F : set_system U) : - [lim F in T] != point -> [cvg F in T]. -Proof. by apply: contra_neqP; apply: dvg_inP. Qed. - -Lemma cvgNpoint (T : pnbhsType) (F : set_system T) : lim F != point -> cvg F. -Proof. exact: cvg_inNpoint. Qed. - -End FilteredTheory. -Arguments cvg_inP {U T F} l. -Arguments dvg_inP {U} T {F}. -Arguments cvgP {T F} l. -Arguments dvgP {T F}. - -Lemma nbhs_nearE {U} {T : filteredType U} (x : T) (P : set U) : - nbhs x P = \near x, P x. -Proof. by []. Qed. - -Lemma near_nbhs {U} {T : filteredType U} (x : T) (P : set U) : - (\forall x \near nbhs x, P x) = \near x, P x. -Proof. by []. Qed. - -Lemma near2_curry {U V} (F : set_system U) (G : set_system V) (P : U -> set V) : - {near F & G, forall x y, P x y} = {near (F, G), forall x, P x.1 x.2}. -Proof. by []. Qed. - -Lemma near2_pair {U V} (F : set_system U) (G : set_system V) (P : set (U * V)) : - {near F & G, forall x y, P (x, y)} = {near (F, G), forall x, P x}. -Proof. by symmetry; congr (nbhs _); rewrite predeqE => -[]. Qed. - -Definition near2E := (@near2_curry, @near2_pair). - -Lemma filter_of_nearI (X : Type) (fX : filteredType X) - (x : fX) : forall P, - nbhs x P = @prop_near1 X fX x P (inPhantom (forall x, P x)). -Proof. by []. Qed. - -Module Export NearNbhs. -Definition near_simpl := (@near_nbhs, @nbhs_nearE, filter_of_nearI). -Ltac near_simpl := rewrite ?near_simpl. -End NearNbhs. - -Lemma near_swap {U V} (F : set_system U) (G : set_system V) (P : U -> set V) : - (\forall x \near F & y \near G, P x y) = (\forall y \near G & x \near F, P x y). -Proof. -rewrite propeqE; split => -[[/=A B] [FA FB] ABP]; -by exists (B, A) => // -[x y] [/=Bx Ay]; apply: (ABP (y, x)). -Qed. - -(** Filters *) - -Class Filter {T : Type} (F : set_system T) := { - filterT : F setT ; - filterI : forall P Q : set T, F P -> F Q -> F (P `&` Q) ; - filterS : forall P Q : set T, P `<=` Q -> F P -> F Q -}. -Global Hint Mode Filter - ! : typeclass_instances. - -Class ProperFilter' {T : Type} (F : set_system T) := { - filter_not_empty : not (F (fun _ => False)) ; - filter_filter' : Filter F -}. -(* TODO: Reuse :> above and remove the following line and the coercion below - after 8.21 is the minimum required version for Coq *) -Global Existing Instance filter_filter'. -Global Hint Mode ProperFilter' - ! : typeclass_instances. -Arguments filter_not_empty {T} F {_}. - -Notation ProperFilter := ProperFilter'. - -Lemma in_nearW {T : Type} (F : set_system T) (P : T -> Prop) (S : set T) : - Filter F -> F S -> {in S, forall x, P x} -> \near F, P F. -Proof. -move=> FF FS SP; rewrite -nbhs_nearE. -by apply: (@filterS _ F _ S) => // x /mem_set /SP. -Qed. - -Lemma filter_setT (T' : Type) : Filter [set: set T']. -Proof. by constructor. Qed. - -Lemma filterP_strong T (F : set_system T) {FF : Filter F} (P : set T) : - (exists Q : set T, exists FQ : F Q, forall x : T, Q x -> P x) <-> F P. -Proof. -split; last by exists P. -by move=> [Q [FQ QP]]; apply: (filterS QP). -Qed. - -Structure filter_on T := FilterType { - filter :> set_system T; - _ : Filter filter -}. -Definition filter_class T (F : filter_on T) : Filter F := - let: FilterType _ class := F in class. -Arguments FilterType {T} _ _. -#[global] Existing Instance filter_class. -(* Typeclasses Opaque filter. *) -Coercion filter_filter' : ProperFilter >-> Filter. - -Structure pfilter_on T := PFilterPack { - pfilter :> (T -> Prop) -> Prop; - _ : ProperFilter pfilter -}. -Definition pfilter_class T (F : pfilter_on T) : ProperFilter F := - let: PFilterPack _ class := F in class. -Arguments PFilterPack {T} _ _. -#[global] Existing Instance pfilter_class. -(* Typeclasses Opaque pfilter. *) -Canonical pfilter_filter_on T (F : pfilter_on T) := - FilterType F (pfilter_class F). -Coercion pfilter_filter_on : pfilter_on >-> filter_on. -Definition PFilterType {T} (F : (T -> Prop) -> Prop) - {fF : Filter F} (fN0 : not (F set0)) := - PFilterPack F (Build_ProperFilter' fN0 fF). -Arguments PFilterType {T} F {fF} fN0. - -HB.instance Definition _ T := gen_eqMixin (filter_on T). -HB.instance Definition _ T := gen_choiceMixin (filter_on T). -HB.instance Definition _ T := isPointed.Build (filter_on T) - (FilterType _ (filter_setT T)). -HB.instance Definition _ T := isFiltered.Build T (filter_on T) (@filter T). - -Global Instance filter_on_Filter T (F : filter_on T) : Filter F. -Proof. by case: F. Qed. -Global Instance pfilter_on_ProperFilter T (F : pfilter_on T) : ProperFilter F. -Proof. by case: F. Qed. - -Lemma nbhs_filter_onE T (F : filter_on T) : nbhs F = nbhs (filter F). -Proof. by []. Qed. -Definition nbhs_simpl := (@nbhs_simpl, @nbhs_filter_onE). - -Lemma near_filter_onE T (F : filter_on T) (P : set T) : - (\forall x \near F, P x) = \forall x \near filter F, P x. -Proof. by []. Qed. -Definition near_simpl := (@near_simpl, @near_filter_onE). - -Program Definition trivial_filter_on T := FilterType [set setT : set T] _. -Next Obligation. -split=> // [_ _ -> ->|Q R sQR QT]; first by rewrite setIT. -by move; rewrite eqEsubset; split => // ? _; apply/sQR; rewrite QT. -Qed. -Canonical trivial_filter_on. - -Lemma filter_nbhsT {T : Type} (F : set_system T) : - Filter F -> nbhs F setT. -Proof. by move=> FF; apply: filterT. Qed. -#[global] Hint Resolve filter_nbhsT : core. - -Lemma nearT {T : Type} (F : set_system T) : Filter F -> \near F, True. -Proof. by move=> FF; apply: filterT. Qed. -#[global] Hint Resolve nearT : core. - -Lemma filter_not_empty_ex {T : Type} (F : set_system T) : - (forall P, F P -> exists x, P x) -> ~ F set0. -Proof. by move=> /(_ set0) ex /ex []. Qed. - -Definition Build_ProperFilter {T : Type} (F : set_system T) - (filter_ex : forall P, F P -> exists x, P x) - (filter_filter : Filter F) := - Build_ProperFilter' (filter_not_empty_ex filter_ex) (filter_filter). - -Lemma filter_ex_subproof {T : Type} (F : set_system T) : - ~ F set0 -> (forall P, F P -> exists x, P x). -Proof. -move=> NFset0 P FP; apply: contra_notP NFset0 => nex; suff <- : P = set0 by []. -by rewrite funeqE => x; rewrite propeqE; split=> // Px; apply: nex; exists x. -Qed. - -Definition filter_ex {T : Type} (F : set_system T) {FF : ProperFilter F} := - filter_ex_subproof (filter_not_empty F). -Arguments filter_ex {T F FF _}. - -Lemma filter_getP {T : pointedType} (F : set_system T) {FF : ProperFilter F} - (P : set T) : F P -> P (get P). -Proof. by move=> /filter_ex /getPex. Qed. - -(* Near Tactic *) - -Record in_filter T (F : set_system T) := InFilter { - prop_in_filter_proj : T -> Prop; - prop_in_filterP_proj : F prop_in_filter_proj -}. -(* add ball x e as a canonical instance of nbhs x *) - -Module Type PropInFilterSig. -Axiom t : forall (T : Type) (F : set_system T), in_filter F -> T -> Prop. -Axiom tE : t = prop_in_filter_proj. -End PropInFilterSig. -Module PropInFilter : PropInFilterSig. -Definition t := prop_in_filter_proj. -Lemma tE : t = prop_in_filter_proj. Proof. by []. Qed. -End PropInFilter. -(* Coercion PropInFilter.t : in_filter >-> Funclass. *) -Notation prop_of := PropInFilter.t. -Definition prop_ofE := PropInFilter.tE. -Notation "x \is_near F" := (@PropInFilter.t _ F _ x). -Definition is_nearE := prop_ofE. - -Lemma prop_ofP T F (iF : @in_filter T F) : F (prop_of iF). -Proof. by rewrite prop_ofE; apply: prop_in_filterP_proj. Qed. - -Definition in_filterT T F (FF : Filter F) : @in_filter T F := - InFilter (filterT). -Canonical in_filterI T F (FF : Filter F) (P Q : @in_filter T F) := - InFilter (filterI (prop_in_filterP_proj P) (prop_in_filterP_proj Q)). - -Lemma filter_near_of T F (P : @in_filter T F) (Q : set T) : Filter F -> - (forall x, prop_of P x -> Q x) -> F Q. -Proof. -by move: P => [P FP] FF /=; rewrite prop_ofE /= => /filterS; apply. -Qed. - -Fact near_key : unit. Proof. exact. Qed. - -Lemma mark_near (P : Prop) : locked_with near_key P -> P. -Proof. by rewrite unlock. Qed. - -Lemma near_acc T F (P : @in_filter T F) (Q : set T) (FF : Filter F) - (FQ : \forall x \near F, Q x) : - locked_with near_key (forall x, prop_of (in_filterI FF P (InFilter FQ)) x -> Q x). -Proof. by rewrite unlock => x /=; rewrite !prop_ofE /= => -[Px]. Qed. - -Lemma near_skip_subproof T F (P Q : @in_filter T F) (G : set T) (FF : Filter F) : - locked_with near_key (forall x, prop_of P x -> G x) -> - locked_with near_key (forall x, prop_of (in_filterI FF P Q) x -> G x). -Proof. -rewrite !unlock => FG x /=; rewrite !prop_ofE /= => -[Px Qx]. -by have /= := FG x; apply; rewrite prop_ofE. -Qed. - -Tactic Notation "near=>" ident(x) := apply: filter_near_of => x ?. - -Ltac just_discharge_near x := - tryif match goal with Hx : x \is_near _ |- _ => move: (x) (Hx); apply: mark_near end - then idtac else fail "the variable" x "is not a ""near"" variable". -Ltac near_skip := - match goal with |- locked_with near_key (forall _, @PropInFilter.t _ _ ?P _ -> _) => - tryif is_evar P then fail "nothing to skip" else apply: near_skip_subproof end. - -Tactic Notation "near:" ident(x) := - just_discharge_near x; - tryif do ![apply: near_acc; first shelve|near_skip] - then idtac - else fail "the goal depends on variables introduced after" x. - -Ltac under_near i tac := near=> i; tac; near: i. -Tactic Notation "near=>" ident(i) "do" tactic3(tac) := under_near i ltac:(tac). -Tactic Notation "near=>" ident(i) "do" "[" tactic4(tac) "]" := near=> i do tac. -Tactic Notation "near" "do" tactic3(tac) := - let i := fresh "i" in under_near i ltac:(tac). -Tactic Notation "near" "do" "[" tactic4(tac) "]" := near do tac. - -Ltac end_near := do ?exact: in_filterT. - -Ltac done := - trivial; hnf; intros; solve - [ do ![solve [trivial | apply: sym_equal; trivial] - | discriminate | contradiction | split] - | match goal with H : ~ _ |- _ => solve [case H; trivial] end - | match goal with |- ?x \is_near _ => near: x; apply: prop_ofP end ]. - -Lemma have_near (U : Type) (fT : filteredType U) (x : fT) (P : Prop) : - ProperFilter (nbhs x) -> (\forall x \near x, P) -> P. -Proof. by move=> FF nP; have [] := @filter_ex _ _ FF (fun=> P). Qed. -Arguments have_near {U fT} x. - -Tactic Notation "near" constr(F) "=>" ident(x) := - apply: (have_near F); near=> x. - -Lemma near T (F : set_system T) P (FP : F P) (x : T) - (Px : prop_of (InFilter FP) x) : P x. -Proof. by move: Px; rewrite prop_ofE. Qed. -Arguments near {T F P} FP x Px. - -Lemma nearW {T : Type} {F : set_system T} (P : T -> Prop) : - Filter F -> (forall x, P x) -> (\forall x \near F, P x). -Proof. by move=> FF FP; exact: (in_nearW _ filterT). Qed. - -Lemma filterE {T : Type} {F : set_system T} : - Filter F -> forall P : set T, (forall x, P x) -> F P. -Proof. by move=> [FT _ +] P fP => /(_ setT); apply. Qed. - -Lemma filter_app (T : Type) (F : set_system T) : - Filter F -> forall P Q : set T, F (fun x => P x -> Q x) -> F P -> F Q. -Proof. by move=> FF P Q subPQ FP; near=> x do suff: P x. -Unshelve. all: by end_near. Qed. - -Lemma filter_app2 (T : Type) (F : set_system T) : - Filter F -> forall P Q R : set T, F (fun x => P x -> Q x -> R x) -> - F P -> F Q -> F R. -Proof. by move=> ???? PQR FP; apply: filter_app; apply: filter_app FP. Qed. - -Lemma filter_app3 (T : Type) (F : set_system T) : - Filter F -> forall P Q R S : set T, F (fun x => P x -> Q x -> R x -> S x) -> - F P -> F Q -> F R -> F S. -Proof. by move=> ????? PQR FP; apply: filter_app2; apply: filter_app FP. Qed. - -Lemma filterS2 (T : Type) (F : set_system T) : - Filter F -> forall P Q R : set T, (forall x, P x -> Q x -> R x) -> - F P -> F Q -> F R. -Proof. by move=> ? ? ? ? ?; apply: filter_app2; apply: filterE. Qed. - -Lemma filterS3 (T : Type) (F : set_system T) : - Filter F -> forall P Q R S : set T, (forall x, P x -> Q x -> R x -> S x) -> - F P -> F Q -> F R -> F S. -Proof. by move=> ? ? ? ? ? ?; apply: filter_app3; apply: filterE. Qed. - -Lemma filter_const {T : Type} {F} {FF: @ProperFilter T F} (P : Prop) : - F (fun=> P) -> P. -Proof. by move=> FP; case: (filter_ex FP). Qed. - -Lemma in_filter_from {I T : Type} (D : set I) (B : I -> set T) (i : I) : - D i -> filter_from D B (B i). -Proof. by exists i. Qed. - -Lemma near_andP {T : Type} F (b1 b2 : T -> Prop) : Filter F -> - (\forall x \near F, b1 x /\ b2 x) <-> - (\forall x \near F, b1 x) /\ (\forall x \near F, b2 x). -Proof. -move=> FF; split=> [H|[H1 H2]]; first by split; apply: filterS H => ? []. -by apply: filterS2 H1 H2. -Qed. - -Lemma nearP_dep {T U} {F : set_system T} {G : set_system U} - {FF : Filter F} {FG : Filter G} (P : T -> U -> Prop) : - (\forall x \near F & y \near G, P x y) -> - \forall x \near F, \forall y \near G, P x y. -Proof. -move=> [[Q R] [/=FQ GR]] QRP. -by apply: filterS FQ => x Q1x; apply: filterS GR => y Q2y; apply: (QRP (_, _)). -Qed. - -Lemma filter2P T U (F : set_system T) (G : set_system U) - {FF : Filter F} {FG : Filter G} (P : set (T * U)) : - (exists2 Q : set T * set U, F Q.1 /\ G Q.2 - & forall (x : T) (y : U), Q.1 x -> Q.2 y -> P (x, y)) - <-> \forall x \near (F, G), P x. -Proof. -split=> [][[A B] /=[FA GB] ABP]; exists (A, B) => //=. - by move=> [a b] [/=Aa Bb]; apply: ABP. -by move=> a b Aa Bb; apply: (ABP (_, _)). -Qed. - -Lemma filter_ex2 {T U : Type} (F : set_system T) (G : set_system U) - {FF : ProperFilter F} {FG : ProperFilter G} (P : set T) (Q : set U) : - F P -> G Q -> exists x : T, exists2 y : U, P x & Q y. -Proof. by move=> /filter_ex [x Px] /filter_ex [y Qy]; exists x, y. Qed. -Arguments filter_ex2 {T U F G FF FG _ _}. - -Lemma filter_fromP {I T : Type} (D : set I) (B : I -> set T) (F : set_system T) : - Filter F -> F `=>` filter_from D B <-> forall i, D i -> F (B i). -Proof. -split; first by move=> FB i ?; apply/FB/in_filter_from. -by move=> FB P [i Di BjP]; apply: (filterS BjP); apply: FB. -Qed. - -Lemma filter_fromTP {I T : Type} (B : I -> set T) (F : set_system T) : - Filter F -> F `=>` filter_from setT B <-> forall i, F (B i). -Proof. by move=> FF; rewrite filter_fromP; split=> [P i|P i _]; apply: P. Qed. - -Lemma filter_from_filter {I T : Type} (D : set I) (B : I -> set T) : - (exists i : I, D i) -> - (forall i j, D i -> D j -> exists2 k, D k & B k `<=` B i `&` B j) -> - Filter (filter_from D B). -Proof. -move=> [i0 Di0] Binter; constructor; first by exists i0. - move=> P Q [i Di BiP] [j Dj BjQ]; have [k Dk BkPQ]:= Binter _ _ Di Dj. - by exists k => // x /BkPQ [/BiP ? /BjQ]. -by move=> P Q subPQ [i Di BiP]; exists i => //; apply: subset_trans subPQ. -Qed. - -Lemma filter_fromT_filter {I T : Type} (B : I -> set T) : - (exists _ : I, True) -> - (forall i j, exists k, B k `<=` B i `&` B j) -> - Filter (filter_from setT B). -Proof. -move=> [i0 _] BI; apply: filter_from_filter; first by exists i0. -by move=> i j _ _; have [k] := BI i j; exists k. -Qed. - -Lemma filter_from_proper {I T : Type} (D : set I) (B : I -> set T) : - Filter (filter_from D B) -> - (forall i, D i -> B i !=set0) -> - ProperFilter (filter_from D B). -Proof. -move=> FF BN0; apply: Build_ProperFilter=> P [i Di BiP]. -by have [x Bix] := BN0 _ Di; exists x; apply: BiP. -Qed. - -Lemma filter_bigI T (I : choiceType) (D : {fset I}) (f : I -> set T) - (F : set_system T) : - Filter F -> (forall i, i \in D -> F (f i)) -> - F (\bigcap_(i in [set` D]) f i). -Proof. -move=> FF FfD. -suff: F [set p | forall i, i \in enum_fset D -> f i p] by []. -have {FfD} : forall i, i \in enum_fset D -> F (f i) by move=> ? /FfD. -elim: (enum_fset D) => [|i s ihs] FfD; first exact: filterS filterT. -apply: (@filterS _ _ _ (f i `&` [set p | forall i, i \in s -> f i p])). - by move=> p [fip fsp] j; rewrite inE => /orP [/eqP->|] //; apply: fsp. -apply: filterI; first by apply: FfD; rewrite inE eq_refl. -by apply: ihs => j sj; apply: FfD; rewrite inE sj orbC. -Qed. - -Lemma filter_forall T (I : finType) (f : I -> set T) (F : set_system T) : - Filter F -> (forall i : I, \forall x \near F, f i x) -> - \forall x \near F, forall i, f i x. -Proof. -move=> FF fIF; apply: filterS (@filter_bigI T I [fset x in I]%fset f F FF _). - by move=> x fIx i; have := fIx i; rewrite /= inE/=; apply. -by move=> i; rewrite inE/= => _; apply: (fIF i). -Qed. - -Lemma filter_imply [T : Type] [P : Prop] [f : set T] [F : set_system T] : - Filter F -> (P -> \near F, f F) -> \near F, P -> f F. -Proof. -move=> ? PF; near do move=> /asboolP. -by case: asboolP=> [/PF|_]; by [apply: filterS|apply: nearW]. -Unshelve. all: by end_near. Qed. - -(** Limits expressed with filters *) - -Definition fmap {T U : Type} (f : T -> U) (F : set_system T) : set_system U := - [set P | F (f @^-1` P)]. -Arguments fmap _ _ _ _ _ /. - -Lemma fmapE {U V : Type} (f : U -> V) - (F : set_system U) (P : set V) : fmap f F P = F (f @^-1` P). -Proof. by []. Qed. - -Notation "E @[ x --> F ]" := - (fmap (fun x => E) (nbhs F)) : classical_set_scope. -Notation "E @[ x \oo ]" := - (fmap (fun x => E) \oo) : classical_set_scope. -Notation "f @ F" := (fmap f (nbhs F)) : classical_set_scope. - -Notation limn F := (lim (F @ \oo)). -Notation cvgn F := (cvg (F @ \oo)). - -Global Instance fmap_filter T U (f : T -> U) (F : set_system T) : - Filter F -> Filter (f @ F). -Proof. -move=> FF; constructor => [|P Q|P Q PQ]; rewrite ?fmapE //=. -- exact: filterT. -- exact: filterI. -- by apply: filterS=> ?/PQ. -Qed. -(*Typeclasses Opaque fmap.*) - -Global Instance fmap_proper_filter T U (f : T -> U) (F : set_system T) : - ProperFilter F -> ProperFilter (f @ F). -Proof. -move=> FF; apply: Build_ProperFilter'; -by rewrite fmapE; apply: filter_not_empty. -Qed. -Definition fmap_proper_filter' := fmap_proper_filter. - -Definition fmapi {T U : Type} (f : T -> set U) (F : set_system T) : - set_system _ := - [set P | \forall x \near F, exists y, f x y /\ P y]. - -Notation "E `@[ x --> F ]" := - (fmapi (fun x => E) (nbhs F)) : classical_set_scope. -Notation "f `@ F" := (fmapi f (nbhs F)) : classical_set_scope. - -Lemma fmapiE {U V : Type} (f : U -> set V) - (F : set_system U) (P : set V) : - fmapi f F P = \forall x \near F, exists y, f x y /\ P y. -Proof. by []. Qed. - -Global Instance fmapi_filter T U (f : T -> set U) (F : set_system T) : - infer {near F, is_totalfun f} -> Filter F -> Filter (f `@ F). -Proof. -move=> f_totalfun FF; rewrite /fmapi; apply: Build_Filter. -- by apply: filterS f_totalfun => x [[y Hy] H]; exists y. -- move=> /= P Q FP FQ; near=> x. - have [//|y [fxy Py]] := near FP x. - have [//|z [fxz Qz]] := near FQ x. - have [//|_ fx_prop] := near f_totalfun x. - by exists y; split => //; split => //; rewrite [y](fx_prop _ z). -- move=> /= P Q subPQ FP; near=> x. - by have [//|y [fxy /subPQ Qy]] := near FP x; exists y. -Unshelve. all: by end_near. Qed. - -#[global] Typeclasses Opaque fmapi. - -Global Instance fmapi_proper_filter - T U (f : T -> U -> Prop) (F : set_system T) : - infer {near F, is_totalfun f} -> - ProperFilter F -> ProperFilter (f `@ F). -Proof. -move=> f_totalfun FF; apply: Build_ProperFilter. -by move=> P; rewrite /fmapi/= => /filter_ex [x [y [??]]]; exists y. -Qed. -Definition filter_map_proper_filter' := fmapi_proper_filter. - -Lemma cvg_id T (F : set_system T) : x @[x --> F] --> F. -Proof. exact. Qed. -Arguments cvg_id {T F}. - -Lemma fmap_comp {A B C} (f : B -> C) (g : A -> B) F: - Filter F -> (f \o g)%FUN @ F = f @ (g @ F). -Proof. by []. Qed. - -Lemma appfilter U V (f : U -> V) (F : set_system U) : - f @ F = [set P : set _ | \forall x \near F, P (f x)]. -Proof. by []. Qed. - -Lemma cvg_app U V (F G : set_system U) (f : U -> V) : - F --> G -> f @ F --> f @ G. -Proof. by move=> FG P /=; exact: FG. Qed. -Arguments cvg_app {U V F G} _. - -Lemma cvgi_app U V (F G : set_system U) (f : U -> set V) : - F --> G -> f `@ F --> f `@ G. -Proof. by move=> FG P /=; exact: FG. Qed. - -Lemma cvg_comp T U V (f : T -> U) (g : U -> V) - (F : set_system T) (G : set_system U) (H : set_system V) : - f @ F `=>` G -> g @ G `=>` H -> g \o f @ F `=>` H. -Proof. by move=> fFG gGH; apply: cvg_trans gGH => P /fFG. Qed. - -Lemma cvgi_comp T U V (f : T -> U) (g : U -> set V) - (F : set_system T) (G : set_system U) (H : set_system V) : - f @ F `=>` G -> g `@ G `=>` H -> g \o f `@ F `=>` H. -Proof. by move=> fFG gGH; apply: cvg_trans gGH => P /fFG. Qed. - -Lemma near_eq_cvg {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) : - {near F, f =1 g} -> g @ F `=>` f @ F. -Proof. by move=> eq_fg P /=; apply: filterS2 eq_fg => x /= <-. Qed. - -Lemma eq_cvg (T T' : Type) (F : set_system T) (f g : T -> T') (x : set_system T') : - f =1 g -> (f @ F --> x) = (g @ F --> x). -Proof. by move=> /funext->. Qed. - -Lemma eq_is_cvg_in (T T' : Type) (fT : pfilteredType T') (F : set_system T) (f g : T -> T') : - f =1 g -> [cvg (f @ F) in fT] = [cvg (g @ F) in fT]. -Proof. by move=> /funext->. Qed. - -Lemma eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') : - f =1 g -> cvg (f @ F) = cvg (g @ F). -Proof. by move=> /funext->. Qed. - -Lemma neari_eq_loc {T U} {F : set_system T} {FF : Filter F} (f g : T -> set U) : - {near F, f =2 g} -> g `@ F `=>` f `@ F. -Proof. -move=> eq_fg P /=; apply: filterS2 eq_fg => x eq_fg [y [fxy Py]]. -by exists y; rewrite -eq_fg. -Qed. - -Lemma cvg_near_const (T U : Type) (f : T -> U) (F : set_system T) (G : set_system U) : - Filter F -> ProperFilter G -> - (\forall y \near G, \forall x \near F, f x = y) -> f @ F --> G. -Proof. -move=> FF FG fFG P /= GP; rewrite !near_simpl; apply: (have_near G). -by apply: filter_app fFG; near do apply: filterS => x /= ->. -Unshelve. all: by end_near. Qed. - -(* globally filter *) - -Definition globally {T : Type} (A : set T) : set_system T := - [set P : set T | forall x, A x -> P x]. -Arguments globally {T} A _ /. - -Lemma globally0 {T : Type} (A : set T) : globally set0 A. Proof. by []. Qed. - -Global Instance globally_filter {T : Type} (A : set T) : - Filter (globally A). -Proof. -constructor => //= P Q; last by move=> PQ AP x /AP /PQ. -by move=> AP AQ x Ax; split; [apply: AP|apply: AQ]. -Qed. - -Global Instance globally_properfilter {T : Type} (A : set T) a : - infer (A a) -> ProperFilter (globally A). -Proof. by move=> Aa; apply: Build_ProperFilter' => /(_ a). Qed. - -(** Specific filters *) - -Section frechet_filter. -Variable T : Type. - -Definition frechet_filter := [set S : set T | finite_set (~` S)]. - -Global Instance frechet_properfilter : infinite_set [set: T] -> - ProperFilter frechet_filter. -Proof. -move=> infT; rewrite /frechet_filter. -constructor; first by rewrite /= setC0; exact: infT. -constructor; first by rewrite /= setCT. -- by move=> ? ?; rewrite /= setCI finite_setU. -- by move=> P Q PQ; exact/sub_finite_set/subsetC. -Qed. - -End frechet_filter. - -Global Instance frechet_properfilter_nat : ProperFilter (@frechet_filter nat). -Proof. by apply: frechet_properfilter; exact: infinite_nat. Qed. - -Section at_point. - -Context {T : Type}. - -Definition at_point (a : T) (P : set T) : Prop := P a. - -Global Instance at_point_filter (a : T) : ProperFilter (at_point a). -Proof. by constructor=> //; constructor=> // P Q subPQ /subPQ. Qed. -Typeclasses Opaque at_point. - -End at_point. - -(** Filters for pairs *) - -Global Instance filter_prod_filter T U (F : set_system T) (G : set_system U) : - Filter F -> Filter G -> Filter (filter_prod F G). -Proof. -move=> FF FG; apply: filter_from_filter. - by exists (setT, setT); split; apply: filterT. -move=> [P Q] [P' Q'] /= [FP GQ] [FP' GQ']. -exists (P `&` P', Q `&` Q') => /=; first by split; apply: filterI. -by move=> [x y] [/= [??] []]. -Qed. - -Canonical prod_filter_on T U (F : filter_on T) (G : filter_on U) := - FilterType (filter_prod F G) (filter_prod_filter _ _). - -Global Instance filter_prod_proper {T1 T2 : Type} - {F : (T1 -> Prop) -> Prop} {G : (T2 -> Prop) -> Prop} - {FF : ProperFilter F} {FG : ProperFilter G} : - ProperFilter (filter_prod F G). -Proof. -apply: filter_from_proper => -[A B] [/=FA GB]. -by have [[x ?] [y ?]] := (filter_ex FA, filter_ex GB); exists (x, y). -Qed. -Definition filter_prod_proper' := @filter_prod_proper. - -Lemma filter_prod1 {T U} {F : set_system T} {G : set_system U} - {FG : Filter G} (P : set T) : - (\forall x \near F, P x) -> \forall x \near F & _ \near G, P x. -Proof. -move=> FP; exists (P, setT)=> //= [|[?? []//]]. -by split=> //; apply: filterT. -Qed. -Lemma filter_prod2 {T U} {F : set_system T} {G : set_system U} - {FF : Filter F} (P : set U) : - (\forall y \near G, P y) -> \forall _ \near F & y \near G, P y. -Proof. -move=> FP; exists (setT, P)=> //= [|[?? []//]]. -by split=> //; apply: filterT. -Qed. - -Program Definition in_filter_prod {T U} {F : set_system T} {G : set_system U} - (P : in_filter F) (Q : in_filter G) : in_filter (filter_prod F G) := - @InFilter _ _ (fun x => prop_of P x.1 /\ prop_of Q x.2) _. -Next Obligation. -move=> T U F G P Q. -by exists (prop_of P, prop_of Q) => //=; split; apply: prop_ofP. -Qed. - -Lemma near_pair {T U} {F : set_system T} {G : set_system U} - {FF : Filter F} {FG : Filter G} - (P : in_filter F) (Q : in_filter G) x : - prop_of P x.1 -> prop_of Q x.2 -> prop_of (in_filter_prod P Q) x. -Proof. by case: x=> x y; do ?rewrite prop_ofE /=; split. Qed. - -Lemma cvg_fst {T U F G} {FG : Filter G} : - (@fst T U) @ filter_prod F G --> F. -Proof. by move=> P; apply: filter_prod1. Qed. - -Lemma cvg_snd {T U F G} {FF : Filter F} : - (@snd T U) @ filter_prod F G --> G. -Proof. by move=> P; apply: filter_prod2. Qed. - -Lemma near_map {T U} (f : T -> U) (F : set_system T) (P : set U) : - (\forall y \near f @ F, P y) = (\forall x \near F, P (f x)). -Proof. by []. Qed. - -Lemma near_map2 {T T' U U'} (f : T -> U) (g : T' -> U') - (F : set_system T) (G : set_system T') (P : U -> set U') : - Filter F -> Filter G -> - (\forall y \near f @ F & y' \near g @ G, P y y') = - (\forall x \near F & x' \near G , P (f x) (g x')). -Proof. -move=> FF FG; rewrite propeqE; split=> -[[A B] /= [fFA fGB] ABP]. - exists (f @^-1` A, g @^-1` B) => //= -[x y /=] xyAB. - by apply: (ABP (_, _)); apply: xyAB. -exists (f @` A, g @` B) => //=; last first. - by move=> -_ [/= [x Ax <-] [x' Bx' <-]]; apply: (ABP (_, _)). -rewrite !nbhs_simpl /fmap /=; split. - by apply: filterS fFA=> x Ax; exists x. -by apply: filterS fGB => x Bx; exists x. -Qed. - -Lemma near_mapi {T U} (f : T -> set U) (F : set_system T) (P : set U) : - (\forall y \near f `@ F, P y) = (\forall x \near F, exists y, f x y /\ P y). -Proof. by []. Qed. - -Lemma filter_pair_set (T T' : Type) (F : set_system T) (F' : set_system T') : - Filter F -> Filter F' -> - forall (P : set T) (P' : set T') (Q : set (T * T')), - (forall x x', P x -> P' x' -> Q (x, x')) -> F P /\ F' P' -> - filter_prod F F' Q. -Proof. -by move=> FF FF' P P' Q PQ [FP FP']; - near=> x do [have := PQ x.1 x.2; rewrite -surjective_pairing; apply]; - [apply: cvg_fst | apply: cvg_snd]. -Unshelve. all: by end_near. Qed. - -Lemma filter_pair_near_of (T T' : Type) (F : set_system T) (F' : set_system T') : - Filter F -> Filter F' -> - forall (P : @in_filter T F) (P' : @in_filter T' F') (Q : set (T * T')), - (forall x x', prop_of P x -> prop_of P' x' -> Q (x, x')) -> - filter_prod F F' Q. -Proof. -move=> FF FF' [P FP] [P' FP'] Q PQ; rewrite prop_ofE in FP FP' PQ. -by exists (P, P') => //= -[t t'] [] /=; exact: PQ. -Qed. - -Tactic Notation "near=>" ident(x) ident(y) := - (apply: filter_pair_near_of => x y ? ?). -Tactic Notation "near" constr(F) "=>" ident(x) ident(y) := - apply: (have_near F); near=> x y. - -Module Export NearMap. -Definition near_simpl := (@near_simpl, @near_map, @near_mapi, @near_map2). -Ltac near_simpl := rewrite ?near_simpl. -End NearMap. - -Lemma filterN {R : numDomainType} (P : pred R) (F : set_system R) : - (\forall x \near - x @[x --> F], (P \o -%R) x) = \forall x \near F, P x. -Proof. by rewrite near_simpl/= !nearE; under eq_fun do rewrite opprK. Qed. - -Lemma cvg_pair {T U V F} {G : set_system U} {H : set_system V} - {FF : Filter F} {FG : Filter G} {FH : Filter H} (f : T -> U) (g : T -> V) : - f @ F --> G -> g @ F --> H -> - (f x, g x) @[x --> F] --> (G, H). -Proof. -move=> fFG gFH P; rewrite !near_simpl => -[[A B] /=[GA HB] ABP]; near=> x. -by apply: (ABP (_, _)); split=> //=; near: x; [apply: fFG|apply: gFH]. -Unshelve. all: by end_near. Qed. - -Lemma cvg_comp2 {T U V W} - {F : set_system T} {G : set_system U} {H : set_system V} {I : set_system W} - {FF : Filter F} {FG : Filter G} {FH : Filter H} - (f : T -> U) (g : T -> V) (h : U -> V -> W) : - f @ F --> G -> g @ F --> H -> - h (fst x) (snd x) @[x --> (G, H)] --> I -> - h (f x) (g x) @[x --> F] --> I. -Proof. by move=> fFG gFH hGHI P /= IP; apply: cvg_pair (hGHI _ IP). Qed. -Arguments cvg_comp2 {T U V W F G H I FF FG FH f g h} _ _ _. -Definition cvg_to_comp_2 := @cvg_comp2. - -(* Lemma cvgi_comp_2 {T U V W} *) -(* {F : set_system T} {G : set_system U} {H : set_system V} {I : set_system W} *) -(* {FF : Filter F} *) -(* (f : T -> U) (g : T -> V) (h : U -> V -> set W) : *) -(* f @ F --> G -> g @ F --> H -> *) -(* h (fst x) (snd x) `@[x --> (G, H)] --> I -> *) -(* h (f x) (g x) `@[x --> F] --> I. *) -(* Proof. *) -(* intros Cf Cg Ch. *) -(* change (fun x => h (f x) (g x)) with (fun x => h (fst (f x, g x)) (snd (f x, g x))). *) -(* apply: cvgi_comp Ch. *) -(* now apply cvg_pair. *) -(* Qed. *) - -(** Restriction of a filter to a domain *) - -Section within. -Context {T : Type}. -Implicit Types (D : set T) (F : set_system T). - -Definition within D F : set_system T := [set P | {near F, D `<=` P}]. -Arguments within : simpl never. - -Lemma near_withinE D F (P : set T) : - (\forall x \near within D F, P x) = {near F, D `<=` P}. -Proof. by []. Qed. - -Lemma withinT F D : Filter F -> within D F D. -Proof. by move=> FF; rewrite /within/=; apply: filterE. Qed. - -Lemma near_withinT F D : Filter F -> \forall x \near within D F, D x. -Proof. exact: withinT. Qed. - -Lemma cvg_within {F} {FF : Filter F} D : within D F --> F. -Proof. by move=> P; apply: filterS. Qed. - -Lemma withinET {F} {FF : Filter F} : within setT F = F. -Proof. -rewrite eqEsubset /within; split => X //=; -by apply: filter_app => //=; apply: nearW => // x; apply. -Qed. - -End within. - -Global Instance within_filter T D F : Filter F -> Filter (@within T D F). -Proof. -move=> FF; rewrite /within; constructor => /=. -- by apply: filterE. -- by move=> P Q; apply: filterS2 => x DP DQ Dx; split; [apply: DP|apply: DQ]. -- by move=> P Q subPQ; apply: filterS => x DP /DP /subPQ. -Qed. - -#[global] Typeclasses Opaque within. - -Canonical within_filter_on T D (F : filter_on T) := - FilterType (within D F) (within_filter _ _). - -Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) - (F : set (set T)) (P : set T) : - Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) -> - F ([set j | P j -> (\bigcap_(i in [set` D]) f i) j]). -Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed. - -Definition subset_filter {T} (F : set_system T) (D : set T) := - [set P : set {x | D x} | F [set x | forall Dx : D x, P (exist _ x Dx)]]. -Arguments subset_filter {T} F D _. - -Global Instance subset_filter_filter T F (D : set T) : - Filter F -> Filter (subset_filter F D). -Proof. -move=> FF; constructor; rewrite /subset_filter/=. -- exact: filterE. -- by move=> P Q; apply: filterS2=> x PD QD Dx; split. -- by move=> P Q subPQ; apply: filterS => R PD Dx; apply: subPQ. -Qed. -#[global] Typeclasses Opaque subset_filter. - -Lemma subset_filter_proper {T F} {FF : Filter F} (D : set T) : - (forall P, F P -> ~ ~ exists x, D x /\ P x) -> - ProperFilter (subset_filter F D). -Proof. -move=> DAP; apply: Build_ProperFilter'; rewrite /subset_filter => subFD. -by have /(_ subFD) := DAP (~` D); apply => -[x [dx /(_ dx)]]. -Qed. - -(* For using near on sets in a filter *) -Section NearSet. -Context {Y : Type}. -Context (F : set_system Y) (PF : ProperFilter F). - -Definition powerset_filter_from : set_system (set Y) := filter_from - [set M | [/\ M `<=` F, - (forall E1 E2, M E1 -> F E2 -> E2 `<=` E1 -> M E2) & M !=set0 ] ] - id. - -Global Instance powerset_filter_from_filter : ProperFilter powerset_filter_from. -Proof. -split. - rewrite (_ : xpredp0 = set0); last by rewrite eqEsubset; split. - by move=> [W [_ _ [N +]]]; rewrite subset0 => /[swap] ->; apply. -apply: filter_from_filter. - by exists F; split => //; exists setT; exact: filterT. -move=> M N /= [entM subM [M0 MM0]] [entN subN [N0 NN0]]. -exists [set E | exists P Q, [/\ M P, N Q & E = P `&` Q] ]; first split. -- by move=> ? [? [? [? ? ->]]]; apply: filterI; [exact: entM | exact: entN]. -- move=> ? E2 [P [Q [MP MQ ->]]] entE2 E2subPQ; exists E2, E2. - split; last by rewrite setIid. - + by apply: (subM _ _ MP) => // ? /E2subPQ []. - + by apply: (subN _ _ MQ) => // ? /E2subPQ []. -- by exists (M0 `&` N0), M0, N0. -- move=> E /= [P [Q [MP MQ ->]]]; have entPQ : F (P `&` Q). - by apply: filterI; [exact: entM | exact: entN]. - by split; [apply: (subM _ _ MP) | apply: (subN _ _ MQ)] => // ? []. -Qed. - -Lemma near_small_set : \forall E \near powerset_filter_from, F E. -Proof. by exists F => //; split => //; exists setT; exact: filterT. Qed. - -Lemma small_set_sub (E : set Y) : F E -> - \forall E' \near powerset_filter_from, E' `<=` E. -Proof. -move=> entE; exists [set E' | F E' /\ E' `<=` E]; last by move=> ? []. -split; [by move=> E' [] | | by exists E; split]. -by move=> E1 E2 [] ? subE ? ?; split => //; exact: subset_trans subE. -Qed. - -Lemma near_powerset_filter_fromP (P : set Y -> Prop) : - (forall A B, A `<=` B -> P B -> P A) -> - (\forall U \near powerset_filter_from, P U) <-> exists2 U, F U & P U. -Proof. -move=> Psub; split=> [[M [FM ? [U MU]]] MsubP|[U FU PU]]. - by exists U; [exact: FM | exact: MsubP]. -exists [set V | F V /\ V `<=` U]; last by move=> V [_] /Psub; exact. -split=> [E [] //| |]; last by exists U; split. -by move=> E1 E2 [F1 E1U F2 E2subE1]; split => //; exact: subset_trans E1U. -Qed. - -Lemma powerset_filter_fromP C : - F C -> powerset_filter_from [set W | F W /\ W `<=` C]. -Proof. -move=> FC; exists [set W | F W /\ W `<=` C] => //; split; first by move=> ? []. - by move=> A B [_ AC] FB /subset_trans/(_ AC). -by exists C; split. -Qed. - -End NearSet. - -Lemma near_powerset_map {T U : Type} (f : T -> U) (F : set_system T) - (P : set U -> Prop) : - ProperFilter F -> - (\forall y \near powerset_filter_from (f x @[x --> F]), P y) -> - (\forall y \near powerset_filter_from F, P (f @` y)). -Proof. -move=> FF [] G /= [Gf Gs [D GD GP]]. -have PpF : ProperFilter (powerset_filter_from F). - exact: powerset_filter_from_filter. -have /= := Gf _ GD; rewrite nbhs_simpl => FfD. -near=> M; apply: GP; apply: (Gs D) => //. - apply: filterS; first exact: preimage_image. - exact: (near (near_small_set _) M). -have : M `<=` f @^-1` D by exact: (near (small_set_sub FfD) M). -by move/image_subset/subset_trans; apply; exact: image_preimage_subset. -Unshelve. all: by end_near. Qed. - -Lemma near_powerset_map_monoE {T U : Type} (f : T -> U) (F : set_system T) - (P : set U -> Prop) : - (forall X Y, X `<=` Y -> P Y -> P X) -> - ProperFilter F -> - (\forall y \near powerset_filter_from F, P (f @` y)) = - (\forall y \near powerset_filter_from (f x @[x --> F]), P y). -Proof. -move=> Pmono FF; rewrite propeqE; split; last exact: near_powerset_map. -case=> G /= [Gf Gs [D GD GP]]. -have PpF : ProperFilter (powerset_filter_from (f x @[x-->F])). - exact: powerset_filter_from_filter. -have /= := Gf _ GD; rewrite nbhs_simpl => FfD; have ffiD : fmap f F (f@` D). - by rewrite /fmap /=; apply: filterS; first exact: preimage_image. -near=> M; have FfM : fmap f F M by exact: (near (near_small_set _) M). -apply: (@Pmono _ (f @` D)); first exact: (near (small_set_sub ffiD) M). -exact: GP. -Unshelve. all: by end_near. Qed. - -Section PrincipalFilters. - -Definition principal_filter {X : Type} (x : X) : set_system X := - globally [set x]. - -(** we introducing an alias for pointed types with principal filters *) -Definition principal_filter_type (P : Type) : Type := P. -HB.instance Definition _ (P : choiceType) := - Choice.copy (principal_filter_type P) P. -HB.instance Definition _ (P : pointedType) := - Pointed.on (principal_filter_type P). -HB.instance Definition _ (P : choiceType) := - hasNbhs.Build (principal_filter_type P) principal_filter. -HB.instance Definition _ (P : pointedType) := - Filtered.on (principal_filter_type P). - -Lemma principal_filterP {X} (x : X) (W : set X) : principal_filter x W <-> W x. -Proof. by split=> [|? ? ->]; [exact|]. Qed. - -Lemma principal_filter_proper {X} (x : X) : ProperFilter (principal_filter x). -Proof. exact: globally_properfilter. Qed. - -HB.instance Definition _ := hasNbhs.Build bool principal_filter. - -End PrincipalFilters. - (** Topological spaces *) HB.mixin Record Nbhs_isTopological (T : Type) of Nbhs T := { open : set_system T; @@ -1827,16 +417,6 @@ Proof. exact: @nbhs_pfilter T x. Qed. Notation "A ^°" := (interior A) : classical_set_scope. -Definition continuous_at (T U : nbhsType) (x : T) (f : T -> U) := - (f%function @ x --> f%function x). -Notation continuous f := (forall x, continuous_at x f). - -Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) : - {for x, continuous f} -> - (\forall y \near f x, P y) -> (\near x, P (f x)). -Proof. exact. Qed. -Arguments near_fun {T T'} f x. - Lemma continuousP (S T : topologicalType) (f : S -> T) : continuous f <-> forall A, open A -> open (f @^-1` A). Proof. @@ -2020,7 +600,7 @@ Let nbhsE_subproof (p : T) : Proof. rewrite predeqE => A; split=> [p_A|]; last first. move=> [B [Bop Bp sBA]]; apply: filterS sBA _; last exact: Bop. - exact/filter_filter'/nbhs_filter. + exact/nbhs_filter. exists (nbhs^~ A); split=> //; first by move=> ?; apply: nbhs_nbhs. by move=> q /nbhs_singleton. Qed. @@ -2052,7 +632,7 @@ HB.instance Definition _ := hasNbhs.Build T (nbhs_of_open op). Let nbhs_pfilter_subproof (p : T) : ProperFilter (nbhs p). Proof. -apply: Build_ProperFilter. +apply: Build_ProperFilter_ex. by move=> A [B [_ Bp sBA]]; exists p; apply: sBA. split; first by exists setT; split=> [|//|//]; exact: opT. move=> A B [C [Cop Cp sCA]] [D [Dop Dp sDB]]. @@ -2142,113 +722,6 @@ HB.instance Definition _ := isOpenTopological.Build T HB.end. -Section filter_supremums. - -Global Instance smallest_filter_filter {T : Type} (F : set (set T)) : - Filter (smallest Filter F). -Proof. -split. -- by move=> G [? _]; apply: filterT. -- by move=> ? ? sFP sFQ ? [? ?]; apply: filterI; [apply: sFP | apply: sFQ]. -- by move=> ? ? /filterS + sFP ? [? ?]; apply; apply: sFP. -Qed. - -Fixpoint filterI_iter {T : Type} (F : set (set T)) (n : nat) := - if n is m.+1 - then [set P `&` Q | - P in filterI_iter F m & Q in filterI_iter F m] - else setT |` F. - -Lemma filterI_iter_sub {T : Type} (F : set (set T)) : - {homo filterI_iter F : i j / (i <= j)%N >-> i `<=` j}. -Proof. -move=> + j; elim: j; first by move=> i; rewrite leqn0 => /eqP ->. -move=> j IH i; rewrite leq_eqVlt => /predU1P[->//|]. -by move=> /IH/subset_trans; apply=> A ?; do 2 exists A => //; rewrite setIid. -Qed. - -Lemma filterI_iterE {T : Type} (F : set (set T)) : - smallest Filter F = filter_from (\bigcup_n (filterI_iter F n)) id. -Proof. -rewrite eqEsubset; split. - apply: smallest_sub => //; first last. - by move=> A FA; exists A => //; exists O => //; right. - apply: filter_from_filter; first by exists setT; exists O => //; left. - move=> P Q [i _ sFP] [j _ sFQ]; exists (P `&` Q) => //. - exists (maxn i j).+1 => //=; exists P. - by apply: filterI_iter_sub; first exact: leq_maxl. - by exists Q => //; apply: filterI_iter_sub; first exact: leq_maxr. -move=> + [+ [n _]]; elim: n => [A B|n IH/= A B]. - move=> [-> /[!(@subTset T)] ->|]; first exact: filterT. - by move=> FB /filterS; apply; apply: sub_gen_smallest. -move=> [P sFP] [Q sFQ] PQB /filterS; apply; rewrite -PQB. -by apply: (filterI _ _); [exact: (IH _ _ sFP)|exact: (IH _ _ sFQ)]. -Qed. - -(** Topology defined by a subbase of open sets *) - -Definition finI_from (I : choiceType) T (D : set I) (f : I -> set T) := - [set \bigcap_(i in [set` D']) f i | - D' in [set A : {fset I} | {subset A <= D}]]. - -Lemma finI_from_cover (I : choiceType) T (D : set I) (f : I -> set T) : - \bigcup_(A in finI_from D f) A = setT. -Proof. -rewrite predeqE => t; split=> // _; exists setT => //. -by exists fset0 => //; rewrite set_fset0 bigcap_set0. -Qed. - -Lemma finI_from1 (I : choiceType) T (D : set I) (f : I -> set T) i : - D i -> finI_from D f (f i). -Proof. -move=> Di; exists [fset i]%fset; first by move=> ?; rewrite !inE => /eqP ->. -by rewrite bigcap_fset big_seq_fset1. -Qed. - -Lemma finI_from_countable (I : pointedType) T (D : set I) (f : I -> set T) : - countable D -> countable (finI_from D f). -Proof. -move=> ?; apply: (card_le_trans (card_image_le _ _)). -exact: fset_subset_countable. -Qed. - -Lemma finI_fromI {I : choiceType} T D (f : I -> set T) A B : - finI_from D f A -> finI_from D f B -> finI_from D f (A `&` B) . -Proof. -case=> N ND <- [M MD <-]; exists (N `|` M)%fset. - by move=> ?; rewrite inE => /orP[/ND | /MD]. -by rewrite -bigcap_setU set_fsetU. -Qed. - -Lemma filterI_iter_finI {I : choiceType} T D (f : I -> set T) : - finI_from D f = \bigcup_n (filterI_iter (f @` D) n). -Proof. -rewrite eqEsubset; split. - move=> A [N /= + <-]; have /finite_setP[n] := finite_fset N; elim: n N. - move=> ?; rewrite II0 card_eq0 => /eqP -> _; rewrite bigcap_set0. - by exists O => //; left. - move=> n IH N /eq_cardSP[x Ax + ND]; rewrite -set_fsetD1 => Nxn. - have NxD : {subset (N `\ x)%fset <= D}. - by move=> ?; rewrite ?inE => /andP [_ /ND /set_mem]. - have [r _ xr] := IH _ Nxn NxD; exists r.+1 => //; exists (f x). - apply: (@filterI_iter_sub _ _ O) => //; right; exists x => //. - by rewrite -inE; apply: ND. - exists (\bigcap_(i in [set` (N `\ x)%fset]) f i) => //. - by rewrite -bigcap_setU1 set_fsetD1 setD1K. -move=> A [n _]; elim: n A. - move=> a [-> |[i Di <-]]; [exists fset0 | exists [fset i]%fset] => //. - - by rewrite set_fset0 bigcap_set0. - - by move=> ?; rewrite !inE => /eqP ->. - - by rewrite set_fset1 bigcap_set1. -by move=> n IH A /= [B snB [C snC <-]]; apply: finI_fromI; apply: IH. -Qed. - -Lemma smallest_filter_finI {T : choiceType} (D : set T) f : - filter_from (finI_from D f) id = smallest (@Filter T) (f @` D). -Proof. by rewrite filterI_iter_finI filterI_iterE. Qed. - -End filter_supremums. - HB.factory Record isSubBaseTopological T of Choice T := { I : pointedType; D : set I; @@ -2646,30 +1119,6 @@ Qed. Lemma meets_openl {T : topologicalType} (F : set_system T) (x : T) : nbhs x `#` F = open_nbhs x `#` F. Proof. by rewrite meetsC meets_openr meetsC. Qed. - -Lemma meets_globallyl T (A : set T) G : - globally A `#` G = forall B, G B -> A `&` B !=set0. -Proof. -rewrite propeqE; split => [/(_ _ _ (fun=> id))//|clA A' B sA]. -by move=> /clA; apply: subsetI_neq0. -Qed. - -Lemma meets_globallyr T F (B : set T) : - F `#` globally B = forall A, F A -> A `&` B !=set0. -Proof. -by rewrite meetsC meets_globallyl; under eq_forall do rewrite setIC. -Qed. - -Lemma meetsxx T (F : set_system T) (FF : Filter F) : F `#` F = ~ (F set0). -Proof. -rewrite propeqE; split => [FmF F0|]; first by have [x []] := FmF _ _ F0 F0. -move=> FN0 A B /filterI FAI {}/FAI FAB; apply/set0P/eqP => AB0. -by rewrite AB0 in FAB. -Qed. - -Lemma proper_meetsxx T (F : set_system T) (FF : ProperFilter F) : F `#` F. -Proof. by rewrite meetsxx; apply: filter_not_empty. Qed. - (** Closed sets in topological spaces *) Section Closed. @@ -2938,7 +1387,7 @@ Typeclasses Opaque within. Global Instance within_nbhs_proper (A : set T) p : infer (closure A p) -> ProperFilter (within A (nbhs p)). Proof. -move=> clAp; apply: Build_ProperFilter => B. +move=> clAp; apply: Build_ProperFilter_ex => B. by move=> /clAp [q [Aq AqsoBq]]; exists q; apply: AqsoBq. Qed. @@ -3083,13 +1532,6 @@ Unshelve. all: by end_near. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `compact_setX`")] Notation compact_setM := compact_setX (only parsing). -Section UltraFilters. - -Class UltraFilter T (F : set_system T) := { - #[global] ultra_proper :: ProperFilter F ; - max_filter : forall G : set_system T, ProperFilter G -> F `<=` G -> G = F -}. - Lemma ultra_cvg_clusterE (T : topologicalType) (F : set_system T) : UltraFilter F -> cluster F = [set p | F --> p]. Proof. @@ -3098,46 +1540,6 @@ move=> FU; rewrite predeqE => p; split. by move=> cvFp; rewrite cluster_cvgE; exists F; [apply: ultra_proper|split]. Qed. -Lemma ultraFilterLemma T (F : set_system T) : - ProperFilter F -> exists G, UltraFilter G /\ F `<=` G. -Proof. -move=> FF. -set filter_preordset := ({G : set_system T & ProperFilter G /\ F `<=` G}). -set preorder := - fun G1 G2 : {classic filter_preordset} => `[< projT1 G1 `<=` projT1 G2 >]. -suff [G Gmax] : exists G : {classic filter_preordset}, premaximal preorder G. - have [GF sFG] := projT2 G; exists (projT1 G); split; last exact: sFG. - split; [exact: GF|move=> H HF sGH]. - have sFH : F `<=` H by apply: subset_trans sGH. - have sHG : preorder (existT _ H (conj HF sFH)) G. - by move/asboolP in sGH; exact: (Gmax (existT _ H (conj HF sFH)) sGH). - by rewrite predeqE => A; split; [move/asboolP : sHG; exact|exact: sGH]. -have sFF : F `<=` F by []. -apply: (ZL_preorder (existT _ F (conj FF sFF))). -- by move=> t; exact/asboolP. -- move=> r s t; rewrite /preorder => /asboolP sr /asboolP st. - exact/asboolP/(subset_trans _ st). -- move=> A Atot; have [[G AG] | A0] := pselect (A !=set0); last first. - exists (existT _ F (conj FF sFF)) => G AG. - by have /asboolP := A0; rewrite asbool_neg => /forallp_asboolPn /(_ G). - have [GF sFG] := projT2 G. - suff UAF : ProperFilter (\bigcup_(H in A) projT1 H). - have sFUA : F `<=` \bigcup_(H in A) projT1 H. - by move=> B FB; exists G => //; exact: sFG. - exists (existT _ (\bigcup_(H in A) projT1 H) (conj UAF sFUA)) => H AH. - by apply/asboolP => B HB /=; exists H. - apply: Build_ProperFilter. - by move=> B [H AH HB]; have [HF _] := projT2 H; exact: (@filter_ex _ _ HF). - split; first by exists G => //; apply: filterT. - + move=> B C [HB AHB HBB] [HC AHC HCC]; have [sHBC|sHCB] := Atot _ _ AHB AHC. - * exists HC => //; have [HCF _] := projT2 HC; apply: filterI HCC. - by move/asboolP : sHBC; exact. - * exists HB => //; have [HBF _] := projT2 HB; apply: filterI HBB _. - by move/asboolP : sHCB; exact. - + move=> B C SBC [H AH HB]; exists H => //; have [HF _] := projT2 H. - exact: filterS HB. -Qed. - Lemma compact_ultra (T : topologicalType) : compact = [set A | forall F : set_system T, UltraFilter F -> F A -> A `&` [set p | F --> p] !=set0]. @@ -3150,74 +1552,6 @@ rewrite /= -[_ --> p]/([set _ | _] p) -ultra_cvg_clusterE. by move=> /(cvg_cluster sFG); exists p. Qed. -Lemma filter_image (T U : Type) (f : T -> U) (F : set_system T) : - Filter F -> f @` setT = setT -> Filter [set f @` A | A in F]. -Proof. -move=> FF fsurj; split. -- by exists setT => //; apply: filterT. -- move=> _ _ [A FA <-] [B FB <-]. - exists (f @^-1` (f @` A `&` f @` B)); last by rewrite image_preimage. - have sAB : A `&` B `<=` f @^-1` (f @` A `&` f @` B). - by move=> x [Ax Bx]; split; exists x. - by apply: filterS sAB _; apply: filterI. -- move=> A B sAB [C FC fC_eqA]. - exists (f @^-1` B); last by rewrite image_preimage. - by apply: filterS FC => p Cp; apply: sAB; rewrite -fC_eqA; exists p. -Qed. - -Lemma proper_image (T U : Type) (f : T -> U) (F : set_system T) : - ProperFilter F -> f @` setT = setT -> ProperFilter [set f @` A | A in F]. -Proof. -move=> FF fsurj; apply: Build_ProperFilter; last exact: filter_image. -by move=> _ [A FA <-]; have /filter_ex [p Ap] := FA; exists (f p); exists p. -Qed. - -Lemma principal_filter_ultra {T : Type} (x : T) : - UltraFilter (principal_filter x). -Proof. -split=> [|G [G0 xG] FG]; first exact: principal_filter_proper. -rewrite eqEsubset; split => // U GU; apply/principal_filterP. -have /(filterI GU): G [set x] by exact/FG/principal_filterP. -by rewrite setIC set1I; case: ifPn => // /[!inE]. -Qed. - -Lemma in_ultra_setVsetC T (F : set_system T) (A : set T) : - UltraFilter F -> F A \/ F (~` A). -Proof. -move=> FU; case: (pselect (F (~` A))) => [|nFnA]; first by right. -left; suff : ProperFilter (filter_from (F `|` [set A `&` B | B in F]) id). - move=> /max_filter <-; last by move=> B FB; exists B => //; left. - by exists A => //; right; exists setT; [apply: filterT|rewrite setIT]. -apply: filter_from_proper; last first. - move=> B [|[C FC <-]]; first exact: filter_ex. - apply: contrapT => /asboolP; rewrite asbool_neg => /forallp_asboolPn AC0. - by apply: nFnA; apply: filterS FC => p Cp Ap; apply: (AC0 p). -apply: filter_from_filter. - by exists A; right; exists setT; [apply: filterT|rewrite setIT]. -move=> B C [FB|[DB FDB <-]]. - move=> [FC|[DC FDC <-]]; first by exists (B `&` C)=> //; left; apply: filterI. - exists (A `&` (B `&` DC)); last by rewrite setICA. - by right; exists (B `&` DC) => //; apply: filterI. -move=> [FC|[DC FDC <-]]. - exists (A `&` (DB `&` C)); last by rewrite setIA. - by right; exists (DB `&` C) => //; apply: filterI. -exists (A `&` (DB `&` DC)); last by move=> ??; rewrite setIACA setIid. -by right; exists (DB `&` DC) => //; apply: filterI. -Qed. - -Lemma ultra_image (T U : Type) (f : T -> U) (F : set_system T) : - UltraFilter F -> f @` setT = setT -> UltraFilter [set f @` A | A in F]. -Proof. -move=> FU fsurj; split; first exact: proper_image. -move=> G GF sfFG; rewrite predeqE => A; split; last exact: sfFG. -move=> GA; exists (f @^-1` A); last by rewrite image_preimage. -have [//|FnAf] := in_ultra_setVsetC (f @^-1` A) FU. -have : G (f @` (~` (f @^-1` A))) by apply: sfFG; exists (~` (f @^-1` A)). -suff : ~ G (f @` (~` (f @^-1` A))) by []. -rewrite preimage_setC image_preimage // => GnA. -by have /filter_ex [? []] : G (A `&` (~` A)) by apply: filterI. -Qed. - Lemma compact_cluster_set1 {T : topologicalType} (x : T) F V : hausdorff_space T -> compact V -> nbhs x V -> ProperFilter F -> F V -> cluster F = [set x] -> F --> x. @@ -3240,7 +1574,6 @@ move=> M [MF ME2 [W] MW /(_ _ MW) VUW]. apply: (@filterS _ _ _ (V `&` W)); last by apply: filterI => //; exact: MF. by move=> t [Vt Wt]; apply: contrapT => Ut; exact: (VUW t). Qed. -End UltraFilters. Section Precompact. @@ -3299,33 +1632,6 @@ Qed. Definition locally_compact (A : set X) := [locally precompact A]. End Precompact. - -Definition finI (I : choiceType) T (D : set I) (f : I -> set T) := - forall D' : {fset I}, {subset D' <= D} -> - \bigcap_(i in [set i | i \in D']) f i !=set0. - -Lemma finI_filter (I : choiceType) T (D : set I) (f : I -> set T) : - finI D f -> ProperFilter (filter_from (finI_from D f) id). -Proof. -move=> finIf; apply: (filter_from_proper (filter_from_filter _ _)). -- by exists setT; exists fset0 => //; rewrite predeqE. -- move=> A B [DA sDA IfA] [DB sDB IfB]; exists (A `&` B) => //. - exists (DA `|` DB)%fset. - by move=> ?; rewrite inE => /orP [/sDA|/sDB]. - rewrite -IfA -IfB predeqE => p; split=> [Ifp|[IfAp IfBp] i]. - by split=> i Di; apply: Ifp; rewrite /= inE Di // orbC. - by rewrite /= inE => /orP []; [apply: IfAp|apply: IfBp]. -- by move=> _ [?? <-]; apply: finIf. -Qed. - -Lemma filter_finI (T : choiceType) (F : set_system T) (D : set_system T) - (f : set T -> set T) : - ProperFilter F -> (forall A, D A -> F (f A)) -> finI D f. -Proof. -move=> FF sDFf D' sD; apply: (@filter_ex _ F); apply: filter_bigI. -by move=> A /sD; rewrite inE => /sDFf. -Qed. - Definition finite_subset_cover (I : choiceType) (D : set I) U (F : I -> set U) (A : set U) := exists2 D' : {fset I}, {subset D' <= D} & A `<=` cover [set` D'] F. @@ -3579,7 +1885,8 @@ Lemma cvgi_close T' {F} {FF : ProperFilter F} (f : T' -> set T) (l l' : T) : {near F, is_fun f} -> f `@ F --> l -> f `@ F --> l' -> close l l'. Proof. move=> f_prop fFl fFl'. -suff f_totalfun: infer {near F, is_totalfun f} by exact: cvg_close fFl fFl'. +suff f_totalfun: {near F, is_totalfun f}. + by apply: cvg_close fFl fFl'; exact: fmapi_proper_filter. apply: filter_app f_prop; near do split=> //=. have: (f `@ F) setT by apply: fFl; apply: filterT. by rewrite fmapiE; apply: filterS => x [y []]; exists y. @@ -4596,7 +2903,7 @@ End uniformType1. Global Instance entourage_pfilter {M : puniformType} : ProperFilter (@entourage M). Proof. -apply Build_ProperFilter; last exact: entourage_filter. +apply Build_ProperFilter_ex; last exact: entourage_filter. by move=> A entA; exists (point, point); apply: entourage_refl. Qed. @@ -5362,10 +3669,10 @@ Proof. by move/cvgi_ballP. Qed. End pseudoMetricType_numDomainType. -Global Instance entourage_proper_filter {R : numDomainType} {M : pseudoPMetricType R} : - ProperFilter (@entourage M). +Global Instance entourage_proper_filter {R : numDomainType} + {M : pseudoPMetricType R} : ProperFilter (@entourage M). Proof. -apply: Build_ProperFilter; rewrite -entourage_ballE => A [_/posnumP[e] sbeA]. +apply: Build_ProperFilter_ex; rewrite -entourage_ballE => A [_/posnumP[e] sbeA]. by exists (point, point); apply: sbeA; apply: ballxx. Qed. @@ -5961,7 +4268,7 @@ Qed. Global Instance Proper_dnbhs_regular_numFieldType (R : numFieldType) (x : R^o) : ProperFilter x^'. Proof. -apply: Build_ProperFilter => A /nbhs_ballP[_/posnumP[e] Ae]. +apply: Build_ProperFilter_ex => A /nbhs_ballP[_/posnumP[e] Ae]. exists (x + e%:num / 2)%R; apply: Ae; last first. by rewrite eq_sym addrC -subr_eq subrr eq_sym. rewrite /ball /= opprD addrA subrr distrC subr0 ger0_norm //. @@ -5971,7 +4278,7 @@ Qed. Global Instance Proper_dnbhs_numFieldType (R : numFieldType) (x : R) : ProperFilter x^'. Proof. -apply: Build_ProperFilter => A /nbhs_ballP[_/posnumP[e] Ae]. +apply: Build_ProperFilter_ex => A /nbhs_ballP[_/posnumP[e] Ae]. exists (x + e%:num / 2)%R; apply: Ae; last first. by rewrite eq_sym addrC -subr_eq subrr eq_sym. rewrite /ball /= opprD addrA subrr distrC subr0 ger0_norm //. @@ -6697,7 +5004,6 @@ by move=> ?; exists (P, Q). Qed. End SubspaceOpen. - Lemma compact_subspaceIP (U : set T) : compact (U `&` A : set (subspace A)) <-> compact (U `&` A : set T). Proof.