-- The Fibonacci numbers by a two-register recursion: the recurrence,
-- positivity and monotonicity, the sum identities, Cassini's identity,
-- the addition formula, and the divisibility F(m) ∣ F(m · n)
-- 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.Fibonacci
import Permutations
import NumberTheory.Divisibility

-- fibonacciAux(n, a, b) is the n-th term of the sequence starting a, b.
def fibonacciAux (n a b : Nat) → Nat
  | zero, a, b => a
  | succ(k), a, b => fibonacciAux(k, b, a + b)
  descends n

def fibonacci (n : Nat) : Nat := fibonacciAux(n, 0, 1)

theorem fibonacciAux.zero (a b : Nat)
  shows fibonacciAux(0, a, b) = a
proof
  simp [fibonacciAux]

theorem fibonacciAux.succ (k a b : Nat)
  shows fibonacciAux(k + 1, a, b) = fibonacciAux(k, b, a + b)
proof
  have one : k + 1 = succ(k) := add.right_one with *
  rw one
  simp [fibonacciAux]

theorem fibonacciAux.one (a b : Nat)
  shows fibonacciAux(1, a, b) = b
proof
  simp [fibonacciAux]

theorem fibonacciAux.closed (n : Nat)
  shows ∀ a, Nat(a) → ∀ b, Nat(b) → Nat(fibonacciAux(n, a, b))
proof
  induction n
  | zero =>
    intros a aNat b bNat
    rw fibonacciAux.zero
    exact aNat
  | k + 1 using ih =>
    intros a aNat b bNat
    rw fibonacciAux.succ
    have sumNat : Nat(a + b) by typecheck
    exact ih with b, bNat, a + b, sumNat

-- Every sequence obeying the recursion satisfies the Fibonacci recurrence.
theorem fibonacciAux.shift (n : Nat)
  shows ∀ a, Nat(a) → ∀ b, Nat(b) → fibonacciAux(n + 2, a, b) =
    fibonacciAux(n, a, b) + fibonacciAux(n + 1, a, b)
proof
  induction n
  | zero =>
    intros a aNat b bNat
    have two : 0 + 2 = 2 by compute
    have one : 0 + 1 = 1 by compute
    rw [two, one]
    simp [fibonacciAux]
  | k + 1 using ih =>
    intros a aNat b bNat
    have shape : k + 1 + 2 = (k + 2) + 1 by ring
    have shape2 : k + 1 + 1 = k + 2 by ring
    rw [shape, shape2]
    have top := fibonacciAux.succ at k + 2, a, b
    have middle := fibonacciAux.succ at k, a, b
    have last := fibonacciAux.succ at k + 1, a, b
    rw shape2 at last
    rw [top, middle, last]
    have sumNat : Nat(a + b) by typecheck
    exact ih with b, bNat, a + b, sumNat

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

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

theorem fibonacci.two
  shows fibonacci(2) = 1
proof
  compute

theorem fibonacci.three
  shows fibonacci(3) = 2
proof
  compute

theorem fibonacci.natural (n : Nat)
  shows Nat(fibonacci(n))
proof
  unfold fibonacci
  have zeroNat : Nat(0) by typecheck
  have oneNat : Nat(1) by typecheck
  exact fibonacciAux.closed at n with 0, zeroNat, 1, oneNat

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

theorem fibonacci.positive (n : Nat)
  shows 0 < fibonacci(n + 1)
proof
  induction n
  | zero =>
    have one : 0 + 1 = 1 by compute
    rw [one, fibonacci.one]
    arith
  | k + 1 using ih =>
    have shape : k + 1 + 1 = k + 2 by ring
    rw [shape, fibonacci.succ_succ]
    have natK := fibonacci.natural at k
    have natK1 := fibonacci.natural at k + 1
    arith

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

theorem fibonacci.le_of_le (m d : Nat)
  shows fibonacci(m) ≤ fibonacci(m + d)
proof
  induction d
  | zero =>
    have shape : m + 0 = m by ring
    rw shape
    have natM := fibonacci.natural at m
    exact LessEqual.reflexive at fibonacci(m)
  | j + 1 using ih =>
    have shape : m + (j + 1) = (m + j) + 1 by ring
    rw shape
    have step := fibonacci.monotone at m + j
    have natM := fibonacci.natural at m
    have natJ := fibonacci.natural at m + j
    have natTop := fibonacci.natural at m + j + 1
    exact LessEqual.transitive with ih, step

theorem fibonacci.strict (n : Nat)
  shows fibonacci(n + 2) < fibonacci(n + 3)
proof
  have shape : n + 3 = (n + 1) + 2 by ring
  have step := fibonacci.succ_succ at n + 1
  have shape2 : n + 1 + 1 = n + 2 by ring
  rw shape2 at step
  rw [shape, step]
  have positive := fibonacci.positive at n
  have natN1 := fibonacci.natural at n + 1
  have natN2 := fibonacci.natural at n + 2
  arith

-- Partial sums of the Fibonacci numbers.
def fibonacciSum (n : Nat) → Nat
  | zero => 0
  | succ(k) => fibonacciSum(k) + fibonacci(k)

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

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

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

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

theorem fibonacciSum.sub (n : Nat)
  shows fibonacciSum(n) = fibonacci(n + 1) - 1
proof
  rw ← fibonacciSum.identity
  have natSum := fibonacciSum.natural at n
  symm
  exact sub.add_right at fibonacciSum(n), 1

-- Partial sums of the squares.
def fibonacciSquareSum (n : Nat) → Nat
  | zero => 0
  | succ(k) => fibonacciSquareSum(k) + fibonacci(k) * fibonacci(k)

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

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

-- F(0)² + ⋯ + F(n)² = F(n) · F(n + 1).
theorem fibonacciSquareSum.identity (n : Nat)
  shows fibonacciSquareSum(n + 1) = fibonacci(n) * fibonacci(n + 1)
proof
  induction n
  | zero => compute
  | k + 1 using ih =>
    have two : k + 1 + 1 = k + 2 by ring
    have expand := fibonacciSquareSum.succ at k + 1
    have step := fibonacci.succ_succ at k
    rw two at expand
    rw [two, expand, ih, step]
    have natK := fibonacci.natural at k
    have natK1 := fibonacci.natural at k + 1
    ring

-- Cassini's identity, split by the parity of the index.
theorem fibonacci.cassini_even (n : Nat)
  shows fibonacci(2 * n + 1) * fibonacci(2 * n + 1) =
    fibonacci(2 * n) * fibonacci(2 * n + 2) + 1
proof
  induction n
  | zero => compute
  | k + 1 using ih =>
    have shapeA : 2 * (k + 1) + 1 = 2 * k + 3 by ring
    have shapeB : 2 * (k + 1) = 2 * k + 2 by ring
    have shapeC : 2 * (k + 1) + 2 = 2 * k + 4 by ring
    rw [shapeA, shapeC, shapeB]
    have stepTwo := fibonacci.succ_succ at 2 * k
    have stepThree := fibonacci.succ_succ at 2 * k + 1
    have stepFour := fibonacci.succ_succ at 2 * k + 2
    have three : 2 * k + 1 + 2 = 2 * k + 3 by ring
    have four : 2 * k + 2 + 2 = 2 * k + 4 by ring
    have oneTwo : 2 * k + 1 + 1 = 2 * k + 2 by ring
    have twoThree : 2 * k + 2 + 1 = 2 * k + 3 by ring
    rw three at stepThree
    rw oneTwo at stepThree
    rw [four, twoThree] at stepFour
    rw [stepFour, stepThree, stepTwo]
    rw stepTwo at ih
    have natA := fibonacci.natural at 2 * k
    have natB := fibonacci.natural at 2 * k + 1
    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 ring
    rw ih at balance
    exact add.right_cancel with balance

theorem fibonacci.cassini_odd (n : Nat)
  shows fibonacci(2 * n + 2) * fibonacci(2 * n + 2) + 1 =
    fibonacci(2 * n + 1) * fibonacci(2 * n + 3)
proof
  have even := fibonacci.cassini_even at n
  have stepTwo := fibonacci.succ_succ at 2 * n
  have stepThree := fibonacci.succ_succ at 2 * n + 1
  have three : 2 * n + 1 + 2 = 2 * n + 3 by ring
  have oneTwo : 2 * n + 1 + 1 = 2 * n + 2 by ring
  rw [three, oneTwo] at stepThree
  rw [stepThree, stepTwo]
  rw stepTwo at even
  have natA := fibonacci.natural at 2 * n
  have natB := fibonacci.natural at 2 * n + 1
  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 ring
  rw even at balance
  exact add.right_cancel with balance

-- The addition formula F(m + n + 1) = F(m) F(n) + F(m + 1) F(n + 1), proved
-- together with its successor.
theorem fibonacci.add_pair (m n : Nat)
  shows fibonacci(m + n + 1) = fibonacci(m) * fibonacci(n) + fibonacci(m + 1) * fibonacci(n + 1) ∧
    fibonacci(m + n + 2) = fibonacci(m) * fibonacci(n + 1) + fibonacci(m + 1) * fibonacci(n + 2)
proof
  induction n
  | zero =>
    have shapeA : m + 0 + 1 = m + 1 by ring
    have shapeB : m + 0 + 2 = m + 2 by ring
    have one : 0 + 1 = 1 by compute
    have two : 0 + 2 = 2 by compute
    rw [shapeA, shapeB, one, two, fibonacci.zero, fibonacci.one, fibonacci.two, fibonacci.succ_succ]
    have natM := fibonacci.natural at m
    have natM1 := fibonacci.natural at m + 1
    constructor
    . ring
    . ring
  | k + 1 using ih =>
    have first := ih.left
    have second := ih.right
    have shapeA : m + (k + 1) + 1 = m + k + 2 by ring
    have shapeB : m + (k + 1) + 2 = (m + k + 1) + 2 by ring
    have shapeC : k + 1 + 1 = k + 2 by ring
    have shapeD : k + 1 + 2 = k + 3 by ring
    rw [shapeA, shapeB, shapeC, shapeD]
    have stepTop := fibonacci.succ_succ at m + k + 1
    have shapeE : m + k + 1 + 1 = m + k + 2 by ring
    rw shapeE at stepTop
    have stepK := fibonacci.succ_succ at k
    have stepK1 := fibonacci.succ_succ at k + 1
    have shapeF : k + 1 + 2 = k + 3 by ring
    rw [shapeF, shapeC] at stepK1
    have natM := fibonacci.natural at m
    have natM1 := fibonacci.natural at m + 1
    have natK := fibonacci.natural at k
    have natK1 := fibonacci.natural at k + 1
    have natK2 := fibonacci.natural at k + 2
    constructor
    . exact second
    . rw [stepTop, first, second]
      ring [stepK1, stepK]

theorem fibonacci.add (m n : Nat)
  shows
    fibonacci(m + n + 1) = fibonacci(m) * fibonacci(n) + fibonacci(m + 1) * fibonacci(n + 1)
proof
  have pair := fibonacci.add_pair at m, n
  exact pair.left

theorem fibonacci.odd_index (n : Nat)
  shows
    fibonacci(2 * n + 1) = fibonacci(n) * fibonacci(n) + fibonacci(n + 1) * fibonacci(n + 1)
proof
  have shape : 2 * n + 1 = n + n + 1 by ring
  rw shape
  exact fibonacci.add at n, n

-- F(m) divides F(m · n).
theorem fibonacci.divides_mul (m n : Nat)
  shows fibonacci(m) ∣ fibonacci(m * n)
proof
  induction n
  | zero =>
    have shape : m * 0 = 0 by ring
    rw [shape, fibonacci.zero]
    have natM := fibonacci.natural at m
    exact divides.zero at fibonacci(m)
  | k + 1 using ih =>
    have split := natural.zero_or_successor at m
    cases split with isZero | isSucc
    . rw isZero
      have shape : 0 * (k + 1) = 0 by ring
      rw [shape, fibonacci.zero]
      exact divides.zero at 0
    . obtain ⟨j, jNat, shape⟩ := isSucc
      have hj : succ(j) = j + 1
        symm
        exact add.right_one at j
      rw [shape, hj]
      rw [shape, hj] at ih
      have expand : (j + 1) * (k + 1) = (j + 1) * k + j + 1 by ring
      rw expand
      have formula := fibonacci.add at (j + 1) * k, j
      rw formula
      have natProduct := fibonacci.natural at (j + 1) * k
      have natProduct1 := fibonacci.natural at (j + 1) * k + 1
      have natJ := fibonacci.natural at j
      have natJ1 := fibonacci.natural at j + 1
      have left : fibonacci(j + 1) ∣ fibonacci((j + 1) * k) * fibonacci(j)
        exact divides.multiply_right with ih
      have right : fibonacci(j + 1) ∣ fibonacci((j + 1) * k + 1) * fibonacci(j + 1)
        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))
      exact divides.add with left, right