Documentation

Mathlib.Tactic.NormNum.NatFib

norm_num extension for Nat.fib #

This norm_num extension uses a strategy parallel to that of Nat.fastFib, but it instead produces proofs of what Nat.fib evaluates to.

source
def Mathlib.Meta.NormNum.IsFibAux (n a b : ℕ) :
Prop

Auxiliary definition for proveFib extension.

Equations
Instances For
    source
    theorem Mathlib.Meta.NormNum.isFibAux_zero :
    Mathlib.Meta.NormNum.IsFibAux 0 0 1
    source
    theorem Mathlib.Meta.NormNum.isFibAux_one :
    Mathlib.Meta.NormNum.IsFibAux 1 1 1
    source
    theorem Mathlib.Meta.NormNum.isFibAux_two_mul {n a b n' a' b' : ℕ} (H : Mathlib.Meta.NormNum.IsFibAux n a b) (hn : 2 * n = n') (h1 : a * (2 * b - a) = a') (h2 : a * a + b * b = b') :
    Mathlib.Meta.NormNum.IsFibAux n' a' b'
    source
    theorem Mathlib.Meta.NormNum.isFibAux_two_mul_add_one {n a b n' a' b' : ℕ} (H : Mathlib.Meta.NormNum.IsFibAux n a b) (hn : 2 * n + 1 = n') (h1 : a * a + b * b = a') (h2 : b * (2 * a + b) = b') :
    Mathlib.Meta.NormNum.IsFibAux n' a' b'
    source
    partial def Mathlib.Meta.NormNum.proveNatFibAux (en' : Q(ℕ)) :
    (ea' : Q(ℕ)) × (eb' : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsFibAux «$en'» «$ea'» «$eb'»)
    source
    theorem Mathlib.Meta.NormNum.isFibAux_two_mul_done {n a b n' a' : ℕ} (H : Mathlib.Meta.NormNum.IsFibAux n a b) (hn : 2 * n = n') (h : a * (2 * b - a) = a') :
    Nat.fib n' = a'
    source
    theorem Mathlib.Meta.NormNum.isFibAux_two_mul_add_one_done {n a b n' a' : ℕ} (H : Mathlib.Meta.NormNum.IsFibAux n a b) (hn : 2 * n + 1 = n') (h : a * a + b * b = a') :
    Nat.fib n' = a'
    source
    def Mathlib.Meta.NormNum.proveNatFib (en' : Q(ℕ)) :
    (em : Q(ℕ)) × Q(Nat.fib «$en'» = «$em»)

    Given the natural number literal ex, returns Nat.fib ex as a natural number literal and an equality proof. Panics if ex isn't a natural number literal.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Mathlib.Meta.NormNum.isNat_fib {x nx z : ℕ} :
      Mathlib.Meta.NormNum.IsNat x nx → Nat.fib nx = z → Mathlib.Meta.NormNum.IsNat (Nat.fib x) z
      source
      def Mathlib.Meta.NormNum.evalNatFib :
      Mathlib.Meta.NormNum.NormNumExt

      Evaluates the Nat.fib function.

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