Grace/Cumulus/Combinatorics/Fibonacci.g17

Open in Workbench Download source

Imports

Permutations · NumberTheory.Divisibility

Declarations

Source

1-- The Fibonacci numbers by a two-register recursion: the recurrence,2-- positivity and monotonicity, the sum identities, Cassini's identity,3-- the addition formula, and the divisibility F(m) ∣ F(m · n)4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Combinatorics.Fibonacci10import Permutations11import NumberTheory.Divisibility1213-- fibonacciAux(n, a, b) is the n-th term of the sequence starting a, b.14def fibonacciAux (n a b : Nat) → Nat15  | zero, a, b => a16  | succ(k), a, b => fibonacciAux(k, b, a + b)17  descends n1819def fibonacci (n : Nat) : Nat := fibonacciAux(n, 0, 1)2021theorem fibonacciAux.zero (a b : Nat)22  shows fibonacciAux(0, a, b) = a23proof24  simp [fibonacciAux]2526theorem fibonacciAux.succ (k a b : Nat)27  shows fibonacciAux(k + 1, a, b) = fibonacciAux(k, b, a + b)28proof29  have one : k + 1 = succ(k) := add.right_one with *30  rw one31  simp [fibonacciAux]3233theorem fibonacciAux.one (a b : Nat)34  shows fibonacciAux(1, a, b) = b35proof36  simp [fibonacciAux]3738theorem fibonacciAux.closed (n : Nat)39  shows ∀ a, Nat(a) → ∀ b, Nat(b) → Nat(fibonacciAux(n, a, b))40proof41  induction n42  | zero =>43    intros a aNat b bNat44    rw fibonacciAux.zero45    exact aNat46  | k + 1 using ih =>47    intros a aNat b bNat48    rw fibonacciAux.succ49    have sumNat : Nat(a + b) by typecheck50    exact ih with b, bNat, a + b, sumNat5152-- Every sequence obeying the recursion satisfies the Fibonacci recurrence.53theorem fibonacciAux.shift (n : Nat)54  shows ∀ a, Nat(a) → ∀ b, Nat(b) → fibonacciAux(n + 2, a, b) =55    fibonacciAux(n, a, b) + fibonacciAux(n + 1, a, b)56proof57  induction n58  | zero =>59    intros a aNat b bNat60    have two : 0 + 2 = 2 by compute61    have one : 0 + 1 = 1 by compute62    rw [two, one]63    simp [fibonacciAux]64  | k + 1 using ih =>65    intros a aNat b bNat66    have shape : k + 1 + 2 = (k + 2) + 1 by ring67    have shape2 : k + 1 + 1 = k + 2 by ring68    rw [shape, shape2]69    have top := fibonacciAux.succ at k + 2, a, b70    have middle := fibonacciAux.succ at k, a, b71    have last := fibonacciAux.succ at k + 1, a, b72    rw shape2 at last73    rw [top, middle, last]74    have sumNat : Nat(a + b) by typecheck75    exact ih with b, bNat, a + b, sumNat7677theorem fibonacci.zero78  shows fibonacci(0) = 079proof80  compute8182theorem fibonacci.one83  shows fibonacci(1) = 184proof85  compute8687theorem fibonacci.two88  shows fibonacci(2) = 189proof90  compute9192theorem fibonacci.three93  shows fibonacci(3) = 294proof95  compute9697theorem fibonacci.natural (n : Nat)98  shows Nat(fibonacci(n))99proof100  unfold fibonacci101  have zeroNat : Nat(0) by typecheck102  have oneNat : Nat(1) by typecheck103  exact fibonacciAux.closed at n with 0, zeroNat, 1, oneNat104105theorem fibonacci.succ_succ (n : Nat)106  shows fibonacci(n + 2) = fibonacci(n) + fibonacci(n + 1)107proof108  unfold fibonacci109  have zeroNat : Nat(0) by typecheck110  have oneNat : Nat(1) by typecheck111  exact fibonacciAux.shift at n with 0, zeroNat, 1, oneNat112113theorem fibonacci.positive (n : Nat)114  shows 0 < fibonacci(n + 1)115proof116  induction n117  | zero =>118    have one : 0 + 1 = 1 by compute119    rw [one, fibonacci.one]120    arith121  | k + 1 using ih =>122    have shape : k + 1 + 1 = k + 2 by ring123    rw [shape, fibonacci.succ_succ]124    have natK := fibonacci.natural at k125    have natK1 := fibonacci.natural at k + 1126    arith127128theorem fibonacci.monotone (n : Nat)129  shows fibonacci(n) ≤ fibonacci(n + 1)130proof131  have split := natural.zero_or_successor at n132  cases split with isZero | isSucc133  . rw isZero134    have one : 0 + 1 = 1 by compute135    rw [one, fibonacci.zero, fibonacci.one]136    arith137  . obtain ⟨k, kNat, shape⟩ := isSucc138    have hk : succ(k) = k + 1139      symm140      exact add.right_one at k141    rw [shape, hk]142    have shape2 : k + 1 + 1 = k + 2 by ring143    rw [shape2, fibonacci.succ_succ]144    have natK := fibonacci.natural at k145    have natK1 := fibonacci.natural at k + 1146    arith147148theorem fibonacci.le_of_le (m d : Nat)149  shows fibonacci(m) ≤ fibonacci(m + d)150proof151  induction d152  | zero =>153    have shape : m + 0 = m by ring154    rw shape155    have natM := fibonacci.natural at m156    exact LessEqual.reflexive at fibonacci(m)157  | j + 1 using ih =>158    have shape : m + (j + 1) = (m + j) + 1 by ring159    rw shape160    have step := fibonacci.monotone at m + j161    have natM := fibonacci.natural at m162    have natJ := fibonacci.natural at m + j163    have natTop := fibonacci.natural at m + j + 1164    exact LessEqual.transitive with ih, step165166theorem fibonacci.strict (n : Nat)167  shows fibonacci(n + 2) < fibonacci(n + 3)168proof169  have shape : n + 3 = (n + 1) + 2 by ring170  have step := fibonacci.succ_succ at n + 1171  have shape2 : n + 1 + 1 = n + 2 by ring172  rw shape2 at step173  rw [shape, step]174  have positive := fibonacci.positive at n175  have natN1 := fibonacci.natural at n + 1176  have natN2 := fibonacci.natural at n + 2177  arith178179-- Partial sums of the Fibonacci numbers.180def fibonacciSum (n : Nat) → Nat181  | zero => 0182  | succ(k) => fibonacciSum(k) + fibonacci(k)183184theorem fibonacciSum.zero185  shows fibonacciSum(0) = 0186proof187  compute188189theorem fibonacciSum.succ (k : Nat)190  shows fibonacciSum(k + 1) = fibonacciSum(k) + fibonacci(k)191proof192  have one : k + 1 = succ(k) := add.right_one with *193  rw one194  simp [fibonacciSum]195196theorem fibonacciSum.natural (n : Nat)197  shows Nat(fibonacciSum(n))198proof199  induction n200  | zero =>201    rw fibonacciSum.zero202    typecheck203  | k + 1 using ih =>204    rw fibonacciSum.succ205    have natK := fibonacci.natural at k206    typecheck207208-- F(0) + ⋯ + F(n − 1) = F(n + 1) − 1.209theorem fibonacciSum.identity (n : Nat)210  shows fibonacciSum(n) + 1 = fibonacci(n + 1)211proof212  induction n213  | zero => compute214  | k + 1 using ih =>215    have shape : k + 1 + 1 = k + 2 by ring216    rw [shape, fibonacci.succ_succ, fibonacciSum.succ, ← ih]217    have natK := fibonacci.natural at k218    have natSum := fibonacciSum.natural at k219    ring220221theorem fibonacciSum.sub (n : Nat)222  shows fibonacciSum(n) = fibonacci(n + 1) - 1223proof224  rw ← fibonacciSum.identity225  have natSum := fibonacciSum.natural at n226  symm227  exact sub.add_right at fibonacciSum(n), 1228229-- Partial sums of the squares.230def fibonacciSquareSum (n : Nat) → Nat231  | zero => 0232  | succ(k) => fibonacciSquareSum(k) + fibonacci(k) * fibonacci(k)233234theorem fibonacciSquareSum.zero235  shows fibonacciSquareSum(0) = 0236proof237  compute238239theorem fibonacciSquareSum.succ (k : Nat)240  shows241    fibonacciSquareSum(k + 1) = fibonacciSquareSum(k) + fibonacci(k) * fibonacci(k)242proof243  have one : k + 1 = succ(k) := add.right_one with *244  rw one245  simp [fibonacciSquareSum]246247-- F(0)² + ⋯ + F(n)² = F(n) · F(n + 1).248theorem fibonacciSquareSum.identity (n : Nat)249  shows fibonacciSquareSum(n + 1) = fibonacci(n) * fibonacci(n + 1)250proof251  induction n252  | zero => compute253  | k + 1 using ih =>254    have two : k + 1 + 1 = k + 2 by ring255    have expand := fibonacciSquareSum.succ at k + 1256    have step := fibonacci.succ_succ at k257    rw two at expand258    rw [two, expand, ih, step]259    have natK := fibonacci.natural at k260    have natK1 := fibonacci.natural at k + 1261    ring262263-- Cassini's identity, split by the parity of the index.264theorem fibonacci.cassini_even (n : Nat)265  shows fibonacci(2 * n + 1) * fibonacci(2 * n + 1) =266    fibonacci(2 * n) * fibonacci(2 * n + 2) + 1267proof268  induction n269  | zero => compute270  | k + 1 using ih =>271    have shapeA : 2 * (k + 1) + 1 = 2 * k + 3 by ring272    have shapeB : 2 * (k + 1) = 2 * k + 2 by ring273    have shapeC : 2 * (k + 1) + 2 = 2 * k + 4 by ring274    rw [shapeA, shapeC, shapeB]275    have stepTwo := fibonacci.succ_succ at 2 * k276    have stepThree := fibonacci.succ_succ at 2 * k + 1277    have stepFour := fibonacci.succ_succ at 2 * k + 2278    have three : 2 * k + 1 + 2 = 2 * k + 3 by ring279    have four : 2 * k + 2 + 2 = 2 * k + 4 by ring280    have oneTwo : 2 * k + 1 + 1 = 2 * k + 2 by ring281    have twoThree : 2 * k + 2 + 1 = 2 * k + 3 by ring282    rw three at stepThree283    rw oneTwo at stepThree284    rw [four, twoThree] at stepFour285    rw [stepFour, stepThree, stepTwo]286    rw stepTwo at ih287    have natA := fibonacci.natural at 2 * k288    have natB := fibonacci.natural at 2 * k + 1289    have balance : (fibonacci(2 * k + 1) + (fibonacci(2 * k) + fibonacci(2 * k + 1))) * (fibonacci(2 * k + 1) + (fibonacci(2 * k) + fibonacci(2 * k + 1))) + (fibonacci(2 * k) * (fibonacci(2 * k) + fibonacci(2 * k + 1)) + 1) = (fibonacci(2 * k) + fibonacci(2 * k + 1)) * (fibonacci(2 * k) + fibonacci(2 * k + 1) + (fibonacci(2 * k + 1) + (fibonacci(2 * k) + fibonacci(2 * k + 1)))) + 1 + fibonacci(2 * k + 1) * fibonacci(2 * k + 1) by ring290    rw ih at balance291    exact add.right_cancel with balance292293theorem fibonacci.cassini_odd (n : Nat)294  shows fibonacci(2 * n + 2) * fibonacci(2 * n + 2) + 1 =295    fibonacci(2 * n + 1) * fibonacci(2 * n + 3)296proof297  have even := fibonacci.cassini_even at n298  have stepTwo := fibonacci.succ_succ at 2 * n299  have stepThree := fibonacci.succ_succ at 2 * n + 1300  have three : 2 * n + 1 + 2 = 2 * n + 3 by ring301  have oneTwo : 2 * n + 1 + 1 = 2 * n + 2 by ring302  rw [three, oneTwo] at stepThree303  rw [stepThree, stepTwo]304  rw stepTwo at even305  have natA := fibonacci.natural at 2 * n306  have natB := fibonacci.natural at 2 * n + 1307  have balance : (fibonacci(2 * n) + fibonacci(2 * n + 1)) * (fibonacci(2 * n) + fibonacci(2 * n + 1)) + 1 + fibonacci(2 * n + 1) * fibonacci(2 * n + 1) = fibonacci(2 * n + 1) * (fibonacci(2 * n + 1) + (fibonacci(2 * n) + fibonacci(2 * n + 1))) + (fibonacci(2 * n) * (fibonacci(2 * n) + fibonacci(2 * n + 1)) + 1) by ring308  rw even at balance309  exact add.right_cancel with balance310311-- The addition formula F(m + n + 1) = F(m) F(n) + F(m + 1) F(n + 1), proved312-- together with its successor.313theorem fibonacci.add_pair (m n : Nat)314  shows fibonacci(m + n + 1) = fibonacci(m) * fibonacci(n) + fibonacci(m + 1) * fibonacci(n + 1) ∧315    fibonacci(m + n + 2) = fibonacci(m) * fibonacci(n + 1) + fibonacci(m + 1) * fibonacci(n + 2)316proof317  induction n318  | zero =>319    have shapeA : m + 0 + 1 = m + 1 by ring320    have shapeB : m + 0 + 2 = m + 2 by ring321    have one : 0 + 1 = 1 by compute322    have two : 0 + 2 = 2 by compute323    rw [shapeA, shapeB, one, two, fibonacci.zero, fibonacci.one, fibonacci.two, fibonacci.succ_succ]324    have natM := fibonacci.natural at m325    have natM1 := fibonacci.natural at m + 1326    constructor327    . ring328    . ring329  | k + 1 using ih =>330    have first := ih.left331    have second := ih.right332    have shapeA : m + (k + 1) + 1 = m + k + 2 by ring333    have shapeB : m + (k + 1) + 2 = (m + k + 1) + 2 by ring334    have shapeC : k + 1 + 1 = k + 2 by ring335    have shapeD : k + 1 + 2 = k + 3 by ring336    rw [shapeA, shapeB, shapeC, shapeD]337    have stepTop := fibonacci.succ_succ at m + k + 1338    have shapeE : m + k + 1 + 1 = m + k + 2 by ring339    rw shapeE at stepTop340    have stepK := fibonacci.succ_succ at k341    have stepK1 := fibonacci.succ_succ at k + 1342    have shapeF : k + 1 + 2 = k + 3 by ring343    rw [shapeF, shapeC] at stepK1344    have natM := fibonacci.natural at m345    have natM1 := fibonacci.natural at m + 1346    have natK := fibonacci.natural at k347    have natK1 := fibonacci.natural at k + 1348    have natK2 := fibonacci.natural at k + 2349    constructor350    . exact second351    . rw [stepTop, first, second]352      ring [stepK1, stepK]353354theorem fibonacci.add (m n : Nat)355  shows356    fibonacci(m + n + 1) = fibonacci(m) * fibonacci(n) + fibonacci(m + 1) * fibonacci(n + 1)357proof358  have pair := fibonacci.add_pair at m, n359  exact pair.left360361theorem fibonacci.odd_index (n : Nat)362  shows363    fibonacci(2 * n + 1) = fibonacci(n) * fibonacci(n) + fibonacci(n + 1) * fibonacci(n + 1)364proof365  have shape : 2 * n + 1 = n + n + 1 by ring366  rw shape367  exact fibonacci.add at n, n368369-- F(m) divides F(m · n).370theorem fibonacci.divides_mul (m n : Nat)371  shows fibonacci(m) ∣ fibonacci(m * n)372proof373  induction n374  | zero =>375    have shape : m * 0 = 0 by ring376    rw [shape, fibonacci.zero]377    have natM := fibonacci.natural at m378    exact divides.zero at fibonacci(m)379  | k + 1 using ih =>380    have split := natural.zero_or_successor at m381    cases split with isZero | isSucc382    . rw isZero383      have shape : 0 * (k + 1) = 0 by ring384      rw [shape, fibonacci.zero]385      exact divides.zero at 0386    . obtain ⟨j, jNat, shape⟩ := isSucc387      have hj : succ(j) = j + 1388        symm389        exact add.right_one at j390      rw [shape, hj]391      rw [shape, hj] at ih392      have expand : (j + 1) * (k + 1) = (j + 1) * k + j + 1 by ring393      rw expand394      have formula := fibonacci.add at (j + 1) * k, j395      rw formula396      have natProduct := fibonacci.natural at (j + 1) * k397      have natProduct1 := fibonacci.natural at (j + 1) * k + 1398      have natJ := fibonacci.natural at j399      have natJ1 := fibonacci.natural at j + 1400      have left : fibonacci(j + 1) ∣ fibonacci((j + 1) * k) * fibonacci(j)401        exact divides.multiply_right with ih402      have right : fibonacci(j + 1) ∣ fibonacci((j + 1) * k + 1) * fibonacci(j + 1)403        exact divides.multiply_left at fibonacci(j + 1), fibonacci(j + 1), fibonacci((j + 1) * k + 1) with natJ1, natJ1, natProduct1, (divides.reflexive at fibonacci(j + 1))404      exact divides.add with left, right405