This file proves properties of the acyclicity function in Cedar/SymCC/Enforcer.lean. #
theorem
Cedar.Thm.swf_implies_interpret_acyclicity
{x : Spec.Expr}
{t : SymCC.Term}
{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)
(hse : env.StronglyWellFormedFor x)
(hok : SymCC.compile x εnv = Except.ok t)
(hty : t.typeOf = (SymCC.TermType.entity ety).option)
:
theorem
Cedar.Thm.interpret_acyclicity_implies_acyclic
{t : SymCC.Term}
{ts : Data.Set SymCC.Term}
{uid : Spec.EntityUID}
{δ : SymCC.SymEntityData}
{f : SymCC.UUF}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
(hwε : εnv.WellFormed)
(hI : I.WellFormed εnv.entities)
(hwt : SymCC.Term.WellFormed εnv.entities t)
(hδ : Data.Map.find? εnv.entities uid.ty = some δ)
(hf : δ.ancestors.find? uid.ty = some (SymCC.UnaryFunction.uuf f))
(ht : SymCC.Term.interpret I t = (SymCC.Term.entity uid).some)
(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))
(ha : SymCC.Term.interpret I (SymCC.acyclicity t εnv.entities) = SymCC.Term.prim (SymCC.TermPrim.bool true))
: