From TLC Require Import LibTactics.
From TLC Require Import LibLogic. (* defines [pred_incl] *)
From TLC Require Import LibSet. (* defines [set] *)
(* ---------------------------------------------------------------------------- *)
(* Technically, a filter is a nonempty set of nonempty subsets of A, which is
closed under inclusion and intersection. *)
Definition filter A := set (set A).
(* Intuitively, a filter is a modality. Let us write [ultimately] for a filter.
If [P] is a predicate, then [ultimately P] is a proposition. Technically,
this proposition asserts that [P] is an element of the filter; intuitively,
it means that [P] holds ``in the limit''. *)
Class Filter {A : Type} (ultimately : filter A) := {
(* A filter must be nonempty. *)
filter_nonempty:
exists P, ultimately P;
(* A filter does not have the empty set as a member. *)
filter_member_nonempty:
forall P, ultimately P ->
exists a, P a;
(* A filter is closed by inclusion and by intersection. *)
filter_closed_under_intersection:
forall P1 P2 P : set A,
ultimately P1 ->
ultimately P2 ->
(forall a, P1 a -> P2 a -> P a) ->
ultimately P
}.
(* ---------------------------------------------------------------------------- *)
(* Basic properties of filters. *)
Section Properties.
Context {A : Type} {ultimately : filter A} `{@Filter A ultimately}.
(* A filter is closed by subset inclusion. In other words, if [ultimately]
is a filter, then it is covariant. *)
Lemma filter_closed_under_inclusion:
forall P1 P2 : set A,
ultimately P1 ->
(forall a, P1 a -> P2 a) ->
ultimately P2.
Proof.
intros. eapply filter_closed_under_intersection; eauto.
Qed.
(* A filter is compatible with extensional equality: if [P1] and [P2] are
extensionally equal, then [ultimately P1] is equivalent to [ultimately
P2]. *)
Lemma filter_extensional:
forall P1 P2 : set A,
(forall a, P1 a <-> P2 a) ->
(ultimately P1 <-> ultimately P2).
Proof.
introv h. split; intros; eapply filter_closed_under_inclusion; eauto;
intros; eapply h; eauto.
Qed.
(* A filter always contains the universe as a member. In other words, if
[P] holds everywhere, then [ultimately P] holds. *)
Lemma filter_universe:
forall P : set A,
(forall a, P a) ->
ultimately P.
Proof.
(* A filter is nonempty, so it has one inhabitant. *)
destruct filter_nonempty.
(* A filter is closed by inclusion, so the universe is also
an inhabitant of the filter. *)
eauto using @filter_closed_under_inclusion.
Qed.
(* If [P] holds ultimately and is independent of its argument, then [P]
holds, period. *)
Lemma filter_const:
forall P : Prop,
ultimately (fun _ => P) ->
P.
Proof.
intros.
forwards [ a ? ]: filter_member_nonempty. eauto.
eauto.
Qed.
End Properties.
(* ---------------------------------------------------------------------------- *)
(* Inclusion of filters. *)
Notation finer ultimately1 ultimately2 :=
(pred_incl ultimately2 ultimately1).
Notation coarser ultimately1 ultimately2 :=
(pred_incl ultimately1 ultimately2).
(* These relations are reflexive and transitive; see [pred_incl_refl] and
[pred_incl_trans] in [LibLogic]. *)
(* ---------------------------------------------------------------------------- *)
(* Applying a function [f] to a filter [ultimately] produces another filter,
known as the image of [ultimately] under [f]. *)
Definition image {A} (ultimately : filter A) {B} (f : A -> B) : set (set B) :=
fun P => ultimately (fun x => P (f x)).
(* Make this a definition, not an instance, because we do not wish it to be
used during the automated search for instances. *)
Definition filter_image {A} ultimately `{Filter A ultimately} {B} (f : A -> B) :
Filter (image ultimately f).
Proof.
econstructor; unfold image.
(* There exists an element in this filter, namely the universe. *)
exists (fun (_ : B) => True). eauto using filter_universe.
(* No element of this filter is empty. *)
intros.
forwards [ a ? ]: filter_member_nonempty; eauto. simpl in *.
eauto.
(* This filter is stable under intersection. *)
introv h1 h2 ?.
eapply (filter_closed_under_intersection _ _ _ h1 h2).
eauto.
Qed.
(* ---------------------------------------------------------------------------- *)
(* A notion of limit, or convergence. *)
(* The definition of [limit] does not really need proofs that [ultimatelyA]
and [ultimatelyB] are filters. Requesting these proofs anyway is useful,
as it helps the implicit argument inference system. *)
Definition limit
{A} ultimatelyA `{Filter A ultimatelyA}
{B} ultimatelyB `{Filter B ultimatelyB}
(f : A -> B)
:=
coarser ultimatelyB (image ultimatelyA f).
Lemma limit_id:
forall A ultimately `{Filter A ultimately},
limit _ _ (fun a : A => a).
Proof.
unfold limit, image. repeat intro. eapply filter_closed_under_inclusion; eauto.
Qed.
(* ---------------------------------------------------------------------------- *)
(* The product of two filters. *)
Section FilterProduct.
Context {A1} ultimately1 `{Filter A1 ultimately1}.
Context {A2} ultimately2 `{Filter A2 ultimately2}.
Definition product : set (set (A1 * A2)) :=
fun P : set (A1 * A2) =>
exists P1 P2,
ultimately1 P1 /\ ultimately2 P2 /\
forall a1 a2, P1 a1 -> P2 a2 -> P (a1, a2).
Global Instance filter_product : Filter product.
Proof.
econstructor; unfold product.
(* Existence of a member. *)
destruct (@filter_nonempty _ ultimately1) as [ P1 ? ]. eauto.
destruct (@filter_nonempty _ ultimately2) as [ P2 ? ]. eauto.
exists (fun a : A1 * A2 => let (a1, a2) := a in P1 a1 /\ P2 a2) P1 P2.
eauto.
(* Nonemptiness of the members. *)
introv [ P1 [ P2 [ ? [ ? ? ]]]].
forwards [ a1 ? ]: (filter_member_nonempty P1). eauto.
forwards [ a2 ? ]: (filter_member_nonempty P2). eauto.
exists (a1, a2). eauto.
(* Closure under intersection and inclusion. *)
intros P Q R.
introv [ P1 [ P2 [ ? [ ? ? ]]]].
introv [ Q1 [ Q2 [ ? [ ? ? ]]]].
intros.
exists (fun a1 => P1 a1 /\ Q1 a1).
exists (fun a2 => P2 a2 /\ Q2 a2).
repeat split.
eapply filter_closed_under_intersection. 3: eauto. eauto. eauto.
eapply filter_closed_under_intersection. 3: eauto. eauto. eauto.
intuition eauto.
Qed.
(* When the pair [a1, a2] goes to infinity, its components go to infinity. *)
Lemma limit_fst:
limit _ _ (@fst A1 A2).
Proof.
unfold limit, image, product. simpl.
intros P1 ?.
exists P1 (fun _ : A2 => True).
repeat split.
eauto.
eapply filter_universe. eauto.
eauto.
Qed.
Lemma limit_snd:
limit _ _ (@snd A1 A2).
Proof.
unfold limit, image, product. simpl.
intros P2 ?.
exists (fun _ : A1 => True) P2.
repeat split.
eapply filter_universe. eauto.
eauto.
eauto.
Qed.
(* When both components go to infinity, the pair goes to infinity. *)
(* The limit of a pair is a pair of the limits. *)
Lemma limit_pair :
forall A ultimately `{@Filter A ultimately},
forall (f1 : A -> A1) (f2 : A -> A2),
limit _ _ f1 ->
limit _ _ f2 ->
limit _ _ (fun a => (f1 a, f2 a)).
Proof.
unfold limit, image.
introv ? h1 h2. intros P [ P1 [ P2 [ ? [ ? ? ]]]].
eapply filter_closed_under_intersection.
eapply h1. eauto.
eapply h2. eauto.
eauto.
Qed.
End FilterProduct.