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 <[email protected]>

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

_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

classical/Make

@@ -17,4 +17,5 @@ cardinality.v
 fsbigop.v
 set_interval.v
 classical_orders.v
+filter.v
 all_classical.v

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.

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.