Documentation

Mathlib.Tactic.NormNum.Core

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.

Attribute for identifying norm_num extensions.

Equations
  • One or more equations did not get rendered due to their size.
structure Mathlib.Meta.NormNum.IsNat {α : Type u_1} [inst : AddMonoidWithOne α] (a : α) (n : ) :
  • The element is equal to the coercion of the natural number.

    out : a = n

Assert that an element of a semiring is equal to the coercion of some natural number.

Instances For
    def Nat.rawCast {α : Type u_1} [inst : AddMonoidWithOne α] (n : ) :
    α

    A "raw nat cast" is an expression of the form (Nat.rawCast lit : α) where lit is a raw natural number literal. These expressions are used by tactics like ring to decrease the number of typeclass arguments required in each use of a number literal at type α.

    Equations
    theorem Mathlib.Meta.NormNum.IsNat.to_eq {α : Type u_1} [inst : AddMonoidWithOne α] {n : } {a : α} {a' : α} :
    Mathlib.Meta.NormNum.IsNat a nn = a'a = a'
    structure Mathlib.Meta.NormNum.IsInt {α : Type u_1} [inst : Ring α] (a : α) (n : ) :
    • The element is equal to the coercion of the integer.

      out : a = n

    Assert that an element of a ring is equal to the coercion of some integer.

    Instances For
      def Int.rawCast {α : Type u_1} [inst : Ring α] (n : ) :
      α

      A "raw int cast" is an expression of the form:

      • (Nat.rawCast lit : α) where lit is a raw natural number literal
      • (Int.rawCast (Int.negOfNat lit) : α) where lit is a nonzero raw natural number literal

      (That is, we only actually use this function for negative integers.) This representation is used by tactics like ring to decrease the number of typeclass arguments required in each use of a number literal at type α.

      Equations
      theorem Mathlib.Meta.NormNum.IsInt.to_raw_eq {α : Type u_1} {a : α} {n : } [inst : Ring α] :
      theorem Mathlib.Meta.NormNum.IsInt.neg_to_eq {α : Type u_1} [inst : Ring α] {n : } {a : α} {a' : α} :
      Mathlib.Meta.NormNum.IsInt a (Int.negOfNat n)n = a'a = -a'
      theorem Mathlib.Meta.NormNum.IsInt.nonneg_to_eq {α : Type u_1} [inst : Ring α] {n : } {a : α} {a' : α} (h : Mathlib.Meta.NormNum.IsInt a (Int.ofNat n)) (e : n = a') :
      a = a'

      Represent an integer as a typed expression.

      Equations
      • One or more equations did not get rendered due to their size.

      A shortcut (non)instance for AddMonoidWithOne ℕ to shrink generated proofs.

      Equations

      A shortcut (non)instance for Ring ℤ to shrink generated proofs.

      Equations
      inductive Mathlib.Meta.NormNum.IsRat {α : Type u_1} [inst : Ring α] (a : α) (num : ) (denom : ) :

      Assert that an element of a ring is equal to num / denom (and denom is invertible so that this makes sense). We will usually also have num and denom coprime, although this is not part of the definition.

      Instances For
        def Rat.rawCast {α : Type u_1} [inst : DivisionRing α] (n : ) (d : ) :
        α

        A "raw rat cast" is an expression of the form:

        • (Nat.rawCast lit : α) where lit is a raw natural number literal
        • (Int.rawCast (Int.negOfNat lit) : α) where lit is a nonzero raw natural number literal
        • (Rat.rawCast n d : α) where n is a raw int cast, d is a raw nat cast, and d is not 1 or 0.

        This representation is used by tactics like ring to decrease the number of typeclass arguments required in each use of a number literal at type α.

        Equations
        theorem Mathlib.Meta.NormNum.IsRat.to_raw_eq {α : Type u_1} {n : } {d : } [inst : DivisionRing α] {a : α} :
        theorem Mathlib.Meta.NormNum.IsRat.neg_to_eq {α : Type u_1} [inst : DivisionRing α] {n : } {d : } {a : α} {n' : α} {d' : α} :
        Mathlib.Meta.NormNum.IsRat a (Int.negOfNat n) dn = n'd = d'a = -(n' / d')
        theorem Mathlib.Meta.NormNum.IsRat.nonneg_to_eq {α : Type u_1} [inst : DivisionRing α] {n : } {d : } {a : α} {n' : α} {d' : α} :
        Mathlib.Meta.NormNum.IsRat a (Int.ofNat n) dn = n'd = d'a = n' / d'
        theorem Mathlib.Meta.NormNum.IsRat.of_raw (α : Type u_1) [inst : DivisionRing α] (n : ) (d : ) (h : d 0) :
        theorem Mathlib.Meta.NormNum.IsRat.den_nz {α : Type u_1} [inst : DivisionRing α] {a : α} {n : } {d : } :

        Represent an integer as a typed expression.

        Equations
        • One or more equations did not get rendered due to their size.

        A shortcut (non)instance for Ring ℚ to shrink generated proofs.

        Equations

        A shortcut (non)instance for DivisionRing ℚ to shrink generated proofs.

        Equations

        The result of norm_num running on an expression x of type α. Untyped version of Result.

        Instances For

          The result of norm_num running on an expression x of type α.

          Equations
          instance Mathlib.Meta.NormNum.instInhabitedResult :
          {a : Lean.Level} → {α : Q(Type a)} → {x : Q(«$α»)} → Inhabited (Mathlib.Meta.NormNum.Result x)
          Equations
          @[match_pattern, inline]

          The result is proof : x, where x is a (true) proposition.

          Equations
          @[match_pattern, inline]

          The result is proof : ¬x¬x, where x is a (false) proposition.

          Equations
          @[match_pattern, inline]
          def Mathlib.Meta.NormNum.Result.isNat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {x : Qq.QQ α} (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne [u]) α)) _auto✝) (lit : Q()) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsNat [u]) α) inst) x) lit)) :

          The result is lit : ℕ (a raw nat literal) and proof : isNat x lit.

          Equations
          @[match_pattern, inline]
          def Mathlib.Meta.NormNum.Result.isNegNat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {x : Qq.QQ α} (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) _auto✝) (lit : Q()) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsInt [u]) α) inst) x) (Lean.Expr.app (Lean.Expr.const `Int.negOfNat []) lit))) :

          The result is -lit where lit is a raw nat literal and proof : isInt x (.negOfNat lit).

          Equations
          @[match_pattern, inline]
          def Mathlib.Meta.NormNum.Result.isRat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {x : Qq.QQ α} (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) (q : ) (n : Q()) (d : Q()) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) inst)) x) n) d)) :

          The result is proof : isRat x n d, where n is either .ofNat lit or .negOfNat lit with lit a raw nat literal and d is a raw nat literal (not 0 or 1), and q is the value of n / d.

          Equations

          A shortcut (non)instance for AddMonoidWithOne α from Ring α to shrink generated proofs.

          Equations
          • Mathlib.Meta.NormNum.instAddMonoidWithOne = inferInstance
          def Mathlib.Meta.NormNum.Result.isInt {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {x : Qq.QQ α} (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) _auto✝) (z : Q()) (n : ) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsInt [u]) α) inst) x) z)) :

          The result is z : ℤ and proof : isNat x z.

          Equations
          • One or more equations did not get rendered due to their size.
          def Mathlib.Meta.NormNum.Result.toRat :
          {a : Lean.Level} → {α : Q(Type a)} → {e : Q(«$α»)} → Mathlib.Meta.NormNum.Result eOption

          Returns the rational number that is the result of norm_num evaluation.

          Equations
          • One or more equations did not get rendered due to their size.
          def Lean.LOption.toOption {α : Type u_1} :

          Convert undef to none to make an LOption into an Option.

          Equations

          Helper function to synthesize a typed AddMonoidWithOne α expression.

          Equations
          • One or more equations did not get rendered due to their size.

          Helper function to synthesize a typed Semiring α expression.

          Equations
          • One or more equations did not get rendered due to their size.

          Helper function to synthesize a typed Ring α expression.

          Equations
          • One or more equations did not get rendered due to their size.

          Helper function to synthesize a typed DivisionRing α expression.

          Equations
          • One or more equations did not get rendered due to their size.

          Helper function to synthesize a typed OrderedSemiring α expression.

          Equations
          • One or more equations did not get rendered due to their size.

          Helper function to synthesize a typed OrderedRing α expression.

          Equations
          • One or more equations did not get rendered due to their size.

          Helper function to synthesize a typed LinearOrderedField α expression.

          Equations
          • One or more equations did not get rendered due to their size.
          def Mathlib.Meta.NormNum.inferCharZeroOfRing {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) _auto✝) :
          Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) _i))))

          Helper function to synthesize a typed CharZero α expression given Ring α.

          Equations
          • One or more equations did not get rendered due to their size.
          def Mathlib.Meta.NormNum.inferCharZeroOfRing? {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) _auto✝) :
          Lean.MetaM (Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) _i)))))

          Helper function to synthesize a typed CharZero α expression given Ring α, if it exists.

          Equations
          • One or more equations did not get rendered due to their size.

          Helper function to synthesize a typed CharZero α expression given AddMonoidWithOne α.

          Equations
          • One or more equations did not get rendered due to their size.

          Helper function to synthesize a typed CharZero α expression given AddMonoidWithOne α, if it exists.

          Equations
          • One or more equations did not get rendered due to their size.
          def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) :
          Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) _i)))))

          Helper function to synthesize a typed CharZero α expression given DivisionRing α.

          Equations
          • One or more equations did not get rendered due to their size.
          def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing? {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) :
          Lean.MetaM (Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) _i))))))

          Helper function to synthesize a typed CharZero α expression given DivisionRing α, if it exists.

          Equations
          • One or more equations did not get rendered due to their size.

          Extract from a Result the integer value (as both a term and an expression), and the proof that the original expression is equal to this integer.

          Equations
          • One or more equations did not get rendered due to their size.
          def Mathlib.Meta.NormNum.Result.toRat' {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {e : Qq.QQ α} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) :
          Mathlib.Meta.NormNum.Result eOption ( × (n : Q()) × (d : Q()) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) _i)) e) n) d))

          Extract from a Result the rational value (as both a term and an expression), and the proof that the original expression is equal to this rational number.

          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.

          Given a NormNum.Result e (which uses IsNat, IsInt, IsRat to express equality to a rational numeral), converts it to an equality e = Nat.rawCast n, e = Int.rawCast n, or e = Rat.rawCast n d to a raw cast expression, so it can be used for rewriting.

          Equations
          • One or more equations did not get rendered due to their size.

          Result.toRawEq but providing an integer. Given a NormNum.Result e for something known to be an integer (which uses IsNat or IsInt to express equality to an integer numeral), converts it to an equality e = Nat.rawCast n or e = Int.rawCast n to a raw cast expression, so it can be used for rewriting. Gives none if not an integer.

          Equations
          • One or more equations did not get rendered due to their size.

          Constructs a Result out of a raw nat cast. Assumes e is a raw nat cast expression.

          Equations
          • One or more equations did not get rendered due to their size.

          Constructs a Result out of a raw int cast. Assumes e is a raw int cast expression denoting n.

          Equations
          • One or more equations did not get rendered due to their size.

          Constructs a Result out of a raw rat cast. Assumes e is a raw rat cast expression denoting n.

          Equations
          • One or more equations did not get rendered due to their size.
          def Mathlib.Meta.NormNum.Result.isRat' {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {x : Qq.QQ α} (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) (q : ) (n : Q()) (d : Q()) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) inst)) x) n) d)) :

          The result depends on whether q : ℚ happens to be an integer, in which case the result is .isInt .. whereas otherwise it's .isRat ...

          Equations
          • One or more equations did not get rendered due to their size.
          def Mathlib.Meta.NormNum.Result.toRatNZ :
          {a : Lean.Level} → {α : Q(Type a)} → {e : Q(«$α»)} → Mathlib.Meta.NormNum.Result eOption ( × Option Lean.Expr)

          Returns the rational number that is the result of norm_num evaluation, along with a proof that the denominator is nonzero in the isRat case.

          Equations
          • One or more equations did not get rendered due to their size.
          def Mathlib.Meta.NormNum.mkOfNat {u : Lean.Level} (α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))) (_sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne [u]) α)) (lit : Q()) :
          Lean.MetaM ((a' : Qq.QQ α) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Eq [Lean.Level.succ u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Nat.cast [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne.toNatCast [u]) α) _sα)) lit)) a'))

          Constructs an ofNat application a' with the canonical instance, together with a proof that the instance is equal to the result of Nat.cast on the given AddMonoidWithOne instance.

          This function is performance-critical, as many higher level tactics have to construct numerals. So rather than using typeclass search we hardcode the (relatively small) set of solutions to the typeclass problem.

          Equations
          • One or more equations did not get rendered due to their size.

          Convert a Result to a Simp.Result.

          Equations
          • One or more equations did not get rendered due to their size.

          A extension for norm_num.

          Instances For

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

            Equations
            @[inline]

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

            Equations

            The state of the norm_num extension environment

            Instances For

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

              Equations
              • One or more equations did not get rendered due to their size.
              def Mathlib.Meta.NormNum.deriveNat' {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) :
              Lean.MetaM ((_inst : Qq.QQ (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne [u]) α)) × (lit : Qq.QQ (Lean.Expr.const `Nat [])) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsNat [u]) α) _inst) 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.

              Equations
              • One or more equations did not get rendered due to their size.
              def Mathlib.Meta.NormNum.deriveNat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (_inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne [u]) α)) _auto✝) :
              Lean.MetaM ((lit : Q()) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsNat [u]) α) _inst) 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.

              Equations
              • One or more equations did not get rendered due to their size.
              def Mathlib.Meta.NormNum.deriveInt {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (_inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) _auto✝) :
              Lean.MetaM ((lit : Q()) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsInt [u]) α) _inst) 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.

              Equations
              • One or more equations did not get rendered due to their size.
              def Mathlib.Meta.NormNum.deriveRat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (_inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) :
              Lean.MetaM ( × (n : Q()) × (d : Q()) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) _inst)) 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.

              Equations
              • One or more equations did not get rendered due to their size.

              Extract the natural number n if the expression is of the form OfNat.ofNat n.

              Equations
              • One or more equations did not get rendered due to their size.

              Extract the integer i if the expression is either a natural number literal or the negation of one.

              Equations
              • One or more equations did not get rendered due to their size.

              Extract the numerator n : ℤ and denominator d : ℕ if the expression is either an integer literal, or the division of one integer literal by another.

              Equations
              • One or more equations did not get rendered due to their size.

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

              Equations
              • One or more equations did not get rendered due to their size.

              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.

              Equations

              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.

              Equations
              • One or more equations did not get rendered due to their size.

              A simp plugin which calls NormNum.eval.

              Equations
              • One or more equations did not get rendered due to their size.

              Constructs a proof that the original expression is true given a simp result which simplifies the target to True.

              Equations
              • One or more equations did not get rendered due to their size.

              A Methods implementation which calls norm_num.

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

              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
              Equations
              • One or more equations did not get rendered due to their size.

              Constructs a simp context from the simp argument syntax.

              Equations
              • One or more equations did not get rendered due to their size.

              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
              Equations
              • One or more equations did not get rendered due to their size.

              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≠ B, A < B and A ≤ B≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

              Equations
              • One or more equations did not get rendered due to their size.

              Basic version of norm_num that does not call simp.

              Equations
              • One or more equations did not get rendered due to their size.

              Basic version of norm_num that does not call simp.

              Equations

              Elaborator for norm_num1 conv tactic.

              Equations
              • One or more equations did not get rendered due to their size.

              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≠ B, A < B and A ≤ B≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

              Equations
              • One or more equations did not get rendered due to their size.

              Elaborator for norm_num conv tactic.

              Equations
              • One or more equations did not get rendered due to their size.

              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.

              Equations
              • One or more equations did not get rendered due to their size.