This file proves that a term produced by compiling an expression x
has the same value under interpretations I₁ and I₂ that agree
on the footprint of x. See compile_interpret_on_footprint.
This proof relies on the theorem compile_interpret_in_footprint, which says
that every entity produced by interpreting a subexpression of x is
in the footprint of x. #
theorem
Cedar.Thm.compile_interpret_in_footprint
{x : Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{t : SymCC.Term}
{uid : Spec.EntityUID}
(hwε : εnv.WellFormedFor x)
(hI : I.WellFormed εnv.entities)
(hok : SymCC.compile x εnv = Except.ok t)
(ht : SymCC.Term.interpret I t = (SymCC.Term.entity uid).some)
:
∃ (tₑ : SymCC.Term), tₑ ∈ SymCC.footprint x εnv ∧ SymCC.Term.interpret I tₑ = (SymCC.Term.entity uid).some
theorem
Cedar.Thm.compile_interpret_lit_on_footprint
{p : Spec.Prim}
{εnv : SymCC.SymEnv}
{I₁ I₂ : SymCC.Interpretation}
{t : SymCC.Term}
(hok : SymCC.compile (Spec.Expr.lit p) εnv = Except.ok t)
:
theorem
Cedar.Thm.compile_interpret_var_on_footprint
{v : Spec.Var}
{ft : Data.Set SymCC.Term}
{εnv : SymCC.SymEnv}
{I₁ I₂ : SymCC.Interpretation}
{t : SymCC.Term}
(hwε : εnv.WellFormedFor (Spec.Expr.var v))
(hsm : εnv.SameOn ft I₁ I₂)
(hok : SymCC.compile (Spec.Expr.var v) εnv = Except.ok t)
:
theorem
Cedar.Thm.compile_interpret_on_footprint
{x : Spec.Expr}
{ft : Data.Set SymCC.Term}
{εnv : SymCC.SymEnv}
{I₁ I₂ : SymCC.Interpretation}
{t : SymCC.Term}
(hwε : εnv.WellFormedFor x)
(hI₁ : I₁.WellFormed εnv.entities)
(hI₂ : I₂.WellFormed εnv.entities)
(hsm : εnv.SameOn ft I₁ I₂)
(hft : SymCC.footprint x εnv ⊆ ft)
(hok : SymCC.compile x εnv = Except.ok t)
: