Running AtomM metaprograms recursively

Tactics such as ring and abel are implemented using the AtomM monad, which tracks "atoms" -- expressions which cannot be further parsed according to the arithmetic operations they handle -- to allow for consistent normalization relative to these atoms.

This file provides methods to allow for such normalization to run recursively: the atoms themselves will have the normalization run on any of their subterms for which this makes sense. For example, given an implementation of ring-normalization, the methods in this file implement the bottom-to-top recursive ring-normalization in which sin (x + y) + sin (y + x) is normalized first to sin (x + y) + sin (x + y) and then to 2 * sin (x + y).

Main declarations

• Mathlib.Tactic.AtomM.RecurseM.run: run a metaprogram (in AtomM or its slight extension AtomM.RecurseM), with atoms normalized according to a provided normalization operation (in AtomM), run recursively.

• Mathlib.Tactic.AtomM.recurse: run a normalization operation (in AtomM) recursively on an expression.

structure Mathlib.Tactic.AtomM.Recurse.Config : Type

Configuration for AtomM.Recurse.

• red : Lean.Meta.TransparencyMode

  the reducibility setting to use when comparing atoms for defeq

• zetaDelta : Bool

  if true, local let variables can be unfolded

instance Mathlib.Tactic.AtomM.Recurse.instInhabitedConfig : Inhabited Config

Equations

• Mathlib.Tactic.AtomM.Recurse.instInhabitedConfig = { default := Mathlib.Tactic.AtomM.Recurse.instInhabitedConfig.default }

def Mathlib.Tactic.AtomM.Recurse.instInhabitedConfig.default : Config

Equations

• Mathlib.Tactic.AtomM.Recurse.instInhabitedConfig.default = { red := default, zetaDelta := default }

def Mathlib.Tactic.AtomM.Recurse.instBEqConfig.beq : Config → Config → Bool

Equations

• Mathlib.Tactic.AtomM.Recurse.instBEqConfig.beq { red := a, zetaDelta := a_1 } { red := b, zetaDelta := b_1 } = (a == b && a_1 == b_1)
• Mathlib.Tactic.AtomM.Recurse.instBEqConfig.beq x✝¹ x✝ = false

instance Mathlib.Tactic.AtomM.Recurse.instBEqConfig : BEq Config

Equations

• Mathlib.Tactic.AtomM.Recurse.instBEqConfig = { beq := Mathlib.Tactic.AtomM.Recurse.instBEqConfig.beq }

def Mathlib.Tactic.AtomM.Recurse.instReprConfig.repr : Config → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Mathlib.Tactic.AtomM.Recurse.instReprConfig : Repr Config

Equations

• Mathlib.Tactic.AtomM.Recurse.instReprConfig = { reprPrec := Mathlib.Tactic.AtomM.Recurse.instReprConfig.repr }

structure Mathlib.Tactic.AtomM.Recurse.Context : Type

The read-only state of the AtomM.Recurse monad.

• ctx : Lean.Meta.Simp.Context

  A basically empty simp context, passed to the simp traversal in AtomM.onSubexpressions.

• simp : Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result

  A cleanup routine, which simplifies evaluation results to a more human-friendly format.

@[reducible, inline]

abbrev Mathlib.Tactic.AtomM.RecurseM (α : Type) : Type

The monad for AtomM.Recurse contains, in addition to the AtomM state, a simp context for the main traversal and a cleanup function to simplify evaluation results.

Equations

• Mathlib.Tactic.AtomM.RecurseM = ReaderT Mathlib.Tactic.AtomM.Recurse.Context Mathlib.Tactic.AtomM

def Mathlib.Tactic.AtomM.onSubexpressions (eval : Lean.Expr → AtomM Lean.Meta.Simp.Result) (parent : Lean.Expr) (root : Bool := true) : RecurseM Lean.Meta.Simp.Result

A tactic in the AtomM.RecurseM monad which will simplify expression parent to a normal form, by running a core operation eval (in the AtomM monad) on the maximal subexpression(s) on which eval does not fail.

There is also a subsequent clean-up operation, governed by the context from the AtomM.RecurseM monad.

• root: true if this is a direct call to the function. AtomM.RecurseM.run sets this to false in recursive mode.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.AtomM.RecurseM.run {α : Type} (s : IO.Ref State) (cfg : Recurse.Config) (eval : Lean.Expr → AtomM Lean.Meta.Simp.Result) (simp : Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result) (x : RecurseM α) : Lean.MetaM α

Runs a tactic in the AtomM.RecurseM monad, given initial data:

• s: a reference to the mutable AtomM state, for persisting across calls. This ensures that atom ordering is used consistently.
• cfg: the configuration options
• eval: a normalization operation which will be run recursively, potentially dependent on a known atom ordering
• simp: a cleanup operation which will be used to post-process expressions
• x: the tactic to run

Equations

• One or more equations did not get rendered due to their size.

partial def Mathlib.Tactic.AtomM.RecurseM.run.rctx (s : IO.Ref State) (cfg : Recurse.Config) (eval : Lean.Expr → AtomM Lean.Meta.Simp.Result) (nctx : Recurse.Context) : Context

The recursive context.

partial def Mathlib.Tactic.AtomM.RecurseM.run.evalAtom (s : IO.Ref State) (cfg : Recurse.Config) (eval : Lean.Expr → AtomM Lean.Meta.Simp.Result) (nctx : Recurse.Context) (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

The atom evaluator calls AtomM.onSubexpressions recursively.

def Mathlib.Tactic.AtomM.recurse (s : IO.Ref State) (cfg : Recurse.Config) (eval : Lean.Expr → AtomM Lean.Meta.Simp.Result) (simp : Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result) (tgt : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Normalizes an expression, given initial data:

• s: a reference to the mutable AtomM state, for persisting across calls. This ensures that atom ordering is used consistently.
• cfg: the configuration options
• eval: a normalization operation which will be run recursively, potentially dependent on a known atom ordering
• simp: a cleanup operation which will be used to post-process expressions
• tgt: the expression to normalize

Equations

• Mathlib.Tactic.AtomM.recurse s cfg eval simp tgt = Mathlib.Tactic.AtomM.RecurseM.run s cfg eval simp (Mathlib.Tactic.AtomM.onSubexpressions eval tgt)