inductive Cedar.Thm.Asserts.Equiv : SymCC.Asserts → SymCC.Asserts → Prop

A notion of equivalence for Asserts, suited to the purposes of Cedar.Thm.SymCC.Opt.

• rfl (a : SymCC.Asserts) : a ~ a
• constantFalse {a₁ a₂ : SymCC.Asserts} (h₁ : SymCC.Term.prim (SymCC.TermPrim.bool false) ∈ a₁) (h₂ : SymCC.Term.prim (SymCC.TermPrim.bool false) ∈ a₂) : a₁ ~ a₂

def Cedar.Thm.«term_~_» : Lean.TrailingParserDescr

Equations

• Cedar.Thm.«term_~_» = Lean.ParserDescr.trailingNode `Cedar.Thm.«term_~_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 51))

def Cedar.Thm.ResultAssertsEquiv {ε : Type u_1} (res₁ res₂ : Except ε SymCC.Asserts) : Prop

Equations

• (Except.ok a₁ ~ Except.ok a₂) = (a₁ ~ a₂)
• (Except.error e₁ ~ Except.error e₂) = (e₁ = e₂)
• (res₁ ~ res₂) = (false = true)

def Cedar.Thm.«term_~__1» : Lean.TrailingParserDescr

Equations

• Cedar.Thm.«term_~__1» = Lean.ParserDescr.trailingNode `Cedar.Thm.«term_~__1» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 51))

theorem Cedar.Thm.Asserts.Equiv.symm {a₁ a₂ : SymCC.Asserts} : a₁ ~ a₂ → a₂ ~ a₁

Symmetry for Asserts.Equiv

theorem Cedar.Thm.Asserts.Equiv.checkUnsatAsserts {a₁ a₂ : SymCC.Asserts} {εnv : SymCC.SymEnv} : a₁ ~ a₂ → SymCC.checkUnsatAsserts a₁ εnv = SymCC.checkUnsatAsserts a₂ εnv

Equivalent Asserts produce the same output in checkUnsatAsserts

theorem Cedar.Thm.Asserts.Equiv.checkSatAsserts {a₁ a₂ : SymCC.Asserts} (εnv : SymCC.SymEnv) : a₁ ~ a₂ → SymCC.checkSatAsserts a₁ εnv = SymCC.checkSatAsserts a₂ εnv

Equivalent Asserts produce the same output in checkSatAsserts

theorem Cedar.Thm.Asserts.Equiv.satAsserts? {a₁ a₂ : SymCC.Asserts} (ps : Spec.Policies) (εnv : SymCC.SymEnv) : a₁ ~ a₂ → SymCC.satAsserts? ps a₁ εnv = SymCC.satAsserts? ps a₂ εnv

Equivalent Asserts produce the same output in satAsserts?

theorem Cedar.Thm.Asserts.Equiv.satAssertsOpt? {a₁ a₂ : SymCC.Asserts} (cpss : List SymCC.CompiledPolicies) : a₁ ~ a₂ → SymCC.satAssertsOpt? cpss a₁ = SymCC.satAssertsOpt? cpss a₂

Equivalent Asserts produce the same output in satAssertsOpt?