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

• contextual : Bool

  if true, implication hypotheses are added to the local context of the discharger

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

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

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

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

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

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

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.

def Mathlib.Tactic.AtomM.onSubexpressions (eval : Lean.Expr → AtomM Lean.Meta.Simp.Result) (parent : Lean.Expr) (wellBehavedDischarge : Bool) (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.

def Mathlib.Tactic.AtomM.RecurseM.run {α : Type} (s : IO.Ref State) (cfg : Recurse.Config) (wellBehavedDischarge : Bool) (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
• wellBehavedDischarge : MUST be set to false IF eval accesses local declarations with index >= Context.lctxInitIndices. Reason: it would cause simp to cache results too aggressively.
• 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

def Mathlib.Tactic.AtomM.recurse (s : IO.Ref State) (cfg : Recurse.Config) (wellBehavedDischarge : Bool) (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
• wellBehavedDischarge : MUST be set to false IF eval accesses local declarations with index >= Context.lctxInitIndices. Reason: it would cause simp to cache results too aggressively.
• 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