# `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

- Mathlib.Meta.NormNum.IsFibAux n a b = (Nat.fib n = a ∧ Nat.fib (n + 1) = b)

Instances For

source
theorem Mathlib.Meta.NormNum.isFibAux_zero :
IsFibAux 0 0 1
source
theorem Mathlib.Meta.NormNum.isFibAux_one :
IsFibAux 1 1 1
source
theorem Mathlib.Meta.NormNum.isFibAux_two_mul {n a b n' a' b' : ℕ} (H : IsFibAux n a b) (hn : 2 * n = n') (h1 : a * (2 * b - a) = a') (h2 : a * a + b * b = b') :
IsFibAux n' a' b'
source
theorem Mathlib.Meta.NormNum.isFibAux_two_mul_add_one {n a b n' a' b' : ℕ} (H : IsFibAux n a b) (hn : 2 * n + 1 = n') (h1 : a * a + b * b = a') (h2 : b * (2 * a + b) = b') :
IsFibAux n' a' b'
source
partial def Mathlib.Meta.NormNum.proveNatFibAux (en' : Q(ℕ)) :
(ea' : Q(ℕ)) × (eb' : Q(ℕ)) × Q(IsFibAux «$en'» «$ea'» «$eb'»)
source
theorem Mathlib.Meta.NormNum.isFibAux_two_mul_done {n a b n' a' : ℕ} (H : 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 : 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 : ℕ} :
IsNat x nx → Nat.fib nx = z → IsNat (Nat.fib x) z
source
def Mathlib.Meta.NormNum.evalNatFib :
NormNumExt

Evaluates the `Nat.fib` function.

Equations

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

Instances For