Qcert.Basic.TypeSystem.RConsistentSubtype




Section RConsistentSubtype.

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


Section rtype_join_meet.

  Lemma consistent_rtype_join_meet1:
    ∀ a b, subtype a b →
                rtype_join a b = b
                ∧ rtype_meet a b = a.

Corollary consistent_rtype_join1:
    ∀ a b, subtype a b → rtype_join a b = b.

Corollary consistent_rtype_meet1:
    ∀ a b, subtype a b → rtype_meet a b = a.

Lemma consistent_rtype_join_meet2:
  ∀ a b, (rtype_join a b = b → subtype a b)
               ∧ (rtype_meet a b = a → subtype a b).

Corollary consistent_rtype_join2:
  ∀ a b, rtype_join a b = b → subtype a b.

Corollary consistent_rtype_meet2:
  ∀ a b, rtype_meet a b = a → subtype a b.

Theorem consistent_rtype_join: ∀ a b, subtype a b ↔ rtype_join a b = b.

  Lemma rtype_join_subtype_l a b: subtype a (rtype_join a b).

  Lemma rtype_join_subtype_r a b: subtype b (rtype_join a b).

  Theorem rtype_join_least {a b c} : a <: c → b <: c → rtype_join a b <: c.

We can compute if the subtype relation holds using its relationship with rtype_join and the computable equality of types
  Theorem subtype_dec_rtype_join a b : {a <: b} + {¬ a <: b}.

  Theorem consistent_rtype_meet : ∀ a b, subtype a b ↔ rtype_meet a b = a.

  Lemma rtype_meet_subtype_l a b: subtype (rtype_meet a b) a.

  Lemma rtype_meet_subtype_r a b: subtype (rtype_meet a b) b.

  Theorem rtype_meet_most {a b c} : a <: b → a <: c → a <: (rtype_meet b c).

We can compute if the subtype relation holds using its relationship with rtype_meet and the computable equality of types
  Theorem subtype_dec_rtype_meet a b : {a <: b} + {¬ a <: b}.

End rtype_join_meet.

Theorem rtype_join_absorptive: ∀ a b, rtype_join a (rtype_meet a b) = a.

Theorem rtype_meet_absorptive: ∀ a b, rtype_meet a (rtype_join a b) = a.

End RConsistentSubtype.