Module mathcomp.classical.filter

# 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 continuous f == f is continuous w.r.t the topology filterI_iter F n == nth stage of recursively building the filter of finite intersections of F finI_from D f == set of \bigcap_(i in E) f i where E is a finite subset of D ``` 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. \oo == "eventually" filter on nat: set of predicates on natural numbers that are eventually true 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=>`. - `near do tac` does `near=> x; tac; near: x` where `x` is a fresh variable