This file proves properties of the footprints function in Cedar/SymCC/Enforcer.lean.

def Cedar.SymCC.SymEntities.SameOn (εs : SymEntities) (ft : Data.Set Term) (I₁ I₂ : Interpretation) : Prop

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.SymEnv.SameOn (εnv : SymEnv) (ft : Data.Set Term) (I₁ I₂ : Interpretation) : Prop

Equations

• εnv.SameOn ft I₁ I₂ = (Cedar.SymCC.SymRequest.interpret I₁ εnv.request = Cedar.SymCC.SymRequest.interpret I₂ εnv.request ∧ εnv.entities.SameOn ft I₁ I₂)

theorem Cedar.Thm.mem_footprints_iff {xs : List Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} : t ∈ SymCC.footprints xs εnv ↔ ∃ (x : Spec.Expr), x ∈ xs ∧ t ∈ SymCC.footprint x εnv

theorem Cedar.Thm.mem_footprint_option_entity {x : Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} : t ∈ SymCC.footprint x εnv → ∃ (ety : Spec.EntityType), t.typeOf = (SymCC.TermType.entity ety).option

theorem Cedar.Thm.mem_footprint_exists_wf {x : Spec.Expr} {tₑ : SymCC.Term} {env : Spec.Env} {εnv : SymCC.SymEnv} : εnv.WellFormedFor x → env.WellFormedFor x → tₑ ∈ SymCC.footprint x εnv → ∃ (xₑ : Spec.Expr), εnv.WellFormedFor xₑ ∧ env.WellFormedFor xₑ ∧ SymCC.compile xₑ εnv = Except.ok tₑ

theorem Cedar.Thm.mem_footprint_compile_exists_swf {x : Spec.Expr} {tₑ : SymCC.Term} {env : Spec.Env} {εnv : SymCC.SymEnv} : εnv.StronglyWellFormedFor x → env.StronglyWellFormedFor x → tₑ ∈ SymCC.footprint x εnv → ∃ (xₑ : Spec.Expr), εnv.StronglyWellFormedFor xₑ ∧ env.StronglyWellFormedFor xₑ ∧ SymCC.compile xₑ εnv = Except.ok tₑ

theorem Cedar.Thm.mem_footprint_wf {x : Spec.Expr} {tₑ : SymCC.Term} {εnv : SymCC.SymEnv} : εnv.WellFormedFor x → tₑ ∈ SymCC.footprint x εnv → SymCC.Term.WellFormed εnv.entities tₑ

theorem Cedar.Thm.mem_footprints_wf {xs : List Spec.Expr} {t : SymCC.Term} {εnv : SymCC.SymEnv} (hwε : εnv.WellFormed) (hvr : ∀ (x : Spec.Expr), x ∈ xs → εnv.entities.ValidRefsFor x) (hin : t ∈ SymCC.footprints xs εnv) : SymCC.Term.WellFormed εnv.entities t

theorem Cedar.Thm.footprints_empty {εnv : SymCC.SymEnv} : SymCC.footprints [] εnv = ∅

theorem Cedar.Thm.footprints_singleton {x : Spec.Expr} {εnv : SymCC.SymEnv} : SymCC.footprints [x] εnv = SymCC.footprint x εnv

theorem Cedar.Thm.footprints_append {xs₁ xs₂ : List Spec.Expr} {εnv : SymCC.SymEnv} : SymCC.footprints (xs₁ ++ xs₂) εnv = SymCC.footprints xs₁ εnv ++ SymCC.footprints xs₂ εnv

theorem Cedar.Thm.footprint_subset_footprints {x : Spec.Expr} {xs : List Spec.Expr} {εnv : SymCC.SymEnv} : x ∈ xs → SymCC.footprint x εnv ⊆ SymCC.footprints xs εnv