This file proves properties of the counterexample extraction functions
in Cedar/SymCC/Extractor.lean. #
theorem
Cedar.Thm.repair_wf
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
:
εnv.WellFormed →
(∀ (x : Spec.Expr), x ∈ xs → εnv.entities.ValidRefsFor x) →
I.WellFormed εnv.entities → (SymCC.Interpretation.repair (SymCC.footprints xs εnv) εnv I).WellFormed εnv.entities
theorem
Cedar.Thm.repair_env_wf_same
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
:
εnv.WellFormed →
(∀ (x : Spec.Expr), x ∈ xs → εnv.entities.ValidRefsFor x) →
I.WellFormed εnv.entities →
(SymCC.Interpretation.repair (SymCC.footprints xs εnv) εnv I).WellFormed εnv.entities ∧ ∃ (env : Spec.Env), env ∼ SymCC.SymEnv.interpret (SymCC.Interpretation.repair (SymCC.footprints xs εnv) εnv I) εnv ∧ env.WellFormed ∧ ∀ (x : Spec.Expr), x ∈ xs → env.entities.ValidRefsFor x
theorem
Cedar.Thm.extract?_env_wf_same
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
:
εnv.WellFormed →
(∀ (x : Spec.Expr), x ∈ xs → εnv.entities.ValidRefsFor x) →
I.WellFormed εnv.entities →
∃ (env : Spec.Env), SymCC.SymEnv.extract? xs I εnv = some env ∧ env ∼ SymCC.SymEnv.interpret (SymCC.Interpretation.repair (SymCC.footprints xs εnv) εnv I) εnv ∧ env.WellFormed ∧ ∀ (x : Spec.Expr), x ∈ xs → env.entities.ValidRefsFor x
theorem
Cedar.Thm.not_mem_footprintUIDs_implies_empty_ancs
{uid : Spec.EntityUID}
{ety : Spec.EntityType}
{f : SymCC.UUF}
{δ : SymCC.SymEntityData}
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
(hwε : εnv.WellFormed)
(hI : I.WellFormed εnv.entities)
(hδ : Data.Map.find? εnv.entities uid.ty = some δ)
(hf : δ.ancestors.find? ety = some (SymCC.UnaryFunction.uuf f))
(hft : ¬uid ∈ SymCC.Interpretation.repair.footprintUIDs (SymCC.footprints xs εnv) I)
:
theorem
Cedar.Thm.mem_footprintUIDs_implies_eq_ancs
{uid : Spec.EntityUID}
{ety : Spec.EntityType}
{f : SymCC.UUF}
{δ : SymCC.SymEntityData}
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
(hwε : εnv.WellFormed)
(hI : I.WellFormed εnv.entities)
(hδ : Data.Map.find? εnv.entities uid.ty = some δ)
(hf : δ.ancestors.find? ety = some (SymCC.UnaryFunction.uuf f))
(hft : uid ∈ SymCC.Interpretation.repair.footprintUIDs (SymCC.footprints xs εnv) I)
:
theorem
Cedar.Thm.mem_footprintUIDs_mem_footprints
{uid : Spec.EntityUID}
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
(hwε : εnv.WellFormed)
(hvr : ∀ (x : Spec.Expr), x ∈ xs → εnv.entities.ValidRefsFor x)
(hI : I.WellFormed εnv.entities)
(hin : uid ∈ SymCC.Interpretation.repair.footprintUIDs (SymCC.footprints xs εnv) I)
:
∃ (t : SymCC.Term), t ∈ SymCC.footprints xs εnv ∧ SymCC.Term.interpret I t = (SymCC.Term.entity uid).some
theorem
Cedar.Thm.mem_mem_footprints_footprintUIDs
{t : SymCC.Term}
{uid : Spec.EntityUID}
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
(hin : t ∈ SymCC.footprints xs εnv)
(ht : SymCC.Term.interpret I t = (SymCC.Term.entity uid).some)
:
theorem
Cedar.Thm.εnv_same_on_footprints
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
(hsε : εnv.StronglyWellFormedForAll xs)
(hI : I.WellFormed εnv.entities)
:
εnv.SameOn (SymCC.footprints xs εnv) I (SymCC.Interpretation.repair (SymCC.footprints xs εnv) εnv I)
theorem
Cedar.Thm.sym_entities_entityUIDs_include_enums
{εnv : SymCC.SymEnv}
{uid : Spec.EntityUID}
{δ : SymCC.SymEntityData}
{eids : Data.Set String}
(I : SymCC.Interpretation)
(hfind_uid_ty : Data.Map.find? εnv.entities uid.ty = some δ)
(heids : δ.members = some eids)
(heid : uid.eid ∈ eids)
:
theorem
Cedar.Thm.extract?_implies_enum_complete
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{exprs : List Spec.Expr}
(hext : some env = SymCC.SymEnv.extract? exprs I εnv)
:
SymCC.Env.EnumCompleteFor env εnv
SymEnv.extract? always produces a concrete Env that satisfies Env.EnumCompleteFor.