This file contains theorems related to TypedExpr.liftBoolTypes

theorem Cedar.Thm.type_of_after_lifted_is_lifted (x : Validation.TypedExpr) : x.liftBoolTypes.typeOf = x.typeOf.liftBoolTypes

theorem Cedar.Thm.type_lifting_preserves_expr (x : Validation.TypedExpr) : x.toExpr = x.liftBoolTypes.toExpr

theorem Cedar.Thm.type_lifting_preserves_evaluation_results {x : Validation.TypedExpr} {request : Spec.Request} {entities : Spec.Entities} : Spec.evaluate x.toExpr request entities = Spec.evaluate x.liftBoolTypes.toExpr request entities

inductive Cedar.Thm.Lifted : Validation.CedarType → Validation.CedarType → Prop

• bool {bty : Validation.BoolType} : Lifted (Validation.CedarType.bool bty) (Validation.CedarType.bool Validation.BoolType.anyBool)
• int : Lifted Validation.CedarType.int Validation.CedarType.int
• string : Lifted Validation.CedarType.string Validation.CedarType.string
• entity {ety : Spec.EntityType} : Lifted (Validation.CedarType.entity ety) (Validation.CedarType.entity ety)
• ext {extTy : Validation.ExtType} : Lifted (Validation.CedarType.ext extTy) (Validation.CedarType.ext extTy)
• set {ty₁ ty₂ : Validation.CedarType} (h : Lifted ty₁ ty₂) : Lifted ty₁.set ty₂.set
• record_nil : Lifted (Validation.CedarType.record (Data.Map.mk [])) (Validation.CedarType.record (Data.Map.mk []))
• record_fst_optional {ty₁ ty₂ : Validation.CedarType} {k : Spec.Attr} {m₁ m₂ : List (Spec.Attr × Validation.QualifiedType)} (h₁ : Lifted ty₁ ty₂) (h₂ : Lifted (Validation.CedarType.record (Data.Map.mk m₁)) (Validation.CedarType.record (Data.Map.mk m₂))) : Lifted (Validation.CedarType.record (Data.Map.mk ((k, Validation.Qualified.optional ty₁) :: m₁))) (Validation.CedarType.record (Data.Map.mk ((k, Validation.Qualified.optional ty₂) :: m₂)))
• record_fst_required {ty₁ ty₂ : Validation.CedarType} {k : Spec.Attr} {m₁ m₂ : List (Spec.Attr × Validation.QualifiedType)} (h₁ : Lifted ty₁ ty₂) (h₂ : Lifted (Validation.CedarType.record (Data.Map.mk m₁)) (Validation.CedarType.record (Data.Map.mk m₂))) : Lifted (Validation.CedarType.record (Data.Map.mk ((k, Validation.Qualified.required ty₁) :: m₁))) (Validation.CedarType.record (Data.Map.mk ((k, Validation.Qualified.required ty₂) :: m₂)))

theorem Cedar.Thm.lifted_record_is_lifted (m : List (Spec.Attr × Validation.QualifiedType)) : Lifted (Validation.CedarType.record (Data.Map.mk m)) (Validation.CedarType.record (Data.Map.mk (List.map (fun (x : Spec.Attr × Validation.QualifiedType) => match x with | (k, v) => (k, v.liftBoolTypes)) m)))

theorem Cedar.Thm.lifted_type_is_lifted (ty : Validation.CedarType) : Lifted ty ty.liftBoolTypes

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

theorem Cedar.Thm.lifted_record_type_is_top {r₁ r₂ : List (Spec.Attr × Validation.Qualified Validation.CedarType)} : IsLubOfRecordTypes r₂ r₁ r₂ → List.map (fun (x : Spec.Attr × Validation.Qualified Validation.CedarType) => match x with | (k, v) => (k, Validation.QualifiedType.liftBoolTypes v)) r₁ = List.map (fun (x : Spec.Attr × Validation.Qualified Validation.CedarType) => match x with | (k, v) => (k, Validation.QualifiedType.liftBoolTypes v)) r₂

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

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

theorem Cedar.Thm.type_lifting_preserves_instance_of_type {env : Validation.TypeEnv} {v : Spec.Value} {ty : Validation.CedarType} : InstanceOfType env v ty → InstanceOfType env v ty.liftBoolTypes

theorem Cedar.Thm.lift_bool_types_record_eq_map_on_values {rty : Data.Map Spec.Attr Validation.QualifiedType} : Validation.RecordType.liftBoolTypes rty = Data.Map.mapOnValues Validation.QualifiedType.liftBoolTypes rty

theorem Cedar.Thm.lift_bool_types_record_eq {rty : Data.Map Spec.Attr Validation.QualifiedType} : (Validation.CedarType.record rty).liftBoolTypes = Validation.CedarType.record (Validation.RecordType.liftBoolTypes rty)

theorem Cedar.Thm.wf_type_iff_wf_liftBoolTypes {env : Validation.TypeEnv} {ty : Validation.CedarType} : Validation.CedarType.WellFormed env ty ↔ Validation.CedarType.WellFormed env ty.liftBoolTypes