Library Contexts

Lifting Type Equivalence and Subsumption to contexts

Require Export Subsumption.
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.

Subsumption on contexts is stronger than point wise Subsumption

Lemma csub_sub {Gamma Delta} : Gamma >=1 Delta -> forall x, Gamma x >= Delta x.
intros [Delta' cte] x.
exists (Delta' x).
now rewrite (cte x).
Qed.
Hint Resolve csub_sub.

Empty is neutral

Lemma cint_Empty_Gamma Gamma : Empty & Gamma =1 Gamma.
intros x ; reflexivity.
Qed.

Lemma cint_Gamma_Empty Gamma : Gamma & Empty =1 Gamma.
intros x ; eauto using int_comm_O.
Qed.

Empty is the kernel of intersection

Lemma cint_Empty Gamma Delta : Gamma & Delta =1 Empty -> Gamma =1 Empty /\ Delta =1 Empty.
intros e.
split ; intros y ; apply (int_eq_O _ _ (e y)).
Qed.

Intersection is commutative, associative, and compatible with point wise Type Equivalence

Lemma cte_comm_cint Gamma Delta : Gamma & Delta ==1 Delta & Gamma.
intros x. simpl ; eauto. Qed.

Lemma cte_assoc_cint Gamma Delta Epsilon : Gamma & (Delta & Epsilon ) ==1 (Gamma & Delta ) & Epsilon.
intros x ; simpl ; eauto. Qed.

Lemma cte_comp_cint Gamma Gamma' Delta Delta' : Gamma ==1 Gamma' -> Delta ==1 Delta' -> Gamma & Delta ==1 Gamma' & Delta'.
intros e1 e2 x ; simpl ; eauto. Qed.

Hint Resolve cte_assoc_cint cte_comm_cint.

Point wise Type Equivalence is an equivalence relation

Lemma cte_refl Gamma : Gamma ==1 Gamma.
intros x ; auto. Qed.

Lemma cte_pwr_refl Gamma Delta : Gamma =1 Delta -> Gamma ==1 Delta.
intros E x. now rewrite E.
Qed.

Lemma cte_sym Gamma Delta : Gamma ==1 Delta -> Delta ==1 Gamma.
intros e x ; auto. Qed.

Lemma cte_trans Gamma Delta Epsilon : Gamma ==1 Delta -> Delta ==1 Epsilon -> Gamma ==1 Epsilon.
intros e1 e2 x ; eauto. Qed.

Hint Resolve cte_refl cte_pwr_refl cte_sym cte_trans.

Instance cte_equivalence : Equivalence (cte).
constructor ; cbv ; eauto.
Qed.

Intersection is commutative with Subsumption on contexts

Lemma csub_comm Gamma Delta : Gamma & Delta >=1 Delta & Gamma.
exists Empty ; eauto. Qed.

Point wise intersection is compatible with point wise Type Equivalence

Instance cte_cint_proper : Proper (cte ==> cte ==> cte) cint.
repeat (hnf ; intros). simpl ; eauto.
Qed.

Point wise Type Equivalence is compatible with Subsumption on contexts

Instance cte_csub : Proper (cte ==> cte ==> impl) csub.
intros Gamma Gamma' eqG Delta Delta' eqD [Delta'' p].
exists Delta''. now rewrite <- eqG, p, eqD.
Qed.

Point wise Type Equivalence is the symmetric closure of Subsumption on contexts

Lemma cte_csub_equiv Gamma Delta : Gamma ==1 Delta <-> (Gamma >=1 Delta /\ Delta >=1 Gamma ).
split.
- split ; exists Empty ; intros x ; simpl ; eauto.
- intros [[D' PD] [G' PG]] x.
apply sub_equiv. split ; econstructor ; eauto.
Qed.

Point wise more resources implies Subsumption on contexts

Lemma cint_csub_l Gamma Delta : Gamma & Delta >=1 Gamma.
exists Delta ; auto.
Qed.

Lemma cint_csub_r {Gamma} Delta : Delta & Gamma >=1 Gamma.
exists Delta ; eauto.
Qed.

Lemma cte_csub_L {Gamma Delta Epsilon} : Gamma & Delta ==1 Epsilon -> Epsilon >=1 Gamma.
exists Delta ; eauto.
Qed.

Lemma cte_csub_R {Gamma Delta Epsilon} : Gamma & Delta ==1 Epsilon -> Epsilon >=1 Delta.
exists Gamma ; eauto.
Qed.

Point wise intersection is compatible with Subsumption on contexts

Lemma csub_cint_comp Gamma Gamma' Delta Delta' : Gamma >=1 Gamma' -> Delta >=1 Delta' -> Gamma & Delta >=1 Gamma' & Delta'.
intros [G' pG'] [D' pD'].
exists (G' & D').
rewrite pG', pD'. intros x ; simpl. rewrite ! te_assoc_int.
apply te_comp_int ; eauto.
Qed.

Hint Resolve csub_cint_comp.

Instance csub_cint_proper : Proper (csub ==> csub ==> csub) cint.
do 6 intro ; eauto.
Qed.

Contexts can be split

Lemma csplit {Gamma Delta1 Delta2} : Gamma >=1 Delta1 & Delta2 -> exists Gamma1 Gamma2, Gamma ==1 Gamma1 & Gamma2 /\ Gamma1 >=1 Delta1 /\ Gamma2 >=1 Delta2.
intros [Gamma' teGamma'].
exists Delta1, (Delta2 & Gamma').
unfold csub.
intuition ; eauto using cte_assoc_cint, cint_Gamma_Empty, cint_csub_l, cte_pwr_refl.
Qed.

Properties of context extension

Lemma csub_ext {Gamma Gamma'} : Gamma >=1 Gamma' -> forall U, U .: Gamma >=1 U .: Gamma'.
intros [G'' eq] U.
exists (OMEGA .: G'').
intros [|x] ; simpl ; eauto.
Qed.

Lemma feq_ext U V Gamma Gamma' : U = V -> Gamma =1 Gamma' -> U .: Gamma =1 V .: Gamma'.
intros eT eC [|x] ; eauto. Qed.

Lemma feq_ext_int U Gamma V V' Delta Delta' : U = V * V' -> Gamma =1 (Delta & Delta') -> U .: Gamma =1 (V .: Delta ) & (V' .: Delta').
intros eT eC [|x] ; eauto. Qed.

Hint Resolve feq_ext feq_ext_int.

Lemma cte_ext U V Gamma Gamma' : U == V -> Gamma ==1 Gamma' -> U .: Gamma ==1 V .: Gamma'.
intros eT eC [|x] ; eauto. Qed.

Lemma cte_ext_int U Gamma V V' Delta Delta' : U == V * V' -> Gamma ==1 (Delta & Delta') -> U .: Gamma ==1 (V .: Delta ) & (V' .: Delta').
intros eT eC [|x] ; eauto. Qed.

Hint Resolve cte_ext cte_ext_int cte_trans.

Properties of relations that are lifted to their point wise counterparts

Lemma feq_trans Gamma Delta Epsilon : Gamma =1 Delta -> Delta =1 Epsilon -> Gamma =1 Epsilon.
intros e1 e2 x ; congruence. Qed.

Lemma feq_eq Gamma Delta : Gamma = Delta -> Gamma =1 Delta.
now intros []. Qed.
Hint Resolve feq_eq feq_trans.

Lemma cte_eq Gamma Delta : Gamma = Delta -> Gamma ==1 Delta.
now intros []. Qed.
Hint Resolve cte_eq.

Dropping the first element and prepending it preserves point wise equality

Lemma cons_drop_inv Gamma : Gamma =1 (Gamma 0) .: drop 1 Gamma.
intros [|x] ; auto.
Qed.