Documentation

Cedar.Thm.SymCC.Enforcer.Footprint

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

source
def Cedar.SymCC.footprint_ofEntity_wf {x : Spec.Expr} {εnv : SymEnv} :
(footprint.ofEntity x εnv).WellFormed
Equations
  • ⋯ = ⋯
Instances For
    source
    def Cedar.SymCC.footprint_ofBranch_wf {εnv : SymEnv} {x : Spec.Expr} {ft₁ ft₂ ft₃ : Data.Set Term} :
    ft₂.WellFormed → ft₃.WellFormed → (footprint.ofBranch εnv x ft₁ ft₂ ft₃).WellFormed
    Equations
    • ⋯ = ⋯
    Instances For
      source
      def Cedar.SymCC.footprint_wf (x : Spec.Expr) (εnv : SymEnv) :
      (footprint x εnv).WellFormed
      Equations
      • ⋯ = ⋯
      Instances For
        source
        def Cedar.SymCC.footprints_wf (xs : List Spec.Expr) (εnv : SymEnv) :
        (footprints xs εnv).WellFormed
        Equations
        • ⋯ = ⋯
        Instances For
          source
          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.
          Instances For
            source
            def Cedar.SymCC.SymEnv.SameOn (εnv : SymEnv) (ft : Data.Set Term) (I₁ I₂ : Interpretation) :
            Prop
            Equations
            Instances For
              source
              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
              source
              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
              source
              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ₑ
              source
              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ₑ
              source
              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ₑ
              source
              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
              source
              theorem Cedar.Thm.footprints_empty {εnv : SymCC.SymEnv} :
              SymCC.footprints [] εnv = ∅
              source
              theorem Cedar.Thm.footprints_singleton {x : Spec.Expr} {εnv : SymCC.SymEnv} :
              SymCC.footprints [x] εnv = SymCC.footprint x εnv
              source
              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
              source
              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