-- The Lucas numbers 2, 1, 3, 4, 7, …: the same recurrence as the Fibonacci
-- numbers with the other start, their expression through Fibonacci numbers,
-- the doubling formula F(2n) = F(n) L(n), and the sum identity
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Combinatorics.Lucas
import Fibonacci

def lucas (n : Nat) : Nat := fibonacciAux(n, 2, 1)

theorem lucas.zero
  shows lucas(0) = 2
proof
  compute

theorem lucas.one
  shows lucas(1) = 1
proof
  compute

theorem lucas.two
  shows lucas(2) = 3
proof
  compute

theorem lucas.natural (n : Nat)
  shows Nat(lucas(n))
proof
  unfold lucas
  have twoNat : Nat(2) by typecheck
  have oneNat : Nat(1) by typecheck
  exact fibonacciAux.closed at n with 2, twoNat, 1, oneNat

theorem lucas.succ_succ (n : Nat)
  shows lucas(n + 2) = lucas(n) + lucas(n + 1)
proof
  unfold lucas
  have twoNat : Nat(2) by typecheck
  have oneNat : Nat(1) by typecheck
  exact fibonacciAux.shift at n with 2, twoNat, 1, oneNat

-- L(n + 1) = F(n) + F(n + 2), proved together with its successor.
theorem lucas.fibonacci_pair (n : Nat)
  shows lucas(n + 1) = fibonacci(n) + fibonacci(n + 2) ∧
    lucas(n + 2) = fibonacci(n + 1) + fibonacci(n + 3)
proof
  induction n
  | zero =>
    have one : 0 + 1 = 1 by compute
    have two : 0 + 2 = 2 by compute
    have three : 0 + 3 = 3 by compute
    rw [one, two, three]
    constructor
    . compute
    . compute
  | k + 1 using ih =>
    have first := ih.left
    have second := ih.right
    have shapeA : k + 1 + 1 = k + 2 by ring
    have shapeB : k + 1 + 2 = k + 3 by ring
    have shapeC : k + 1 + 3 = k + 4 by ring
    rw [shapeA, shapeB, shapeC]
    constructor
    . exact second
    . have stepL := lucas.succ_succ at k + 1
      rw [shapeB, shapeA] at stepL
      have stepF := fibonacci.succ_succ at k
      have stepF2 := fibonacci.succ_succ at k + 2
      have shapeD : k + 2 + 2 = k + 4 by ring
      have shapeE : k + 2 + 1 = k + 3 by ring
      rw [shapeD, shapeE] at stepF2
      rw [stepL, first, second, stepF2, stepF]
      have natK := fibonacci.natural at k
      have natK1 := fibonacci.natural at k + 1
      have natK3 := fibonacci.natural at k + 3
      ring

theorem lucas.fibonacci (n : Nat)
  shows lucas(n + 1) = fibonacci(n) + fibonacci(n + 2)
proof
  have pair := lucas.fibonacci_pair at n
  exact pair.left

theorem lucas.positive (n : Nat)
  shows 0 < lucas(n)
proof
  have split := natural.zero_or_successor at n
  cases split with isZero | isSucc
  . rw [isZero, lucas.zero]
    arith
  . obtain ⟨k, kNat, shape⟩ := isSucc
    have hk : succ(k) = k + 1
      symm
      exact add.right_one at k
    rw [shape, hk, lucas.fibonacci]
    have positive := fibonacci.positive at k + 1
    have shape2 : k + 1 + 1 = k + 2 by ring
    rw shape2 at positive
    have natK := fibonacci.natural at k
    have natK2 := fibonacci.natural at k + 2
    arith

-- The doubling formula F(2(n + 1)) = F(n + 1) · L(n + 1).
theorem fibonacci.double (n : Nat)
  shows fibonacci(2 * (n + 1)) = fibonacci(n + 1) * lucas(n + 1)
proof
  have shape : 2 * (n + 1) = (n + 1) + n + 1 by ring
  rw [shape, fibonacci.add, lucas.fibonacci]
  have shape2 : n + 1 + 1 = n + 2 by ring
  rw shape2
  have natN := fibonacci.natural at n
  have natN1 := fibonacci.natural at n + 1
  have natN2 := fibonacci.natural at n + 2
  ring

-- L(n + 1) + L(n + 3) = 5 · F(n + 2).
theorem lucas.five_fibonacci (n : Nat)
  shows lucas(n + 1) + lucas(n + 3) = 5 * fibonacci(n + 2)
proof
  have first := lucas.fibonacci at n
  have third := lucas.fibonacci at n + 2
  have shapeA : n + 2 + 1 = n + 3 by ring
  have shapeB : n + 2 + 2 = n + 4 by ring
  rw [shapeA, shapeB] at third
  rw [first, third]
  have step0 := fibonacci.succ_succ at n
  have step1 := fibonacci.succ_succ at n + 1
  have step2 := fibonacci.succ_succ at n + 2
  have shapeC : n + 1 + 2 = n + 3 by ring
  have shapeD : n + 1 + 1 = n + 2 by ring
  rw [shapeC, shapeD] at step1
  rw [shapeB, shapeA] at step2
  have natN := fibonacci.natural at n
  have natN1 := fibonacci.natural at n + 1
  ring [step2, step1, step0]

-- Partial sums of the Lucas numbers.
def lucasSum (n : Nat) → Nat
  | zero => 0
  | succ(k) => lucasSum(k) + lucas(k)

theorem lucasSum.zero
  shows lucasSum(0) = 0
proof
  compute

theorem lucasSum.succ (k : Nat)
  shows lucasSum(k + 1) = lucasSum(k) + lucas(k)
proof
  have one : k + 1 = succ(k) := add.right_one with *
  rw one
  simp [lucasSum]

theorem lucasSum.natural (n : Nat)
  shows Nat(lucasSum(n))
proof
  induction n
  | zero =>
    rw lucasSum.zero
    typecheck
  | k + 1 using ih =>
    rw lucasSum.succ
    have natK := lucas.natural at k
    typecheck

-- L(0) + ⋯ + L(n − 1) = L(n + 1) − 1.
theorem lucasSum.identity (n : Nat)
  shows lucasSum(n) + 1 = lucas(n + 1)
proof
  induction n
  | zero => compute
  | k + 1 using ih =>
    have shape : k + 1 + 1 = k + 2 by ring
    rw [shape, lucas.succ_succ, lucasSum.succ, ← ih]
    have natK := lucas.natural at k
    have natSum := lucasSum.natural at k
    ring