This file contains useful definitions and lemmas about the least upper bound (LUB) functions on Cedar types.

inductive Cedar.Thm.IsLubOfRecordTypes : List (Spec.Attr × Validation.Qualified Validation.CedarType) → List (Spec.Attr × Validation.Qualified Validation.CedarType) → List (Spec.Attr × Validation.Qualified Validation.CedarType) → Prop

• nil : IsLubOfRecordTypes [] [] []
• cons {a : Spec.Attr} {qty qty₁ qty₂ : Validation.Qualified Validation.CedarType} {rty rty₁ rty₂ : List (Spec.Attr × Validation.Qualified Validation.CedarType)} (h₁ : Validation.lubQualifiedType qty₁ qty₂ = some qty) (h₂ : IsLubOfRecordTypes rty rty₁ rty₂) : IsLubOfRecordTypes ((a, qty) :: rty) ((a, qty₁) :: rty₁) ((a, qty₂) :: rty₂)

theorem Cedar.Thm.lubRecordType_is_lub_of_record_types {rty rty₁ rty₂ : List (Spec.Attr × Validation.Qualified Validation.CedarType)} : Validation.lubRecordType rty₁ rty₂ = some rty → IsLubOfRecordTypes rty rty₁ rty₂

theorem Cedar.Thm.lubRecord_find_implies_find {a : Spec.Attr} {qty : Validation.QualifiedType} {rty rty₁ rty₂ : List (Spec.Attr × Validation.Qualified Validation.CedarType)} (h₁ : IsLubOfRecordTypes rty rty₁ rty₂) (h₂ : (Data.Map.mk rty).find? a = some qty) : ∃ (qty₁ : Validation.Qualified Validation.CedarType), ∃ (qty₂ : Validation.Qualified Validation.CedarType), (Data.Map.mk rty₁).find? a = some qty₁ ∧ (Data.Map.mk rty₂).find? a = some qty₂ ∧ Validation.lubQualifiedType qty₁ qty₂ = some qty

theorem Cedar.Thm.lubRecord_find_implied_by_find_left {a : Spec.Attr} {qty₁ : Validation.QualifiedType} {rty rty₁ rty₂ : List (Spec.Attr × Validation.Qualified Validation.CedarType)} (h₁ : IsLubOfRecordTypes rty rty₁ rty₂) (h₂ : (Data.Map.mk rty₁).find? a = some qty₁) : ∃ (qty : Validation.Qualified Validation.CedarType), ∃ (qty₂ : Validation.Qualified Validation.CedarType), (Data.Map.mk rty₂).find? a = some qty₂ ∧ (Data.Map.mk rty).find? a = some qty ∧ Validation.lubQualifiedType qty₁ qty₂ = some qty

theorem Cedar.Thm.lubRecord_contains_left {a : Spec.Attr} {rty rty₁ rty₂ : List (Spec.Attr × Validation.Qualified Validation.CedarType)} (h₁ : IsLubOfRecordTypes rty rty₁ rty₂) (h₂ : (Data.Map.mk rty₁).contains a = true) : (Data.Map.mk rty).contains a = true

theorem Cedar.Thm.lubRecord_find_implies_find_left {a : Spec.Attr} {qty : Validation.QualifiedType} {rty rty₁ rty₂ : List (Spec.Attr × Validation.Qualified Validation.CedarType)} (h₁ : IsLubOfRecordTypes rty rty₁ rty₂) (h₂ : (Data.Map.mk rty).find? a = some qty) : ∃ (qty₁ : Validation.Qualified Validation.CedarType), (Data.Map.mk rty₁).find? a = some qty₁ ∧ qty₁.isRequired = Validation.Qualified.isRequired qty

theorem Cedar.Thm.lubRecordType_nil_some {rty₁ rty₂ : List (Spec.Attr × Validation.QualifiedType)} : Validation.lubRecordType [] rty₁ = some rty₂ → rty₁ = [] ∧ rty₂ = []

theorem Cedar.Thm.lubBool_eq_ite {bty₁ bty₂ : Validation.BoolType} : Validation.lubBool bty₁ bty₂ = if bty₁ = bty₂ then bty₁ else Validation.BoolType.anyBool

theorem Cedar.Thm.lubBool_comm {bty₁ bty₂ : Validation.BoolType} : Validation.lubBool bty₁ bty₂ = Validation.lubBool bty₂ bty₁

theorem Cedar.Thm.lubQualified_comm {qty₁ qty₂ : Validation.Qualified Validation.CedarType} : Validation.lubQualifiedType qty₁ qty₂ = Validation.lubQualifiedType qty₂ qty₁

theorem Cedar.Thm.lubRecord_comm {rty₁ rty₂ : List (Spec.Attr × Validation.Qualified Validation.CedarType)} : Validation.lubRecordType rty₁ rty₂ = Validation.lubRecordType rty₂ rty₁

theorem Cedar.Thm.lub?_entity {ety₁ ety₂ : Spec.EntityType} : (Validation.CedarType.entity ety₁ ⊔ Validation.CedarType.entity ety₂) = if ety₁ = ety₂ then some (Validation.CedarType.entity ety₁) else none

theorem Cedar.Thm.lub_comm {ty₁ ty₂ : Validation.CedarType} : (ty₁ ⊔ ty₂) = (ty₂ ⊔ ty₁)

theorem Cedar.Thm.lub_refl (ty : Validation.CedarType) : (ty ⊔ ty) = some ty

theorem Cedar.Thm.lubRecordType_refl (rty : List (Spec.Attr × Validation.QualifiedType)) : Validation.lubRecordType rty rty = some rty

theorem Cedar.Thm.lubQualifiedType_refl (qty : Validation.QualifiedType) : Validation.lubQualifiedType qty qty = some qty

theorem Cedar.Thm.lubQualified_is_lub_of_getType {qty qty₁ qty₂ : Validation.Qualified Validation.CedarType} (h₁ : Validation.lubQualifiedType qty₁ qty₂ = some qty) : (qty₁.getType ⊔ qty₂.getType) = some qty.getType

theorem Cedar.Thm.lub_trans {ty₁ ty₂ ty₃ : Validation.CedarType} : (ty₁ ⊔ ty₂) = some ty₂ → (ty₂ ⊔ ty₃) = some ty₃ → (ty₁ ⊔ ty₃) = some ty₃

theorem Cedar.Thm.lubRecordType_trans {rty₁ rty₂ rty₃ : List (Spec.Attr × Validation.QualifiedType)} : Validation.lubRecordType rty₁ rty₂ = some rty₂ → Validation.lubRecordType rty₂ rty₃ = some rty₃ → Validation.lubRecordType rty₁ rty₃ = some rty₃

theorem Cedar.Thm.lubQualifiedType_trans {qty₁ qty₂ qty₃ : Validation.QualifiedType} : Validation.lubQualifiedType qty₁ qty₂ = some qty₂ → Validation.lubQualifiedType qty₂ qty₃ = some qty₃ → Validation.lubQualifiedType qty₁ qty₃ = some qty₃

theorem Cedar.Thm.subty_iff_lub?_eq_some {ty₁ ty₂ : Validation.CedarType} : (ty₁ ⊑ ty₂) = true ↔ (ty₁ ⊔ ty₂) = some ty₂

theorem Cedar.Thm.subty_trans {ty₁ ty₂ ty₃ : Validation.CedarType} : (ty₁ ⊑ ty₂) = true → (ty₂ ⊑ ty₃) = true → (ty₁ ⊑ ty₃) = true

theorem Cedar.Thm.lub_left_subty {ty₁ ty₂ ty₃ : Validation.CedarType} : (ty₁ ⊔ ty₂) = some ty₃ → (ty₁ ⊑ ty₃) = true

theorem Cedar.Thm.lubRecordType_left_subty {rty₁ rty₂ rty₃ : List (Spec.Attr × Validation.QualifiedType)} : Validation.lubRecordType rty₁ rty₂ = some rty₃ → Validation.lubRecordType rty₁ rty₃ = some rty₃

theorem Cedar.Thm.lubQualifiedType_left_subty {qty₁ qty₂ qty₃ : Validation.QualifiedType} : Validation.lubQualifiedType qty₁ qty₂ = some qty₃ → Validation.lubQualifiedType qty₁ qty₃ = some qty₃

theorem Cedar.Thm.sizeOf_qualified_lt_sizeOf_record_type (x : Spec.Attr × Validation.Qualified Validation.CedarType) (xs : List (Spec.Attr × Validation.Qualified Validation.CedarType)) : sizeOf x.snd < sizeOf (x :: xs)

theorem Cedar.Thm.lubBool_assoc_none_some {ty₁ ty₂ : Validation.CedarType} {bty₁ bty₂ : Validation.BoolType} (h₁ : (ty₁ ⊔ Validation.CedarType.bool bty₁) = none) (h₂ : some (Validation.CedarType.bool (Validation.lubBool bty₁ bty₂)) = some ty₂) : (ty₁ ⊔ ty₂) = none

theorem Cedar.Thm.lub_assoc_none_some {ty₁ ty₂ ty₃ ty₄ : Validation.CedarType} (h₁ : (ty₁ ⊔ ty₂) = none) (h₂ : (ty₂ ⊔ ty₃) = some ty₄) : (ty₁ ⊔ ty₄) = none

theorem Cedar.Thm.lubRecordType_assoc_none_some {rty₁ rty₂ rty₃ rty₄ : List (Spec.Attr × Validation.QualifiedType)} (h₁ : Validation.lubRecordType rty₁ rty₂ = none) (h₂ : Validation.lubRecordType rty₂ rty₃ = some rty₄) : Validation.lubRecordType rty₁ rty₄ = none

theorem Cedar.Thm.lubQualifiedType_assoc_none_some {qty₁ qty₂ qty₃ qty₄ : Validation.QualifiedType} (h₁ : Validation.lubQualifiedType qty₁ qty₂ = none) (h₂ : Validation.lubQualifiedType qty₂ qty₃ = some qty₄) : Validation.lubQualifiedType qty₁ qty₄ = none

theorem Cedar.Thm.lubBool_assoc_some_some {ty₄ ty₅ : Validation.CedarType} {bty₁ bty₂ bty₃ : Validation.BoolType} (h₁ : Validation.CedarType.bool (Validation.lubBool bty₁ bty₂) = ty₄) (h₂ : Validation.CedarType.bool (Validation.lubBool bty₂ bty₃) = ty₅) : (ty₄ ⊔ Validation.CedarType.bool bty₃) = (Validation.CedarType.bool bty₁ ⊔ ty₅)

theorem Cedar.Thm.lub_assoc_some_some {ty₁ ty₂ ty₃ ty₄ ty₅ : Validation.CedarType} (h₁ : (ty₁ ⊔ ty₂) = some ty₄) (h₂ : (ty₂ ⊔ ty₃) = some ty₅) : (ty₄ ⊔ ty₃) = (ty₁ ⊔ ty₅)

theorem Cedar.Thm.lubRecordType_assoc_some_some {rty₁ rty₂ rty₃ rty₄ rty₅ : List (Spec.Attr × Validation.QualifiedType)} (h₁ : Validation.lubRecordType rty₁ rty₂ = some rty₄) (h₂ : Validation.lubRecordType rty₂ rty₃ = some rty₅) : Validation.lubRecordType rty₄ rty₃ = Validation.lubRecordType rty₁ rty₅

theorem Cedar.Thm.lubQualifiedType_assoc_some_some {qty₁ qty₂ qty₃ qty₄ qty₅ : Validation.QualifiedType} (h₁ : Validation.lubQualifiedType qty₁ qty₂ = some qty₄) (h₂ : Validation.lubQualifiedType qty₂ qty₃ = some qty₅) : Validation.lubQualifiedType qty₄ qty₃ = Validation.lubQualifiedType qty₁ qty₅

theorem Cedar.Thm.lub_assoc (ty₁ ty₂ ty₃ : Validation.CedarType) : (do let ty₄ ← ty₁ ⊔ ty₂ ty₄ ⊔ ty₃) = do let ty₄ ← ty₂ ⊔ ty₃ ty₁ ⊔ ty₄

theorem Cedar.Thm.lub_lub_fixed {ty₁ ty₂ ty₃ ty₄ : Validation.CedarType} (h₁ : (ty₁ ⊔ ty₂) = some ty₃) (h₂ : (ty₃ ⊔ ty₄) = some ty₄) : (ty₁ ⊔ ty₄) = some ty₄

theorem Cedar.Thm.foldlM_of_lub_is_LUB {ty lubTy : Validation.CedarType} {tys : List Validation.CedarType} (h₁ : List.foldlM Validation.lub? ty tys = some lubTy) : (ty ⊔ lubTy) = some lubTy

theorem Cedar.Thm.foldlM_of_lub_assoc (ty₁ ty₂ : Validation.CedarType) (tys : List Validation.CedarType) : List.foldlM Validation.lub? ty₁ (ty₂ :: tys) = do let ty₃ ← List.foldlM Validation.lub? ty₂ tys ty₁ ⊔ ty₃