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.

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)

theorem Mathlib.Meta.NormNum.isFibAux_zero : IsFibAux 0 0 1

theorem Mathlib.Meta.NormNum.isFibAux_one : IsFibAux 1 1 1

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'

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'

partial def Mathlib.Meta.NormNum.proveNatFibAux (en' : Q(ℕ)) : (ea' : Q(ℕ)) × (eb' : Q(ℕ)) × Q(IsFibAux «$en'» «$ea'» «$eb'»)

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'

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'

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.

theorem Mathlib.Meta.NormNum.isNat_fib {x nx z : ℕ} : IsNat x nx → Nat.fib nx = z → IsNat (Nat.fib x) z

def Mathlib.Meta.NormNum.evalNatFib : NormNumExt

Evaluates the Nat.fib function.

Equations

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