Library Interpretation

Interpretation of terms as filters

Require Export Filters.
Require Import Contexts Types.

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 type context is a mapping from variables to sets of A-Types
Definition type_context := var -> inttype -> Prop.
Implicit Types rho : type_context.

rho is valid if it contains only filters. We only consider valid type contexts.

Definition valid rho := forall x, IFilter (rho x).

Extending with filters preserves validity
Lemma valid_up u rho : IFilter u -> valid rho -> valid (u .: rho).
intros f v [|x] ; eauto. Qed.

rho is compatible with Gamma if it contains all the A-Types in Gamma

Definition compatible rho Gamma := forall x A, Gamma x = A -> rho x A.

Extending consistently preserves compatibility
Lemma compatible_up u rho A Gamma : compatible rho Gamma -> u A -> compatible (u .: rho) ((A : type) .: Gamma).
intros c uA [|x] B ; simpl ; auto. Qed.

Dropping information preserves compatibility

Lemma compatible_down u rho Gamma : compatible (u .: rho) Gamma -> compatible rho (drop 1 Gamma).
intros c x A E.
apply (c (S x) A E). Qed.

The point wise intersection of two compatible contexts is also compatible
Lemma compatible_cint rho Gamma Delta : valid rho -> compatible rho Gamma -> compatible rho Delta -> compatible rho (Gamma & Delta).
intros v cG cD x A E.
simpl in *.
specialize (cG x).
specialize (cD x).
destruct (Gamma x) as [A1|] ; auto.
destruct (Delta x) as [A2|] ; simpl in * ; auto.
replace A with (A1 o A2) by congruence.
apply v ; auto.
Qed.

Type contexts are point wise stable under Subsumption
Lemma compatible_sub_Gamma rho Gamma : valid rho -> compatible rho Gamma -> forall x A, Gamma x >= A -> rho x A.
intros v cG x A E.
destruct (sub_inv_A E) as [B E'].
eapply v ; eauto.
now rewrite <- E'.
Qed.

Compatibility is stable under Subsumption on contexts

Lemma compatible_sub rho Gamma Delta : valid rho -> compatible rho Gamma -> Gamma >=1 Delta -> compatible rho Delta.
intros v cG de x A E.
eapply compatible_sub_Gamma ; eauto.
rewrite <- E ; eauto using csub_sub.
Qed.

The interpretation of a term under a type context is the set of A-Types that can be given to it under some compatible context
Inductive int_t rho t A : Prop :=
| intty (n : nat) Gamma : compatible rho Gamma -> ty n Gamma t A -> int_t rho t A.

Notation "'[' t ']' rho" := (int_t rho t) (at level 1).

The interpretation of a term is a filter
Lemma int_IF rho t : valid rho -> IFilter [t] rho.
split.
- intros A B [n Gamma ? ?] [m Delta ? ?].
  eauto using intty, compatible_cint.
- intros A B [n Gamma ? ?] le.
  eauto using intty, tysubA.
Qed.