Commit 2023-05-27 10:43 67093cd0

View on Github →

port: Nat.fib extension for norm_num (#4036)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Nat/Fib.lean

added theorem Nat.fib_two_mul_add_two

deleted def NormNum.IsFibAux

deleted theorem NormNum.is_fib_aux_bit0

deleted theorem NormNum.is_fib_aux_bit0_done

deleted theorem NormNum.is_fib_aux_bit1

deleted theorem NormNum.is_fib_aux_bit1_done

deleted theorem NormNum.is_fib_aux_one

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/NormNum/NatFib.lean

added def Mathlib.Meta.NormNum.IsFibAux

added def Mathlib.Meta.NormNum.evalNatFib

added theorem Mathlib.Meta.NormNum.isFibAux_one

added theorem Mathlib.Meta.NormNum.isFibAux_two_mul

added theorem Mathlib.Meta.NormNum.isFibAux_two_mul_add_one

added theorem Mathlib.Meta.NormNum.isFibAux_two_mul_add_one_done

added theorem Mathlib.Meta.NormNum.isFibAux_two_mul_done

added theorem Mathlib.Meta.NormNum.isFibAux_zero

added theorem Mathlib.Meta.NormNum.isNat_fib

added def Mathlib.Meta.NormNum.proveNatFib

Modified test/norm_num_ext.lean