Library Subsumption

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

Lemma sub_refl U : U >= U.
exists OMEGA ; destruct U ; simpl ; auto.
Qed.

Lemma sub_trans U V W : U >= V -> V >= W -> U >= W.
intros [V' teV] [W' teW].
exists (V' * W').
rewrite teV, teW ; eauto.
Qed.

Hint Resolve sub_refl sub_trans.

Instance sub_preorder : PreOrder subsumes.
constructor ; hnf ; eauto.
Qed.

Lemma sub_equiv U V : U == V <-> (U >= V /\ V >= U).
split.
- intros H ; split ;
    exists OMEGA ; eauto.
- intros [[V' teV] [U' teU]].
  assert (U == U * (U' * V')) by eauto.
  assert (eint : U' * V' = OMEGA) by eauto.
  destruct (int_eq_O _ _ eint).
  subst ; eauto.
Qed.

Lemma sub_int U V : (U * V) >= U.
exists V ; auto. Qed.

Lemma sub_O U : U >= OMEGA.
exists U ; auto. Qed.

Lemma sub_Int_L A B : A o B >= A.
exists B ; auto. Qed.

Lemma sub_Int_R A B : A o B >= B.
exists A ; eauto. Qed.

Lemma sub_comp_int U U' V V' : U >= U' -> V >= V' -> U * V >= U' * V'.
intros [U'' teU] [V'' teV].
exists (U'' * V'').
rewrite teU, teV, ! te_assoc_int.
apply te_comp_int ;
eauto.
Qed.

Hint Resolve sub_int sub_O sub_comp_int.

Instance sub_proper : Proper (subsumes ==> subsumes ==> subsumes) int.
repeat (hnf ; intro) ; eauto.
Qed.

Instance te_sub : Proper (type_equiv ==> type_equiv ==> impl)
                                  subsumes.
intros U U' eU V V' eV [V'' leV'].
exists V''. eauto. Qed.

Lemma sub_inv_A {U A} : U >= A -> exists B, U = B.
intros [V H].
destruct V ; simpl in * ; eauto using te_inv_A.
Qed.

Lemma sub_inv_O {U} : OMEGA >= U -> U = OMEGA.
destruct U ; auto.
intros e.
destruct (sub_inv_A e) as [B e'].
discriminate.
Qed.

Lemma sub_inv {F U} : F >= U -> (F:type) = U \/ OMEGA = U.
destruct 1 as [U' te].
assert (U * U' = F) by eauto using te_inv_F.
destruct U, U' ; simpl in * ; auto.
Qed.

Lemma sub_inv_F_G {F G} : F >= G -> G = F.
intros le.
destruct (sub_inv le) as [E|E] ; congruence.
Qed.

Inductive includes : type -> basetype -> Prop :=
| includesDropL A B F : includes B F -> includes (A o B) F
| includesDropR A B F : includes A F -> includes (A o B) F
| includesF F : includes F F
.

Hint Constructors includes.

Lemma te_inv_incl {U V} : U == V -> forall F, includes V F -> includes U F.
induction 1 ; intros G inG ; auto ; repeat (match goal with
 | [ H : includes (UpI (_ o _)) _ |- _ ] => inversion H ; clear H
 end) ; auto.
Qed.

Lemma incl_inv_sub {U F} : includes U F -> U >= F.
induction 1 ; auto.
- destruct IHincludes as [V p].
  change (A o B : type) with (A * B). exists (A * V).
  rewrite p. eauto.
- destruct IHincludes as [V p].
  change (A o B : type) with (A * B). exists (B * V).
  rewrite p. eauto.
Qed.

Lemma sub_inv_int {A B F} : A o B >= F -> A >= F \/ B >= F.
intros [V' E].
assert (H : includes (A o B) F).
{ apply (te_inv_incl E). destruct V' ; simpl ; eauto. }
inversion H ; eauto using incl_inv_sub.
Qed.