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 : Mathlib.Meta.NormNum.IsFibAux 0 0 1

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

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'

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'

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

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'

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'

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 : ℕ} : Mathlib.Meta.NormNum.IsNat x nx → Nat.fib nx = z → Mathlib.Meta.NormNum.IsNat (Nat.fib x) z

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.