doc-next-gen

Mathlib.Tactic.NormNum.Core

Module docstring

{"## 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. "}

Mathlib.Meta.NormNum.NormNumExt structure
Full source 
/--
An extension for `norm_num`.
-/
structure NormNumExt where
  /-- The extension should be run in the `pre` phase when used as simp plugin. -/
  pre := true
  /-- The extension should be run in the `post` phase when used as simp plugin. -/
  post := true
  /-- Attempts to prove an expression is equal to some explicit number of the relevant type. -/
  eval {u : Level} {α : Q(Type u)} (e : Q($α)) : MetaM (Result e)
  /-- The name of the `norm_num` extension. -/
  name : Name := by exact decl_name%
`norm_num` extension
Informal description
The structure representing an extension for the `norm_num` tactic, which provides normalization functionality based on simplification.
Mathlib.Meta.NormNum.mkNormNumExt definition
(n : Name) : ImportM NormNumExt
Full source 
/-- Read a `norm_num` extension from a declaration of the right type. -/
def mkNormNumExt (n : Name) : ImportM NormNumExt := do
  let { env, opts, .. } ← read
  IO.ofExcept <| unsafe env.evalConstCheck NormNumExt opts ``NormNumExt n
Creating a `norm_num` extension from declaration
Informal description
The function `mkNormNumExt` reads a `norm_num` extension from a declaration with the given name, evaluating it in the current environment to produce a `NormNumExt` structure that provides normalization functionality for the `norm_num` tactic.
Mathlib.Meta.NormNum.Entry abbrev
Full source 
/-- Each `norm_num` extension is labelled with a collection of patterns
which determine the expressions to which it should be applied. -/
abbrev Entry := ArrayArray (Array DiscrTree.Key) × Name
Normalization procedure registration entry for `norm_num` tactic
Informal description
This defines an entry point for registering new normalization procedures with the `norm_num` tactic system, allowing extensions to be tagged with patterns that determine when they should be applied.
Mathlib.Meta.NormNum.NormNums structure
Full source 
/-- The state of the `norm_num` extension environment -/
structure NormNums where
  /-- The tree of `norm_num` extensions. -/
  tree : DiscrTree NormNumExt := {}
  /-- Erased `norm_num`s. -/
  erased : PHashSet Name := {}
  deriving Inhabited
`norm_num` Extension Environment
Informal description
The structure representing the state of the `norm_num` tactic extension environment, which contains the normalization functionality used by the `norm_num` tactic and `@[norm_num]` attribute. This structure tracks the available normalization procedures that can simplify numerical expressions.
Mathlib.Meta.NormNum.instInhabitedNormNums instance
: Inhabited✝ (@Mathlib.Meta.NormNum.NormNums)
Full source 
Inhabited
Default Instance for `norm_num` Environment
Informal description
The `NormNums` environment for the `norm_num` tactic has a default instance.
Mathlib.Meta.NormNum.normNumExt opaque
: ScopedEnvExtension Entry (Entry × NormNumExt) NormNums
Full source 
/-- Environment extensions for `norm_num` declarations -/
initialize normNumExt : ScopedEnvExtension Entry (Entry × NormNumExt) NormNums ←
  -- we only need this to deduplicate entries in the DiscrTree
  have : BEq NormNumExt := ⟨fun _ _ ↦ false⟩
  /- Insert `v : NormNumExt` into the tree `dt` on all key sequences given in `kss`. -/
  let insert kss v dt := kss.foldl (fun dt ks ↦ dt.insertCore ks v) dt
  registerScopedEnvExtension {
    mkInitial := pure {}
    ofOLeanEntry := fun _ e@(_, n) ↦ return (e, ← mkNormNumExt n)
    toOLeanEntry := (·.1)
    addEntry := fun { tree, erased } ((kss, n), ext) ↦
      { tree := insert kss ext tree, erased := erased.erase n }
  }
`norm_num` Environment Extension for Normalization Procedures
Informal description
The `normNumExt` is a scoped environment extension that registers normalization procedures for the `norm_num` tactic, mapping entries of type `Entry` to pairs of `Entry` and `NormNumExt` within the `NormNums` environment.
Mathlib.Meta.NormNum.deriveBool definition
(p : Q(Prop)) : MetaM ((b : Bool) × BoolResult p b)
Full source 
/-- 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 deriveBool (p : Q(Prop)) : MetaM ((b : Bool) × BoolResult p b) := do
  let .isBool b prf ← derive q($p) | failure
  pure ⟨b, prf⟩
Boolean derivation for propositions via normalization
Informal description
The function takes a proposition `p` and derives a boolean value `b` along with a proof that `p` is equivalent to `b`. This is done by normalizing `p` to a boolean value using the `norm_num` tactic.
Mathlib.Meta.NormNum.deriveBoolOfIff definition
(p p' : Q(Prop)) (hp : Q($p ↔ $p')) : MetaM ((b : Bool) × BoolResult p' b)
Full source 
/-- 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 deriveBoolOfIff (p p' : Q(Prop)) (hp : Q($p ↔ $p')) :
    MetaM ((b : Bool) × BoolResult p' b) := do
  let ⟨b, pb⟩ ← deriveBool p
  match b with
  | true  => return ⟨true, q(Iff.mp $hp $pb)⟩
  | false => return ⟨false, q((Iff.not $hp).mp $pb)⟩
Boolean derivation for equivalent propositions via normalization
Informal description
Given propositions $p$ and $p'$ along with a proof $hp$ that $p \leftrightarrow p'$, the function derives a boolean value $b$ and a proof that $p'$ is equivalent to $b$ by first normalizing $p$ to a boolean value and then using the equivalence $hp$ to transfer the result to $p'$.
Mathlib.Meta.NormNum.NormNums.eraseCore definition
(d : NormNums) (declName : Name) : NormNums
Full source 
/-- Erases a name marked `norm_num` by adding it to the state's `erased` field and
  removing it from the state's list of `Entry`s. -/
def NormNums.eraseCore (d : NormNums) (declName : Name) : NormNums :=
 { d with erased := d.erased.insert declName }
Core erasure function for `norm_num` extensions
Informal description
Given a `norm_num` extension environment `d` and a declaration name `declName`, the function removes `declName` from the list of available normalization procedures in `d` and marks it as erased.
Mathlib.Meta.NormNum.NormNums.erase definition
{m : Type → Type} [Monad m] [MonadError m] (d : NormNums) (declName : Name) : m NormNums
Full source 
/--
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 NormNums.erase {m : Type → Type} [Monad m] [MonadError m] (d : NormNums) (declName : Name) :
    m NormNums := do
  unless d.tree.values.any (·.name == declName) && ! d.erased.contains declName
  do
    throwError "'{declName}' does not have [norm_num] attribute"
  return d.eraseCore declName
Removal of `norm_num` extension declaration
Informal description
Given a monadic context `m` with error handling, a `norm_num` extension environment `d`, and a declaration name `declName`, the function checks if `declName` is marked with the `@[norm_num]` attribute and not already erased, then removes it from the environment. If the declaration is not found or already erased, it throws an error.
Mathlib.Tactic.normNum definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
elab (name := normNum)
    "norm_num" cfg:optConfig only:&" only"? args:(simpArgs ?) loc:(location ?) : tactic =>
  elabNormNum cfg args loc (simpOnly := only.isSome) (useSimp := true)
Numerical normalization tactic (`norm_num`)
Informal description
The `norm_num` tactic normalizes numerical expressions involving operations such as addition (`+`), subtraction (`-`), multiplication (`*`), division (`/`), exponentiation (`^`), modulo (`%`), and inversion (`⁻¹`) over numerical types including natural numbers (`ℕ`), integers (`ℤ`), rationals (`ℚ`), reals (`ℝ`), complex numbers (`ℂ`), and some general algebraic types. It can prove goals of the form `A = B`, `A ≠ B`, `A < B`, and `A ≤ B` where `A` and `B` are numerical expressions, and includes a basic primality prover.
Mathlib.Tactic.elabNormNum1Conv definition
: Tactic
Full source 
/-- Elaborator for `norm_num1` conv tactic. -/
@[tactic normNum1Conv] def elabNormNum1Conv : Tactic := fun _ ↦ withMainContext do
  let ctx ← getSimpContext mkNullNode mkNullNode true
  Conv.applySimpResultConv.applySimpResult (← deriveSimp ctx (← instantiateMVars (← Conv.getLhs)) (useSimp := false))
`norm_num1` conversion tactic elaborator
Informal description
The elaborator for the `norm_num1` conversion tactic, which normalizes numerical expressions in Lean's conv mode by simplifying them using a simp-based driver.
Mathlib.Tactic.elabNormNumConv definition
: Tactic
Full source 
/-- Elaborator for `norm_num` conv tactic. -/
@[tactic normNumConv] def elabNormNumConv : Tactic := fun stx ↦ withMainContext do
  let ctx ← getSimpContext stx[1] stx[3] !stx[2].isNone
  Conv.applySimpResultConv.applySimpResult (← deriveSimp ctx (← instantiateMVars (← Conv.getLhs)) (useSimp := true))
`norm_num` conversion tactic elaborator
Informal description
The elaborator for the `norm_num` conversion tactic, which normalizes numerical expressions in Lean's conv mode by applying simplification rules.
Mathlib.Tactic.normNumCmd definition
: Lean.ParserDescr✝
Full source 
macro (name := normNumCmd) "#norm_num" cfg:optConfig o:(&" only")?
    args:(Parser.Tactic.simpArgs)? " :"? ppSpace e:term : command =>
  `(command| #conv norm_num $cfg:optConfig $[only%$o]? $(args)? => $e)
Numerical expression normalization command (`#norm_num`)
Informal description
The `#norm_num` command normalizes a given numerical expression `e` by applying simplification rules. It accepts optional configuration parameters, a restriction to use only specified lemmas (`only`), and additional simp lemmas. The colon before the expression is optional but aids parsing. Unlike the `norm_num` tactic, this command does not fail if no simplifications are made and can handle local variables.