Grace/Cumulus/Combinatorics/Lucas.g17

Open in Workbench Download source

Imports

Fibonacci

Declarations

Source

1-- The Lucas numbers 2, 1, 3, 4, 7, …: the same recurrence as the Fibonacci2-- numbers with the other start, their expression through Fibonacci numbers,3-- the doubling formula F(2n) = F(n) L(n), and the sum identity4-- 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.Lucas10import Fibonacci1112def lucas (n : Nat) : Nat := fibonacciAux(n, 2, 1)1314theorem lucas.zero15  shows lucas(0) = 216proof17  compute1819theorem lucas.one20  shows lucas(1) = 121proof22  compute2324theorem lucas.two25  shows lucas(2) = 326proof27  compute2829theorem lucas.natural (n : Nat)30  shows Nat(lucas(n))31proof32  unfold lucas33  have twoNat : Nat(2) by typecheck34  have oneNat : Nat(1) by typecheck35  exact fibonacciAux.closed at n with 2, twoNat, 1, oneNat3637theorem lucas.succ_succ (n : Nat)38  shows lucas(n + 2) = lucas(n) + lucas(n + 1)39proof40  unfold lucas41  have twoNat : Nat(2) by typecheck42  have oneNat : Nat(1) by typecheck43  exact fibonacciAux.shift at n with 2, twoNat, 1, oneNat4445-- L(n + 1) = F(n) + F(n + 2), proved together with its successor.46theorem lucas.fibonacci_pair (n : Nat)47  shows lucas(n + 1) = fibonacci(n) + fibonacci(n + 2) ∧48    lucas(n + 2) = fibonacci(n + 1) + fibonacci(n + 3)49proof50  induction n51  | zero =>52    have one : 0 + 1 = 1 by compute53    have two : 0 + 2 = 2 by compute54    have three : 0 + 3 = 3 by compute55    rw [one, two, three]56    constructor57    . compute58    . compute59  | k + 1 using ih =>60    have first := ih.left61    have second := ih.right62    have shapeA : k + 1 + 1 = k + 2 by ring63    have shapeB : k + 1 + 2 = k + 3 by ring64    have shapeC : k + 1 + 3 = k + 4 by ring65    rw [shapeA, shapeB, shapeC]66    constructor67    . exact second68    . have stepL := lucas.succ_succ at k + 169      rw [shapeB, shapeA] at stepL70      have stepF := fibonacci.succ_succ at k71      have stepF2 := fibonacci.succ_succ at k + 272      have shapeD : k + 2 + 2 = k + 4 by ring73      have shapeE : k + 2 + 1 = k + 3 by ring74      rw [shapeD, shapeE] at stepF275      rw [stepL, first, second, stepF2, stepF]76      have natK := fibonacci.natural at k77      have natK1 := fibonacci.natural at k + 178      have natK3 := fibonacci.natural at k + 379      ring8081theorem lucas.fibonacci (n : Nat)82  shows lucas(n + 1) = fibonacci(n) + fibonacci(n + 2)83proof84  have pair := lucas.fibonacci_pair at n85  exact pair.left8687theorem lucas.positive (n : Nat)88  shows 0 < lucas(n)89proof90  have split := natural.zero_or_successor at n91  cases split with isZero | isSucc92  . rw [isZero, lucas.zero]93    arith94  . obtain ⟨k, kNat, shape⟩ := isSucc95    have hk : succ(k) = k + 196      symm97      exact add.right_one at k98    rw [shape, hk, lucas.fibonacci]99    have positive := fibonacci.positive at k + 1100    have shape2 : k + 1 + 1 = k + 2 by ring101    rw shape2 at positive102    have natK := fibonacci.natural at k103    have natK2 := fibonacci.natural at k + 2104    arith105106-- The doubling formula F(2(n + 1)) = F(n + 1) · L(n + 1).107theorem fibonacci.double (n : Nat)108  shows fibonacci(2 * (n + 1)) = fibonacci(n + 1) * lucas(n + 1)109proof110  have shape : 2 * (n + 1) = (n + 1) + n + 1 by ring111  rw [shape, fibonacci.add, lucas.fibonacci]112  have shape2 : n + 1 + 1 = n + 2 by ring113  rw shape2114  have natN := fibonacci.natural at n115  have natN1 := fibonacci.natural at n + 1116  have natN2 := fibonacci.natural at n + 2117  ring118119-- L(n + 1) + L(n + 3) = 5 · F(n + 2).120theorem lucas.five_fibonacci (n : Nat)121  shows lucas(n + 1) + lucas(n + 3) = 5 * fibonacci(n + 2)122proof123  have first := lucas.fibonacci at n124  have third := lucas.fibonacci at n + 2125  have shapeA : n + 2 + 1 = n + 3 by ring126  have shapeB : n + 2 + 2 = n + 4 by ring127  rw [shapeA, shapeB] at third128  rw [first, third]129  have step0 := fibonacci.succ_succ at n130  have step1 := fibonacci.succ_succ at n + 1131  have step2 := fibonacci.succ_succ at n + 2132  have shapeC : n + 1 + 2 = n + 3 by ring133  have shapeD : n + 1 + 1 = n + 2 by ring134  rw [shapeC, shapeD] at step1135  rw [shapeB, shapeA] at step2136  have natN := fibonacci.natural at n137  have natN1 := fibonacci.natural at n + 1138  ring [step2, step1, step0]139140-- Partial sums of the Lucas numbers.141def lucasSum (n : Nat) → Nat142  | zero => 0143  | succ(k) => lucasSum(k) + lucas(k)144145theorem lucasSum.zero146  shows lucasSum(0) = 0147proof148  compute149150theorem lucasSum.succ (k : Nat)151  shows lucasSum(k + 1) = lucasSum(k) + lucas(k)152proof153  have one : k + 1 = succ(k) := add.right_one with *154  rw one155  simp [lucasSum]156157theorem lucasSum.natural (n : Nat)158  shows Nat(lucasSum(n))159proof160  induction n161  | zero =>162    rw lucasSum.zero163    typecheck164  | k + 1 using ih =>165    rw lucasSum.succ166    have natK := lucas.natural at k167    typecheck168169-- L(0) + ⋯ + L(n − 1) = L(n + 1) − 1.170theorem lucasSum.identity (n : Nat)171  shows lucasSum(n) + 1 = lucas(n + 1)172proof173  induction n174  | zero => compute175  | k + 1 using ih =>176    have shape : k + 1 + 1 = k + 2 by ring177    rw [shape, lucas.succ_succ, lucasSum.succ, ← ih]178    have natK := lucas.natural at k179    have natSum := lucasSum.natural at k180    ring181