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

@[norm_num e], where e is an expression (optionally with _s) adds the tagged definition, of type NormNumExt, to the set of normalization procedures used by the norm_num tactic, such that it will fire on expressions matching the form e. Use holes in e to indicate arbitrary subexpressions, for example @[norm_num _ + _] will match any addition.

• @[norm_num e1, e2, ...] will match either e1 or e2 or ...

Example:

@[norm_num -_] def evalNeg : NormNumExt where eval {u α} e := do
  let .app (f : Q($α → $α)) (a : Q($α)) ← whnfR e | failure
  let ra ← derive a
  let rα ← inferRing α
  ra.neg

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.

def Mathlib.Meta.NormNum.instInhabitedNormNums.default : NormNums

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.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

norm_num normalizes numerical expressions in the goal. By default, it supports the operations + - * / ⁻¹ ^ and % over types with (at least) an AddMonoidWithOne instance, such as ℕ, ℤ, ℚ, ℝ, ℂ. In addition to evaluating numerical expressions, norm_num will use simp to simplify the goal. If the goal has the form A = B, A ≠ B, A < B or A ≤ B, where A and B are numerical expressions, norm_num will try to close it. It also has a relatively simple primality prover.

This tactic is extensible. Extensions can allow norm_num to evaluate more kinds of expressions, or to prove more kinds of propositions. See the @[norm_num] attribute for further information on extending norm_num.

• norm_num at l normalizes at location(s) l.
• norm_num [h1, ...] adds the arguments h1, ... to the simp set in addition to the default simp set. All options for simp arguments are supported, in particular ←, ↑ and ↓.
• norm_num only does not use the default simp set for simplification. norm_num only [h1, ...] uses only the arguments h1, ... in addition to the routines tagged @[norm_num]. norm_num only still performs post-processing steps, like simp only, use norm_num1 if you exclusively want to normalize numerical expressions.
• norm_num (config := cfg) uses cfg as configuration for simp calls (see the simp tactic for further details).

Examples:

example : 43 ≤ 74 + (33 : ℤ) := by norm_num
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num

def Mathlib.Tactic.normNum1 : Lean.ParserDescr

norm_num1 normalizes numerical expressions in the goal. It is a basic version of norm_num that does not call simp.

By default, it supports the operations + - * / ⁻¹ ^ and % over types with (at least) an AddMonoidWithOne instance, such as ℕ, ℤ, ℚ, ℝ, ℂ. If the goal has the form A = B, A ≠ B, A < B or A ≤ B, where A and B are numerical expressions, norm_num1 will try to close it. It also has a relatively simple primality prover. :e This tactic is extensible. Extensions can allow norm_num1 to evaluate more kinds of expressions, or to prove more kinds of propositions. See the @[norm_num] attribute for further information on extending norm_num1.

• norm_num1 at l normalizes at location(s) l.

Examples:

example : 43 ≤ 74 + (33 : ℤ) := by norm_num1
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num1

def Mathlib.Tactic.normNum1Conv : Lean.ParserDescr

norm_num1 normalizes numerical expressions in the goal. It is a basic version of norm_num that does not call simp.

By default, it supports the operations + - * / ⁻¹ ^ and % over types with (at least) an AddMonoidWithOne instance, such as ℕ, ℤ, ℚ, ℝ, ℂ. If the goal has the form A = B, A ≠ B, A < B or A ≤ B, where A and B are numerical expressions, norm_num1 will try to close it. It also has a relatively simple primality prover. :e This tactic is extensible. Extensions can allow norm_num1 to evaluate more kinds of expressions, or to prove more kinds of propositions. See the @[norm_num] attribute for further information on extending norm_num1.

• norm_num1 at l normalizes at location(s) l.

Examples:

example : 43 ≤ 74 + (33 : ℤ) := by norm_num1
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num1

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

Elaborator for norm_num1 conv tactic.

def Mathlib.Tactic.normNumConv : Lean.ParserDescr

norm_num normalizes numerical expressions in the goal. By default, it supports the operations + - * / ⁻¹ ^ and % over types with (at least) an AddMonoidWithOne instance, such as ℕ, ℤ, ℚ, ℝ, ℂ. In addition to evaluating numerical expressions, norm_num will use simp to simplify the goal. If the goal has the form A = B, A ≠ B, A < B or A ≤ B, where A and B are numerical expressions, norm_num will try to close it. It also has a relatively simple primality prover.

This tactic is extensible. Extensions can allow norm_num to evaluate more kinds of expressions, or to prove more kinds of propositions. See the @[norm_num] attribute for further information on extending norm_num.

• norm_num at l normalizes at location(s) l.
• norm_num [h1, ...] adds the arguments h1, ... to the simp set in addition to the default simp set. All options for simp arguments are supported, in particular ←, ↑ and ↓.
• norm_num only does not use the default simp set for simplification. norm_num only [h1, ...] uses only the arguments h1, ... in addition to the routines tagged @[norm_num]. norm_num only still performs post-processing steps, like simp only, use norm_num1 if you exclusively want to normalize numerical expressions.
• norm_num (config := cfg) uses cfg as configuration for simp calls (see the simp tactic for further details).

Examples:

example : 43 ≤ 74 + (33 : ℤ) := by norm_num
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num

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

Elaborator for norm_num conv tactic.

def Mathlib.Tactic.normNumCmd : Lean.ParserDescr

#norm_num e, where e is an expression, will print the norm_num form of e. 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.

(In the variants below, the : is optional but helpful for the parser.)

• #norm_num [h1, ...] : e adds the arguments h1, ... to the simp set in addition to the default simp set. All options for simp arguments are supported, in particular ←, ↑ and ↓.
• #norm_num only : e and #norm_num only [h1, ...] : e do not use the default simp set for simplification.
• #norm_num (config := cfg) : e uses cfg as configuration for simp calls (see the simp tactic for further details).

We register norm_num with the hint tactic.