Documentation

Mathlib.Tactic.NormNum.Pow

norm_num plugin for ^. #

structure Mathlib.Meta.NormNum.IsNatPowT (p : Prop) (a : ) (b : ) (c : ) :

This is an opaque wrapper around Nat.pow to prevent lean from unfolding the definition of Nat.pow on numerals. The arbitrary precondition p is actually a formula of the form Nat.pow a' b' = c' but we usually don't care to unfold this proposition so we just carry a reference to it.

  • run' : pa.pow b = c

    Unfolds the assertion.

Instances For
    theorem Mathlib.Meta.NormNum.IsNatPowT.run' {p : Prop} {a : } {b : } {c : } (self : Mathlib.Meta.NormNum.IsNatPowT p a b c) :
    pa.pow b = c

    Unfolds the assertion.

    theorem Mathlib.Meta.NormNum.IsNatPowT.run {a : } {b : } {c : } (p : Mathlib.Meta.NormNum.IsNatPowT (a.pow 1 = a) a b c) :
    a.pow b = c
    theorem Mathlib.Meta.NormNum.IsNatPowT.trans {a : } {b : } {c : } {p : Prop} {b' : } {c' : } (h1 : Mathlib.Meta.NormNum.IsNatPowT p a b c) (h2 : Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a b' c') :

    This is the key to making the proof proceed as a balanced tree of applications instead of a linear sequence. It is just modus ponens after unwrapping the definitions.

    theorem Mathlib.Meta.NormNum.IsNatPowT.bit0 {a : } {b : } {c : } :
    Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a (2 * b) (c.mul c)
    theorem Mathlib.Meta.NormNum.IsNatPowT.bit1 {a : } {b : } {c : } :
    Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a (2 * b + 1) (c.mul (c.mul a))
    def Mathlib.Meta.NormNum.evalNatPow (a : Q()) (b : Q()) :
    (c : Q()) × Q(«$a».pow «$b» = «$c»)

    Proves Nat.pow a b = c where a and b are raw nat literals. This could be done by just rfl but the kernel does not have a special case implementation for Nat.pow so this would proceed by unary recursion on b, which is too slow and also leads to deep recursion.

    We instead do the proof by binary recursion, but this can still lead to deep recursion, so we use an additional trick to do binary subdivision on log2 b. As a result this produces a proof of depth log (log b) which will essentially never overflow before the numbers involved themselves exceed memory limits.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      partial def Mathlib.Meta.NormNum.evalNatPow.go (depth : ) (a : Q()) (b₀ : Q()) (c₀ : Q()) (b : Q()) (p : Q(Prop)) (hp : «$p» =Q («$a».pow «$b₀» = «$c₀»)) :
      (c : Q()) × Q(Mathlib.Meta.NormNum.IsNatPowT «$p» «$a» «$b» «$c»)

      Invariants: a ^ b₀ = c₀, depth > 0, b >>> depth = b₀, p := Nat.pow $a $b₀ = $c₀

      theorem Mathlib.Meta.NormNum.intPow_ofNat {a : } {b : } {c : } (h1 : a.pow b = c) :
      (Int.ofNat a).pow b = Int.ofNat c
      theorem Mathlib.Meta.NormNum.intPow_negOfNat_bit0 {a : } {b : } {c : } {b' : } {c' : } (h1 : a.pow b' = c') (hb : 2 * b' = b) (hc : c' * c' = c) :
      theorem Mathlib.Meta.NormNum.intPow_negOfNat_bit1 {a : } {b : } {c : } {b' : } {c' : } (h1 : a.pow b' = c') (hb : 2 * b' + 1 = b) (hc : c' * (c' * a) = c) :
      def Mathlib.Meta.NormNum.evalIntPow (za : ) (a : Q()) (b : Q()) :
      × (c : Q()) × Q(«$a».pow «$b» = «$c»)

      Evaluates Int.pow a b = c where a and b are raw integer literals.

      Instances For
        theorem Mathlib.Meta.NormNum.isNat_pow {α : Type u_1} [Semiring α] {f : αα} {a : α} {b : } {a' : } {b' : } {c : } :
        f = HPow.hPowMathlib.Meta.NormNum.IsNat a a'Mathlib.Meta.NormNum.IsNat b b'a'.pow b' = cMathlib.Meta.NormNum.IsNat (f a b) c
        theorem Mathlib.Meta.NormNum.isInt_pow {α : Type u_1} [Ring α] {f : αα} {a : α} {b : } {a' : } {b' : } {c : } :
        f = HPow.hPowMathlib.Meta.NormNum.IsInt a a'Mathlib.Meta.NormNum.IsNat b b'a'.pow b' = cMathlib.Meta.NormNum.IsInt (f a b) c
        theorem Mathlib.Meta.NormNum.isRat_pow {α : Type u_1} [Ring α] {f : αα} {a : α} {an : } {cn : } {ad : } {b : } {b' : } {cd : } :
        f = HPow.hPowMathlib.Meta.NormNum.IsRat a an adMathlib.Meta.NormNum.IsNat b b'an.pow b' = cnad.pow b' = cdMathlib.Meta.NormNum.IsRat (f a b) cn cd

        The norm_num extension which identifies expressions of the form a ^ b, such that norm_num successfully recognises both a and b, with b : ℕ.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Mathlib.Meta.NormNum.evalPow.core {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α»«$α»)) (a : Q(«$α»)) (b : Q()) (nb : Q()) (pb : Q(Mathlib.Meta.NormNum.IsNat «$b» «$nb»)) (sα : Q(Semiring «$α»)) (ra : Mathlib.Meta.NormNum.Result a) :

          Main part of evalPow.

          Equations
          Instances For
            theorem Mathlib.Meta.NormNum.isNat_zpow_pos {α : Type u_1} [DivisionSemiring α] {a : α} {b : } {nb : } {ne : } (pb : Mathlib.Meta.NormNum.IsNat b nb) (pe' : Mathlib.Meta.NormNum.IsNat (a ^ nb) ne) :
            theorem Mathlib.Meta.NormNum.isRat_zpow_pos {α : Type u_1} [DivisionRing α] {a : α} {b : } {nb : } {num : } {den : } (pb : Mathlib.Meta.NormNum.IsNat b nb) (pe' : Mathlib.Meta.NormNum.IsRat (a ^ nb) num den) :
            theorem Mathlib.Meta.NormNum.isRat_zpow_neg {α : Type u_1} [DivisionRing α] {a : α} {b : } {nb : } {num : } {den : } (pb : Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb)) (pe' : Mathlib.Meta.NormNum.IsRat (a ^ nb)⁻¹ num den) :

            The norm_num extension which identifies expressions of the form a ^ b, such that norm_num successfully recognises both a and b, with b : ℤ.

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