norm_num core functionality

This file sets up the norm_num tactic and the @[norm_num] attribute, which allow for plugging in new normalization functionality around a simp-based driver. The actual behavior is in @[norm_num]-tagged definitions in Tactic.NormNum.Basic and elsewhere.

def norm_num : Lean.ParserDescr

Attribute for identifying norm_num extensions.

structure Mathlib.Meta.NormNum.NormNumExt : Type

An extension for norm_num.

• pre : Bool

  The extension should be run in the pre phase when used as simp plugin.

• post : Bool

  The extension should be run in the post phase when used as simp plugin.

• eval {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) : Lean.MetaM (Result e)

  Attempts to prove an expression is equal to some explicit number of the relevant type.

• name : Lean.Name

  The name of the norm_num extension.

def Mathlib.Meta.NormNum.mkNormNumExt (n : Lean.Name) : Lean.ImportM NormNumExt

Read a norm_num extension from a declaration of the right type.

@[reducible, inline]

abbrev Mathlib.Meta.NormNum.Entry : Type

Each norm_num extension is labelled with a collection of patterns which determine the expressions to which it should be applied.

structure Mathlib.Meta.NormNum.NormNums : Type

The state of the norm_num extension environment

• tree : Lean.Meta.DiscrTree NormNumExt

  The tree of norm_num extensions.

• erased : Lean.PHashSet Lean.Name

  Erased norm_nums.

instance Mathlib.Meta.NormNum.instInhabitedNormNums : Inhabited NormNums

opaque Mathlib.Meta.NormNum.normNumExt : Lean.ScopedEnvExtension Entry (Entry × NormNumExt) NormNums

Environment extensions for norm_num declarations

def Mathlib.Meta.NormNum.derive {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (post : Bool := false) : Lean.MetaM (Result e)

Run each registered norm_num extension on an expression, returning a NormNum.Result.

def Mathlib.Meta.NormNum.deriveNat {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (_inst : Q(AddMonoidWithOne «$α») := by with_reducible assumption) : Lean.MetaM ((lit : Q(ℕ)) × Q(IsNat «$e» «$lit»))

Run each registered norm_num extension on a typed expression e : α, returning a typed expression lit : ℕ, and a proof of isNat e lit.

def Mathlib.Meta.NormNum.deriveInt {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (_inst : Q(Ring «$α») := by with_reducible assumption) : Lean.MetaM ((lit : Q(ℤ)) × Q(IsInt «$e» «$lit»))

Run each registered norm_num extension on a typed expression e : α, returning a typed expression lit : ℤ, and a proof of IsInt e lit in expression form.

def Mathlib.Meta.NormNum.deriveRat {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (_inst : Q(DivisionRing «$α») := by with_reducible assumption) : Lean.MetaM (ℚ × (n : Q(ℤ)) × (d : Q(ℕ)) × Q(IsRat «$e» «$n» «$d»))

Run each registered norm_num extension on a typed expression e : α, returning a rational number, typed expressions n : ℤ and d : ℕ for the numerator and denominator, and a proof of IsRat e n d in expression form.

def Mathlib.Meta.NormNum.deriveBool (p : Q(Prop)) : Lean.MetaM ((b : Bool) × BoolResult p b)

Run each registered norm_num extension on a typed expression p : Prop, and returning the truth or falsity of p' : Prop from an equivalence p ↔ p'.

def Mathlib.Meta.NormNum.deriveBoolOfIff (p p' : Q(Prop)) (hp : Q(«$p» ↔ «$p'»)) : Lean.MetaM ((b : Bool) × BoolResult p' b)

Run each registered norm_num extension on a typed expression p : Prop, and returning the truth or falsity of p' : Prop from an equivalence p ↔ p'.

def Mathlib.Meta.NormNum.eval (e : Lean.Expr) (post : Bool := false) : Lean.MetaM Lean.Meta.Simp.Result

Run each registered norm_num extension on an expression, returning a Simp.Result.

def Mathlib.Meta.NormNum.NormNums.eraseCore (d : NormNums) (declName : Lean.Name) : NormNums

Erases a name marked norm_num by adding it to the state's erased field and removing it from the state's list of Entrys.

def Mathlib.Meta.NormNum.NormNums.erase {m : Type → Type} [Monad m] [Lean.MonadError m] (d : NormNums) (declName : Lean.Name) : m NormNums

Erase a name marked as a norm_num attribute.

Check that it does in fact have the norm_num attribute by making sure it names a NormNumExt found somewhere in the state's tree, and is not erased.

def Mathlib.Meta.NormNum.tryNormNum (post : Bool := false) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

A simp plugin which calls NormNum.eval.

partial def Mathlib.Meta.NormNum.discharge (ctx : Lean.Meta.Simp.Context) (useSimp : Bool := true) (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Expr)

A discharger which calls norm_num.

partial def Mathlib.Meta.NormNum.methods (ctx : Lean.Meta.Simp.Context) (useSimp : Bool := true) : Lean.Meta.Simp.Methods

A Methods implementation which calls norm_num.

partial def Mathlib.Meta.NormNum.deriveSimp (ctx : Lean.Meta.Simp.Context) (useSimp : Bool := true) (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Traverses the given expression using simp and normalises any numbers it finds.

def Mathlib.Meta.NormNum.normNumAt (g : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (fvarIdsToSimp : Array Lean.FVarId) (simplifyTarget useSimp : Bool := true) : Lean.MetaM (Option (Array Lean.FVarId × Lean.MVarId))

The core of norm_num as a tactic in MetaM.

• g: The goal to simplify
• ctx: The simp context, constructed by mkSimpContext and containing any additional simp rules we want to use
• fvarIdsToSimp: The selected set of hypotheses used in the location argument
• simplifyTarget: true if the target is selected in the location argument
• useSimp: true if we used norm_num instead of norm_num1

def Mathlib.Meta.NormNum.getSimpContext (cfg args : Lean.Syntax) (simpOnly : Bool := false) : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Context

Constructs a simp context from the simp argument syntax.

def Mathlib.Meta.NormNum.elabNormNum (cfg args loc : Lean.Syntax) (simpOnly : Bool := false) (useSimp : Bool := true) : Lean.Elab.Tactic.TacticM Unit

Elaborates a call to norm_num only? [args] or norm_num1.

• args: the (simpArgs)? syntax for simp arguments
• loc: the (location)? syntax for the optional location argument
• simpOnly: true if only was used in norm_num
• useSimp: false if norm_num1 was used, in which case only the structural parts of simp will be used, not any of the post-processing that simp only does without lemmas

def Mathlib.Tactic.normNum : Lean.ParserDescr

Normalize numerical expressions. Supports the operations + - * / ⁻¹ ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ and some general algebraic types, and can prove goals of the form A = B, A ≠ B, A < B and A ≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

def Mathlib.Tactic.normNum1 : Lean.ParserDescr

Basic version of norm_num that does not call simp.

def Mathlib.Tactic.normNum1Conv : Lean.ParserDescr

Basic version of norm_num that does not call simp.

def Mathlib.Tactic.elabNormNum1Conv : Lean.Elab.Tactic.Tactic

Elaborator for norm_num1 conv tactic.

def Mathlib.Tactic.normNumConv : Lean.ParserDescr

Normalize numerical expressions. Supports the operations + - * / ⁻¹ ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ and some general algebraic types, and can prove goals of the form A = B, A ≠ B, A < B and A ≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

def Mathlib.Tactic.elabNormNumConv : Lean.Elab.Tactic.Tactic

Elaborator for norm_num conv tactic.

def Mathlib.Tactic.normNumCmd : Lean.ParserDescr

The basic usage is #norm_num e, where e is an expression, which will print the norm_num form of e.

Syntax: #norm_num (only)? ([ simp lemma list ])? :? expression

This accepts the same options as the #simp command. You can specify additional simp lemmas as usual, for example using #norm_num [f, g] : e. (The colon is optional but helpful for the parser.) The only restricts norm_num to using only the provided lemmas, and so #norm_num only : e behaves similarly to norm_num1.

Unlike norm_num, this command does not fail when no simplifications are made.

#norm_num understands local variables, so you can use them to introduce parameters.