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
Definition realizorCandidate := (inttype -> Prop) -> Prop.
Implicit Types X Y : realizorCandidate.

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.

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.

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.

Realizor Predicates are equivalent if they contain the same sets

Definition rp_equiv X Y := forall u, X u <-> Y u.

Infix "=R=" := rp_equiv (at level 55).

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.

Two maps are equivalent if the are pointwise equivalent

Definition pi_equiv M N := forall X, realizorPredicate X -> M X =R= N X.

If two maps are equivalent, so are their possible intersections

Instance int_equiv : Proper (pi_equiv ==> rp_equiv) possible_int.
intros M N eMN u.
split ; intros H [X PX] ; apply eMN ; auto.
Qed.