# 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

}.

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.

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).

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

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

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.

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.

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

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