Qcert.Basic.TypeSystem.RSubtype

Section subtype.

  Context {ftype:foreign_type}.
  Context {br:brand_relation}.

Inductive subtype : rtype → rtype → Prop :=
  | STop r : subtype r ⊤
  | SBottom r : subtype ⊥ r
  | SRefl r : subtype r r
  | SColl r1 r2 : subtype r1 r2 → subtype (Coll r1) (Coll r2)

Allow width subtyping of open records and depth subtyping of both types of records. Also, a closed record can be a subtype of an open record (but not vice versa)

  | SRec k1 k2 rl1 rl2 pf1 pf2 : (∀ s r',
                      lookup string_dec rl2 s = Some r' →
                      ∃ r, lookup string_dec rl1 s = Some r ∧
                                subtype r r') →
                                (k2 = Closed → k1 = Closed ∧
                                 (∀ s, In s (domain rl1) → In s (domain rl2))) →
                                subtype (Rec k1 rl1 pf1) (Rec k2 rl2 pf2)
  | SEither l1 l2 r1 r2 :
      subtype l1 l2 →
      subtype r1 r2 →
      subtype (Either l1 r1) (Either l2 r2)
  | SArrow in1 in2 out1 out2:
      subtype in2 in1 →
      subtype out1 out2 →
      subtype (Arrow in1 out1) (Arrow in2 out2)
  | SBrand b1 b2 : sub_brands brand_relation_brands b1 b2 → subtype (Brand b1) (Brand b2)
  | SForeign ft1 ft2 :
      foreign_type_sub ft1 ft2 →
      subtype (Foreign ft1) (Foreign ft2)
.

Lemma SRec_open k1 rl1 rl2 pf1 pf2 :
  (∀ s r',
     lookup string_dec rl2 s = Some r' →
     ∃ r, lookup string_dec rl1 s = Some r ∧
               subtype r r') →
  subtype (Rec k1 rl1 pf1) (Rec Open rl2 pf2).

Lemma SRec_closed_in_domain {k1 k2 rl1 rl2 pf1 pf2} :
  subtype (Rec k1 rl1 pf1) (Rec k2 rl2 pf2) →
  (∀ x, In x (domain rl2) → In x (domain rl1)).

Lemma SRec_closed_equiv_domain {k1 rl1 rl2 pf1 pf2} :
  subtype (Rec k1 rl1 pf1) (Rec Closed rl2 pf2) →
  (∀ x, In x (domain rl1) ↔ In x (domain rl2)).

  Lemma UIP_refl_dec
        {A:Type}
        (dec:∀ x y:A, {x = y } + {x ≠ y })
        {x:A}
        (p1:x = x) : p1 = eq_refl x.

This follows trivially from the consistency of join and subtype. However, this version should have better computational properties.

  Lemma subtype_both_dec x y :
    (prod ({subtype x y } + {¬ subtype x y }) ({subtype y x } + {¬ subtype y x })).

  Theorem subtype_dec x y : {subtype x y } + {¬ subtype x y }.

End subtype.

Lemma subtype_ext {ftype:foreign_type} {br:brand_relation} {a b pfa pfb} :
  subtype (exist _ a pfa) (exist _ b pfb) →
             ∀ pfa' pfb',
               subtype (exist _ a pfa') (exist _ b pfb').

Lemma subtype_Either_inv {ftype:foreign_type} {br:brand_relation} {τl τr τl' τr'} :
  subtype (Either τ l τ r) (Either τ l' τ r') →
  subtype τ l τ l' ∧
  subtype τ r τ r'.

Lemma subtype_Arrow_inv {ftype:foreign_type} {br:brand_relation} {τl τr τl' τr'} :
  subtype (Arrow τ l τ r) (Arrow τ l' τ r') →
  subtype τ l' τ l ∧
  subtype τ r τ r'.

Notation "r1 <: r2" := (subtype r1 r2) (at level 70).