This file proves properties of the transitivity function in Cedar/SymCC/Enforcer.lean. #
theorem
Cedar.Thm.swf_implies_interpret_transitivity
{x₁ x₂ : Spec.Expr}
{t₁ t₂ : SymCC.Term}
{ety₁ ety₂ : Spec.EntityType}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
(heq : env ∼ SymCC.SymEnv.interpret I εnv)
(hI : I.WellFormed εnv.entities)
(hwε₁ : εnv.WellFormedFor x₁)
(hwε₂ : εnv.WellFormedFor x₂)
(hse₁ : env.StronglyWellFormedFor x₁)
(hse₂ : env.StronglyWellFormedFor x₂)
(hok₁ : SymCC.compile x₁ εnv = Except.ok t₁)
(hok₂ : SymCC.compile x₂ εnv = Except.ok t₂)
(hty₁ : t₁.typeOf = (SymCC.TermType.entity ety₁).option)
(hty₂ : t₂.typeOf = (SymCC.TermType.entity ety₂).option)
:
SymCC.Term.interpret I (SymCC.transitivity t₁ t₂ εnv.entities) = SymCC.Term.prim (SymCC.TermPrim.bool true)
theorem
Cedar.Thm.interpret_transitivity_implies_transitive
{uid₁ uid₂ uid₃ : Spec.EntityUID}
{t₁ t₂ : SymCC.Term}
{ts₁₂ ts₂₃ : Data.Set SymCC.Term}
{δ₁ δ₂ : SymCC.SymEntityData}
{f₁₂ f₂₃ : SymCC.UUF}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
(hwε : εnv.WellFormed)
(hI : I.WellFormed εnv.entities)
(hwt₁ : SymCC.Term.WellFormed εnv.entities t₁)
(hwt₂ : SymCC.Term.WellFormed εnv.entities t₂)
(ht₁ : SymCC.Term.interpret I t₁ = (SymCC.Term.entity uid₁).some)
(ht₂ : SymCC.Term.interpret I t₂ = (SymCC.Term.entity uid₂).some)
(hδ₁ : Data.Map.find? εnv.entities uid₁.ty = some δ₁)
(hf₁ : δ₁.ancestors.find? uid₂.ty = some (SymCC.UnaryFunction.uuf f₁₂))
(heq₁ :
SymCC.Factory.app (SymCC.UnaryFunction.interpret I (SymCC.UnaryFunction.uuf f₁₂)) (SymCC.Term.entity uid₁) = SymCC.Term.set ts₁₂ (SymCC.TermType.entity uid₂.ty))
(hin₁ : SymCC.Term.entity uid₂ ∈ ts₁₂)
(hδ₂ : Data.Map.find? εnv.entities uid₂.ty = some δ₂)
(hf₂ : δ₂.ancestors.find? uid₃.ty = some (SymCC.UnaryFunction.uuf f₂₃))
(heq₂ :
SymCC.Factory.app (SymCC.UnaryFunction.interpret I (SymCC.UnaryFunction.uuf f₂₃)) (SymCC.Term.entity uid₂) = SymCC.Term.set ts₂₃ (SymCC.TermType.entity uid₃.ty))
(hin₂ : SymCC.Term.entity uid₃ ∈ ts₂₃)
(htr : SymCC.Term.interpret I (SymCC.transitivity t₁ t₂ εnv.entities) = SymCC.Term.prim (SymCC.TermPrim.bool true))
:
∃ (f₁₃ : SymCC.UnaryFunction), ∃ (ts₁₃ : Data.Set SymCC.Term), δ₁.ancestors.find? uid₃.ty = some f₁₃ ∧ SymCC.Factory.app (SymCC.UnaryFunction.interpret I f₁₃) (SymCC.Term.entity uid₁) = SymCC.Term.set ts₁₃ (SymCC.TermType.entity uid₃.ty) ∧ SymCC.Term.entity uid₃ ∈ ts₁₃