Library RealizorPredicates
Realizor Predicates
Require Export Premodel.
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.
Implicit Types x y z : var.
Implicit Types s t : term.
A Realizor Candidate is a set of A-Types
A Realizor Predicate is
- a set of I-Filters,
- which is closed under equivalence,
- contains the top filter,
- and (constructively) excludes the bottom filter
Record realizorPredicate X : Prop := realizor {
excl_bot u : X u -> (exists A, u A) ;
incl_top : X top;
only_filter u : X u -> IFilter u ;
equiv_closed u v : u ~ v -> X u -> X v
}.
Existing Class realizorPredicate.
Instance equiv_rp_p X (rpX : realizorPredicate X) : Proper (filter_equiv ==> iff) X.
split ; apply (equiv_closed X) ; auto using filter_equiv_sym. Qed.
excl_bot u : X u -> (exists A, u A) ;
incl_top : X top;
only_filter u : X u -> IFilter u ;
equiv_closed u v : u ~ v -> X u -> X v
}.
Existing Class realizorPredicate.
Instance equiv_rp_p X (rpX : realizorPredicate X) : Proper (filter_equiv ==> iff) X.
split ; apply (equiv_closed X) ; auto using filter_equiv_sym. Qed.
The intersection of Realizor Predicates is a Realizor Predicate
Definition intersect I (X : I -> realizorCandidate) : realizorCandidate := fun u => forall i : I, X i u.
Lemma intersect_realizable I (X : I -> realizorCandidate) : inhabited I -> (forall i : I, realizorPredicate (X i)) -> realizorPredicate (intersect I X).
intros inh rpI. constructor.
- intros u Xu. destruct inh as [i]. now apply (rpI i).
- intros i. apply (rpI i).
- intros u Xu. destruct inh as [i]. now apply (rpI i).
- intros u v equv Xu i. now rewrite <- equv.
Qed.
The functional product of two Realizor Predicates is a Realizor Predicate
Definition prod X Y : realizorCandidate := fun u => IFilter u /\ forall v, X v -> Y (u @ v).
Lemma prod_realizable X Y : realizorPredicate X -> realizorPredicate Y -> realizorPredicate (prod X Y).
intros rpX rpY. split.
- intros u produ.
destruct (rpY.(excl_bot _) (u @ top)) as [B clB].
+ apply produ ; eauto using incl_top.
apply rpX.
+ induction clB as [F C|] ; eauto.
destruct C as [A uAF _]; eauto.
- constructor ; auto using top_filter.
intros u Xu.
assert (exists A, u A) by now apply rpX.
rewrite <- top_app ; auto.
apply rpY.
- intros u [H ?] ; auto.
- intros u v equv [uF produ].
constructor ; eauto using equiv_filter.
intros v' Xv'.
rewrite <- equv.
auto.
Qed.
The set containing only top is a Realizor Predicate
Definition top_rp u := u ~ top.
Lemma top_rp_realizable : realizorPredicate top_rp.
constructor ; unfold top_rp ; eauto using filter_equiv_refl, filter_equiv_trans, filter_equiv_sym, equiv_filter, top_filter.
intros u equiv. exists (BASE 0). now apply equiv.
Qed.
Lemma top_rp_realizable : realizorPredicate top_rp.
constructor ; unfold top_rp ; eauto using filter_equiv_refl, filter_equiv_trans, filter_equiv_sym, equiv_filter, top_filter.
intros u equiv. exists (BASE 0). now apply equiv.
Qed.
If the map M maps Realizor Predicates to
Realizor Predicates, its possible intersection
(the intersection of all Realizor Predicates mapped under M)
is a Realizor Predicate
Definition possible_int (M : realizorCandidate -> realizorCandidate) : realizorCandidate :=
intersect { X | realizorPredicate X } (fun P => M (proj1_sig P)).
Lemma possible_int_realizable M : (forall X, realizorPredicate X -> realizorPredicate (M X)) -> realizorPredicate (possible_int M).
intros H. apply intersect_realizable.
constructor. exists top_rp ; auto using top_rp_realizable.
intros [X HX] ; simpl. auto. Qed.
Lemma possible_int_specialize {P' u} : possible_int P' u -> forall X, realizorPredicate X -> (P' X) u.
intros ipu X HX.
apply (ipu (exist _ X HX)). Qed.
intersect { X | realizorPredicate X } (fun P => M (proj1_sig P)).
Lemma possible_int_realizable M : (forall X, realizorPredicate X -> realizorPredicate (M X)) -> realizorPredicate (possible_int M).
intros H. apply intersect_realizable.
constructor. exists top_rp ; auto using top_rp_realizable.
intros [X HX] ; simpl. auto. Qed.
Lemma possible_int_specialize {P' u} : possible_int P' u -> forall X, realizorPredicate X -> (P' X) u.
intros ipu X HX.
apply (ipu (exist _ X HX)). Qed.
Realizor Predicates are equivalent if they contain the same sets
Realizor Predicate Equivalence is an equivalence relation
Instance rpe : Equivalence rp_equiv.
constructor.
- intros X u. reflexivity.
- intros X Y E u. now symmetry.
- intros X Y Z EXY EYZ u. now transitivity (Y u).
Qed.
The functional product is compatible with equivalence
Instance prod_equiv : Proper (rp_equiv ==> rp_equiv ==> rp_equiv) prod.
intros X1 X2 eX Y1 Y2 eY.
intros u.
split ; intros [uF HY] ; constructor ; auto ; intros v HX ; apply eY, HY, eX, HX.
Qed.
intros X1 X2 eX Y1 Y2 eY.
intros u.
split ; intros [uF HY] ; constructor ; auto ; intros v HX ; apply eY, HY, eX, HX.
Qed.
Two maps are equivalent if the are pointwise equivalent
If two maps are equivalent, so are their possible intersections