The approx tactic

Given an Approx A R relationship, the approx tactic proves that expressions over A are conservative approximations of expressions over R, using aesop recursion.

def attrApprox : Lean.ParserDescr

Equations

• attrApprox = Lean.ParserDescr.node `attrApprox 1024 (Lean.ParserDescr.nonReservedSymbol "approx" false)

def approxConfig : Aesop.Options

Aesop configuration for approx

Equations

• approxConfig = { enableSimp := false }

def tacticApprox : Lean.ParserDescr

approx tactic for proving simple approx x a goals.

approx x a says that x is a conservative approximation of a as defined by the Approx typeclass. For example, approx_add says that approx (x + y) (a + b) if approx x a and approx y b. approx_add is registered as an @[approx] lemma so that the approx tactic can apply it.

Equations

• tacticApprox = Lean.ParserDescr.node `tacticApprox 1024 (Lean.ParserDescr.nonReservedSymbol "approx" false)

def tacticApprox_simp : Lean.ParserDescr

Same as approx, but also uses simp

Equations

• tacticApprox_simp = Lean.ParserDescr.node `tacticApprox_simp 1024 (Lean.ParserDescr.nonReservedSymbol "approx_simp" false)