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 ``` 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=>.