Qcert.Basic.TypeSystem.TBrandModelProp

Section TBrandModelProp.



  Context {ftype:foreign_type}.
  Context {m:brand_model}.

  Lemma sub_brand_in {b0 b τbrand} :
    sub_brand brand_relation_brands b0 b →
    In (b, τbrand) brand_context_types →
    ∃ τ₂,
      In (b0, τ₂) brand_context_types ∧
      subtype τ₂ τbrand.

  Definition brands_type_list (b:brands) : (list rtype)
    := flat_map (fun bb ⇒
                   match lookup string_dec brand_context_types bb with
                     | Some τ ⇒ (τ::nil)
                     | None ⇒ nil
                   end) b.

  Definition brands_type (b:brands) : rtype
    := fold_left meet (brands_type_list b) ⊤ .

  Lemma brands_type_singleton (bb:brand)
  : brands_type (singleton bb) =
    match lookup string_dec brand_context_types bb with
      | Some τ ⇒ τ
      | None ⇒ ⊤
    end.

  Lemma brands_type_list_app b1 b2 :
    brands_type_list (b1 ++ b2) = brands_type_list b1 ++ brands_type_list b2.

  Lemma brands_type_alt (b :brands) :
    brands_type b = fold_right meet ⊤ (brands_type_list b).


  Global Instance brands_type_sub_proper :
    Proper (sub_brands brand_relation_brands ==> subtype) brands_type.

  Lemma brands_type_sub_part bb τ b :
    lookup string_dec brand_context_types bb = Some τ →
    In bb b →
    brands_type b <: τ.

  Lemma brands_type_of_canon b :
    brands_type (canon_brands brand_relation_brands b) = brands_type b.

End TBrandModelProp.