Library Types

Properties of the typing relation

Require Export Contexts.
Implicit Types x y z : var.
Implicit Types F G H : basetype.
Implicit Types A B C : inttype.
Implicit Types U V W : type.
Implicit Types Gamma Delta : context.

Inversion properties

Lemma invtyVar n Gamma x A : ty n Gamma x A ->
  Gamma x >= A.
intros TY.
remember (x : term) as s.
remember (A : type) as U.
revert A HeqU x Heqs.
induction TY ;
  intros A' eU' x' ex' ; try discriminate ; try injection ex' ;
  intros ; subst ;
  intuition.
rewrite <- (e x'). simpl. eauto.
Qed.

Lemma invtyInt {n Gamma t U V} : ty n Gamma t (U * V) -> exists n1 n2 Gamma1 Gamma2,
  n = n1 + n2 /\ Gamma1 & Gamma2 ==1 Gamma /\ ty n1 Gamma1 t U /\ ty n2 Gamma2 t V.
destruct U as [A1|] ; [ destruct V as [A2|] |] ; simpl ; intros ty.
- inversion ty. eauto 9.
- eauto 10 using cint_Gamma_Empty, tyO.
- exists 0, n ; eauto 8 using cint_Empty_Gamma, tyO.
Qed.

Variables can be typed any way the resources permit

Lemma tyVarA n Gamma x A : Gamma x >= A -> ty n Gamma x A.
revert n Gamma ; induction A ; intros n Gamma e.
- eauto.
- change (A1 o A2 : type) with (A1 * A2) in e.
  destruct e as [U te].
  pose (Gamma' y := if decide (x = y) then (A1 : type) else OMEGA).
  pose (Delta' y := if decide (x = y) then A2 * U else Gamma y).
  change n with (0+n).
  apply tyInt with Gamma' Delta'.
  + apply IHA1. unfold Gamma' ; decide (x = x) ; auto.
  + apply IHA2. unfold Delta' ; decide (x = x) ; auto.
  + intros y. simpl. unfold Gamma', Delta'. decide (x = y) ; eauto.
Qed.

Lemma tyVarU n Gamma x U : Gamma x >= U -> ty n Gamma x U.
destruct U ; intros H.
- now apply tyVarA.
- now apply tyO.
Qed.

Typing is monotone in the resources in the context

Lemma tycsub {n Gamma t U} : ty n Gamma t U -> forall Gamma', Gamma' >=1 Gamma -> ty n Gamma' t U.
Proof with eauto 4 using csub_sub, csub_ext.
induction 1 ; intros Gamma' le...
- rewrite <- e in le.
  destruct (csplit le) as [Gamma'1 [Gamma'2 [P1 [P2 P3]]]].
  eauto.
- rewrite <- e in le.
  destruct (csplit le) as [Gamma'1 [Gamma'2 [P1 [P2 P3]]]].
  eauto.
Qed.

Instance cequi_typep {n} : Proper (cte ==> eq ==> eq ==> impl) (ty n).
intros Gamma Delta eq t1 t2 et U1 U2 eU tyG.
subst.
eapply tycsub ; eauto.
now apply cte_csub_equiv.
Qed.

Typing is monotone in the reduction bound

Lemma tymon {n Gamma t U} : ty n Gamma t U -> forall m, n <= m -> ty m Gamma t U.
induction 1 ; intros m' dm' ; eauto.
- replace m' with (S (m' - S m + m)) ; eauto.
- replace m' with (m' - m + m) ; eauto.
Qed.

Typing is anti-monotone for F-Types

Lemma ty_subsume {n Gamma t U} : ty n Gamma t U -> forall F, U >= F -> ty n Gamma t F.
Proof with eauto using csub_sub, csub_ext, tyVarU, tymon, tycsub, cte_csub_L, cte_csub_R.
induction 1 ; intros G le...
- rewrite (sub_inv_F_G le)...
- rewrite (sub_inv_F_G le). econstructor...
- destruct (sub_inv_int le) as [SA|SB]...
- rewrite (sub_inv_O le)...
Qed.

Typing is stable under point wise equality in the context

Lemma ty_equiv n Gamma s V : ty n Gamma s V -> forall Gamma', Gamma =1 Gamma' -> ty n Gamma' s V.
induction 1 ; intros Gamma' e' ; eauto.
Qed.

Typing is stable under Type Equivalence

Lemma equi_type {U V} : U == V -> forall {n Gamma t}, ty n Gamma t U -> ty n Gamma t V.
induction 1 ; eauto ; intros n Gamma t tys.
- inversion tys as [ | | | Gamma1 n1 ? Gamma2 n2 ? ? ty1 ty2 | ] ; subst.
  replace (n1 + n2) with (n2 + n1) by omega.
  econstructor ; eauto.
- inversion tys as [ | | | Gamma1 n1 ? Gamma2 n2 ? ? ty1 ty2 | ] ; subst.
  econstructor ; eauto.
- inversion tys as [ | | | Gamma12 n12 ? Gamma3 n3 ? ? ty12 ty3 ? E1 | ] ; subst.
  inversion ty12 as [ | | | Gamma1 n1 ? Gamma2 n2 ? ? ty1 ty2 ? E2 | ] ; subst.
  replace (n1 + n2 + n3) with (n1 + (n2 + n3)) by omega.
  econstructor ; eauto 3.
  rewrite <- E1, <- E2.
  intros x ; simpl ; eauto.
- inversion tys as [ | | | Gamma1 n1 ? Gamma23 n23 ? ? ty1 ty23 ? E1 | ] ; subst.
  inversion ty23 as [ | | | Gamma2 n2 ? Gamma3 n3 ? ? ty2 ty3 ? E2 | ] ; subst.
  replace (n1 + (n2 + n3)) with (n1 + n2 + n3) by omega.
  econstructor ; eauto 3.
  rewrite <- E1, <- E2.
  intros x ; simpl ; eauto.
Qed.

Instance equi_typep {n Gamma t} : Proper (type_equiv ==> impl) (ty n Gamma t).
intros U V eq.
unfold impl. now apply equi_type.
Qed.

Typing is anti-monotone for A-Types

Lemma tysubA {A B} : A >= B -> forall {n : nat} {Gamma t}, ty n Gamma t A -> ty n Gamma t B.
intros [V E] n Gamma t tytA.
rewrite E in tytA.
destruct V ; simpl in * ; auto.
inversion tytA ; eauto using tymon, tycsub, cte_csub_L.
Qed.