Qcert.Basic.TypeSystem.RSubtypeProp

Section subtype.

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

Lemma top_subtype z : ⊤ <: z → z = ⊤.

Lemma subtype_bottom z : z <: ⊥ → z = ⊥.

Instance subtype_trans : Transitive subtype.

Global Instance subtype_pre : PreOrder subtype.

Lemma Rec_subtype_cons_weaken k s r l₁ pf pf2:
  Rec k ((s , r ) :: l₁) pf <: Rec Open l₁ pf2.

Lemma Rec_subtype_cons_inv2 {k1 k2 s r l₁ l₂ pf pf2}:
  Rec k1 l₁ pf <: Rec k2 ((s , r ) :: l₂) pf2 →
       ∃ pf',
         Rec k1 l₁ pf <: Rec Open l₂ pf'.

Lemma Rec_subtype_cons_inv1_open {k1 k2 s r l₁ l₂ pf pf2}:
  Rec k1 ((s , r ) :: l₁) pf <: Rec k2 l₂ pf2 →
     lookup string_dec l₂ s = None →
     k2 = Open.

Lemma Rec_subtype_cons_inv1 {k1 k2 s r l₁ l₂ pf pf2}:
  Rec k1 ((s , r ) :: l₁) pf <: Rec k2 l₂ pf2 →
    lookup string_dec l₂ s = None →
       ∃ pf',
         Rec k1 l₁ pf' <: Rec Open l₂ pf2.

Note that unlike the biased inverses, since we are removing an element from both sides, it is possible for k2 to be Closed

Lemma Rec_subtype_cons_inv {k1 k2 s r1 r2 l₁ l₂ pf pf2}:
  Rec k1 ((s , r1 ) :: l₁) pf <: Rec k2 ((s , r2 ) :: l₂) pf2 →
  ∃ pf' pf2',
    Rec k1 l₁ pf' <: Rec k2 l₂ pf2'.

Global Instance subtype_part : PartialOrder eq subtype.

Lemma wf_rtype_subtype_refl τ pf1 pf2:
  exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) τ pf1 <:
  exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) τ pf2.

Lemma Rec_subtype_cons_eq {k₁ k₂ s r₁ r₂ rl₁ rl₂ pf1 pf2} :
      Rec k₁ ((s , r₁ ) :: rl₁) pf1 <: Rec k₂ ((s , r₂ ) :: rl₂) pf2 →
                                  r₁ <: r₂.

Lemma STop₀ pf τ : τ <: exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) ⊤₀ pf.

Lemma SBottom₀ pf τ : exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) ⊥₀ pf <: τ.

Lemma SRefl₀ τ₀ pf : exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) τ ₀ pf <: exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) τ ₀ pf.

Lemma SColl₀ τ₁ pf₁ τ₂ pf₂ :
   exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) τ ₁ pf₁ <: exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) τ ₂ pf₂ →
   exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) (Coll₀ τ ₁) pf₁ <: exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) (Coll₀ τ ₂) pf₂.

Lemma SRec₀ k1 rl1 rl2 k2 pf1 pf2 : (∀ s r' pf',
                      lookup string_dec rl2 s = Some r' →
                      ∃ r pf, lookup string_dec rl1 s = Some r ∧
                                   subtype (exist _ r pf) (exist _ r' pf')) →
                                    (k2 = Closed → k1 = Closed ∧
                                 (∀ s, In s (domain rl1) → In s (domain rl2))) →
exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) (Rec₀ k1 rl1) pf1 <:
exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ ₀ = true) (Rec₀ k2 rl2) pf2.

Lemma subtype_Rec_sublist {k₁ l₁ pf₁ k₂ l₂ pf₂} :
  Rec k₁ l₁ pf₁ <: Rec k₂ l₂ pf₂ → sublist (domain l₂) (domain l₁).

Lemma subtype_Rec_closed_domain {k₁ l₁ pf₁ l₂ pf₂} :
  Rec k₁ l₁ pf₁ <: Rec Closed l₂ pf₂ → (domain l₂ ) = (domain l₁ ).

Lemma subtype_Rec_closed2_closed1 {k1 l1 pf1 l2 pf2}:
  Rec k1 l1 pf1 <: Rec Closed l2 pf2 →
                   k1 = Closed.

  Lemma is_list_sorted_in_cons_lookup_none {B} {b τ₃ s} (τ₁:B) {rl0 rl1 τ₀} (τ₂:B)
   (pf1 : is_list_sorted ODT_lt_dec (domain ((b , τ ₃ ) :: rl1)) = true)
   (x : is_list_sorted ODT_lt_dec (domain ((s , τ ₁ ) :: rl0)) = true)
   (inn:In (b , τ ₀ ) rl0) :
    lookup string_dec ((b , τ ₂ ) :: rl1) s = None.

  Lemma Rec_subtype_In {rl0 pf0 rl1 pf1 b τ₁ τ₂} :
   Rec Open rl0 pf0 <:
   Rec Open rl1 pf1 →
   In (b , τ ₁ ) rl0 → In (b , τ ₂ ) rl1 → τ ₁ <: τ ₂.

End subtype.