Library Filters

Filters

Require Export Definitions.
Require Import Subsumption.
Require Import Setoid Morphisms.

Implicit Types Gamma Delta : context.

Implicit Types u v : inttype -> Prop.
Implicit Types m n : basetype -> Prop.

Implicit Types A B C : inttype.
Implicit Types F G H : basetype.

Intersection Filters

Record IFilter u := {
closed_int A B : u A -> u B -> u (A o B) ;
closed_leu A B : u A -> A >= B -> u B
}.

Closure of a set of F-Types

Inductive closure m : inttype -> Prop :=
| inF F : m F -> closure m F
| inI A B : closure m A -> closure m B -> closure m (A o B).

Closures are stable under Type Equivalence

Lemma equiv_closure {A B} : A == B -> forall m, closure m A -> closure m B.
intros te.
remember (A : type) as U.
remember (B : type) as V.
revert A B HeqU HeqV.
induction te ; intros AA BB eA eB m cA ; try injection eA ; try injection eB ; intros ; subst ; repeat
match goal with
| [ H : closure _ (_ o _) |- _ ] => inversion H ; subst ; clear H
end ; eauto using inF, inI.
Qed.

Closures are I-Filters

Lemma closure_filter m : IFilter (closure m).
constructor.
- now constructor.
- intros A B cA le.
  destruct le as [[B'|] H] ; simpl in * ; eauto 3 using equiv_closure.
  assert (cP := equiv_closure H _ cA).
  now inversion cP.
Qed.

Application of two I-Filters

Inductive app u v F : Prop :=
| inApp A : u (A --> F) -> v A -> app u v F.

Definition int_app u v := closure (app u v).
Infix "@" := int_app (at level 60).

If closures agree on A-Types, they also agree on F-Types

Lemma xe_closure m n : (forall A, closure m A -> closure n A) -> forall F, m F -> n F.
intros xec F mF.
specialize (xec F (inF _ _ mF)).
now inversion xec.
Qed.

If filters agree on F-Types, they also agree on A-Types

Lemma filter_ind_filter u v : IFilter u -> IFilter v -> (forall F, u F -> v F) -> forall A, u A -> v A.
intros uF vF B.
induction A ; intros uA ; auto.
apply vF.
+ apply IHA1. eapply uF ; eauto using sub_Int_L.
+ apply IHA2. eapply uF ; eauto using sub_Int_R.
Qed.

Two filters are equivalent if they contain the same A-Types

Definition filter_equiv u v := forall A, u A <-> v A.

Infix "~" := filter_equiv (at level 70).

Filter equivalence is an equivalence relation

Lemma filter_equiv_refl {u} : u ~ u.
intros A. reflexivity. Qed.

Lemma filter_equiv_sym {u v} : u ~ v -> v ~ u.
intros e A. now symmetry. Qed.

Lemma filter_equiv_trans {u v w} : u ~ v -> v ~ w -> u ~ w.
intros e1 e2 A. now transitivity (v A). Qed.

Instance equiv_e : Equivalence filter_equiv.
constructor ; eauto using filter_equiv_refl, filter_equiv_sym, filter_equiv_trans. Qed.

Filters are preserved by equivalence

Lemma equiv_filter u v : IFilter u -> u ~ v -> IFilter v.
intros [F1 F2] e.
constructor.
- intros A B vA vB. apply e. apply F1 ; now apply e.
- intros A B vA le. apply e. apply F2 with A ; auto.
now apply e.
Qed.

If filters contain the same F-Types, they are equivalent

Lemma filter_filter_equiv u v : IFilter u -> IFilter v -> (forall F, u F -> v F) -> (forall F, v F -> u F) -> u ~ v.
intros uF vF H1 H2 A.
split ; apply filter_ind_filter ; auto.
Qed.

For closures, it suffices to consider the sets of F-Types

Lemma inclosure_F u m : (forall F, u F -> m F) -> (forall F, u F -> closure m F).
auto using inF.
Qed.

Lemma fromclosure_F u m : (forall F, m F -> u F) -> (forall F, closure m F -> u F).
intros B F cmF.
inversion cmF ; auto.
Qed.

A filter and a closure are equivalent if they contain the same F-Types

Lemma closure_filter_equiv u m : IFilter u -> (forall F, u F -> m F) -> (forall F, m F -> u F) -> u ~ closure m.
intros uF H1 H2.
apply filter_filter_equiv ; eauto using closure_filter, inclosure_F, (fromclosure_F u).
Qed.

Two closures are equivalent if their base sets contain the same F-Types

Lemma closure_closure_equiv n m : (forall F, n F -> m F) -> (forall F, m F -> n F) -> closure n ~ closure m.
intros H1 H2.
apply filter_filter_equiv ; eauto using closure_filter, (fromclosure_F (closure n)), (fromclosure_F (closure m)), inF.
Qed.

Filter application is compatible with filter equivalence

Lemma equiv_app_comp {u u'} : u ~ u' -> forall v v', v ~ v' -> u @ v ~ u' @ v'.
intros equivu v v' equivv.
apply closure_closure_equiv ;
intros F [A Hu Hv'] ; exists A ; auto ; now apply equivu || apply equivv.
Qed.

Instance equiv_comp_p : Proper (filter_equiv ==> filter_equiv ==> filter_equiv) int_app.
intros u u' equ v v' eqv.
eauto using equiv_app_comp. Qed.

The top filter contains all A-Types

Definition top A := True.

Lemma top_filter : IFilter top.
split ; eauto. Qed.

The bottom filter contains no A-Types

Definition bot A := False.

Lemma bot_filter : IFilter bot.
split ; eauto. Qed.

Hint Unfold top int_app.

If applied to a non-empty filter, the top filter produces itself

Lemma top_app {u} : (exists A, u A) -> top ~ top @ u.
intros [A uA].
apply closure_filter_equiv ; eauto using top_filter, inApp.
Qed.