A monad for tracking and deduplicating atoms

This monad is used by tactics like ring and abel to keep uninterpreted atoms in a consistent order, and also to allow unifying atoms up to a specified transparency mode.

Note: this can become very expensive because it is using isDefEq. For performance reasons, consider whether Lean.Meta.Canonicalizer.canon can be used instead. After canonicalizing, a HashMap Expr Nat suffices to keep track of previously seen atoms, and is much faster as it uses Expr equality rather than isDefEq.

structure Mathlib.Tactic.AtomM.Context : Type

The context (read-only state) of the AtomM monad.

• red : Lean.Meta.TransparencyMode

  The reducibility setting for definitional equality of atoms

• evalAtom : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result

  A simplification to apply to atomic expressions when they are encountered, before interning them in the atom list.

def Mathlib.Tactic.AtomM.instInhabitedContext.default : Context

@[implicit_reducible]

instance Mathlib.Tactic.AtomM.instInhabitedContext : Inhabited Context

structure Mathlib.Tactic.AtomM.State : Type

The mutable state of the AtomM monad.

• atoms : Array Lean.Expr

  The list of atoms-up-to-defeq encountered thus far, used for atom sorting.

@[reducible, inline]

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

The monad that ring works in. This is only used for collecting atoms.

def Mathlib.Tactic.AtomM.run {α : Type} (red : Lean.Meta.TransparencyMode) (m : AtomM α) (evalAtom : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result := fun (e : Lean.Expr) => pure { expr := e }) : Lean.MetaM α

Run a computation in the AtomM monad.

def Mathlib.Tactic.isDefEqSafe (a b : Lean.Expr) : Lean.MetaM Bool

A safe version of isDefEq that doesn't throw errors. We use it to avoid "unknown free variable _fvar.102937" errors when there may be out-of-scope free variables.

TODO: don't catch any other errors

def Mathlib.Tactic.AtomM.containsThenAdd (e : Lean.Expr) : AtomM (Bool × ℕ × Lean.Expr)

If an atomic expression has already been encountered, return true, the index and the stored form of the atom (which will be defeq at the specified transparency, but not necessarily syntactically equal). If the atomic expression has not already been encountered, store it in the list of atoms, and return the new index (and the stored form of the atom, which will be itself).

In a normalizing tactic, the expression returned by containsThenAdd should be considered the normal form.

def Mathlib.Tactic.AtomM.containsThenAddQ {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) : AtomM (Bool × ℕ × { e' : Q(«$α») // «$e» =Q «$e'» })

If an atomic expression has already been encountered, return true, the index and the stored form of the atom (which will be defeq at the specified transparency, but not necessarily syntactically equal). If the atomic expression has not already been encountered, store it in the list of atoms, and return the new index (and the stored form of the atom, which will be itself).

In a normalizing tactic, the expression returned by AtomM.containsThenAddQ should be considered the normal form.

This is a strongly-typed version of AtomM.containsThenAdd for code using Qq.

def Mathlib.Tactic.AtomM.addAtom (e : Lean.Expr) : AtomM (ℕ × Lean.Expr)

If an atomic expression has already been encountered, get the index and the stored form of the atom (which will be defeq at the specified transparency, but not necessarily syntactically equal). If the atomic expression has not already been encountered, store it in the list of atoms, and return the new index (and the stored form of the atom, which will be itself).

In a normalizing tactic, the expression returned by addAtom should be considered the normal form.

def Mathlib.Tactic.AtomM.addAtomQ {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) : AtomM (ℕ × { e' : Q(«$α») // «$e» =Q «$e'» })

If an atomic expression has already been encountered, get the index and the stored form of the atom (which will be defeq at the specified transparency, but not necessarily syntactically equal). If the atomic expression has not already been encountered, store it in the list of atoms, and return the new index (and the stored form of the atom, which will be itself).

In a normalizing tactic, the expression returned by addAtomQ should be considered the normal form.

This is a strongly-typed version of AtomM.addAtom for code using Qq.