-- The central binomial coefficients and the Catalan numbers: positivity,
-- parity, the step 2n choose n → 2n + 2 choose n + 1 in product form, the
-- closed form (n + 1) · catalan(n) = 2n choose n, the recurrence
-- (n + 2) · catalan(n + 1) = 2(2n + 1) · catalan(n), monotonicity, and the
-- bound catalan(n) ≤ 4 ^ 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.Catalan
import Vandermonde

theorem choose.central_positive (n : Nat)
  shows 0 < (2 * n) choose n
proof
  have le : n ≤ 2 * n by arith
  exact choose.positive with le

theorem choose.central_le_pow (n : Nat)
  shows (2 * n) choose n ≤ 4 ^ n
proof
  have bound := choose.le_pow at 2 * n, n
  have square := pow.mul_exponent at 2, 2, n
  have four : 2 ^ 2 = 4 by compute
  rw four at square
  rw square
  exact bound

-- Pascal's rule and symmetry: 2n + 2 choose n + 1 = 2 · (2n + 1 choose n).
theorem choose.central_double (n : Nat)
  shows (2 * (n + 1)) choose (n + 1) = 2 * ((n + 1 + n) choose (n + 1))
proof
  have shape : 2 * (n + 1) = (n + 1 + n) + 1 by ring
  rw [shape, choose.pascal]
  have mirror := choose.add_symmetric at n + 1, n
  rw mirror
  have cNat := choose.natural at n + 1 + n, n + 1
  ring

theorem choose.central_even (n : Nat)
  shows Even((2 * (n + 1)) choose (n + 1))
proof
  rw choose.central_double
  have cNat := choose.natural at n + 1 + n, n + 1
  exact Even.two_mul at (n + 1 + n) choose (n + 1)

-- The step between consecutive central coefficients, in product form.
theorem choose.central_step (n : Nat)
  shows (n + 1) * ((2 * (n + 1)) choose (n + 1)) =
    2 * (2 * n + 1) * ((2 * n) choose n)
proof
  rw choose.central_double
  have absorb := choose.absorption_at at 2 * n, n
  have shape : 2 * n + 1 = n + 1 + n by ring
  rw shape at absorb
  have cNat := choose.natural at n + 1 + n, n + 1
  have centralNat := choose.natural at 2 * n, n
  rw shape
  ring [absorb]

-- The entry next to the centre:
-- (n + 1) · (2n choose n + 1) = n · (2n choose n).
theorem choose.central_next (n : Nat)
  shows (n + 1) * ((2 * n) choose (n + 1)) = n * ((2 * n) choose n)
proof
  have step := choose.central_step at n
  rw choose.central_double at step
  have inner := choose.pascal at 2 * n, n
  have shape : 2 * n + 1 = n + 1 + n by ring
  rw shape at inner
  rw inner at step
  have aNat := choose.natural at 2 * n, n
  have bNat := choose.natural at 2 * n, n + 1
  have balanced : 2 * ((n + 1) * ((2 * n) choose (n + 1))) +
      2 * (n + 1) * ((2 * n) choose n) =
      2 * (n * ((2 * n) choose n)) + 2 * (n + 1) * ((2 * n) choose n)
    ring [step]
  have cancelled := add.right_cancel with balanced
  have twoPositive : 0 < 2 by arith
  have two := Less.ne_zero_of_positive with twoPositive
  exact mul.left_cancel_positive with two, cancelled

theorem choose.central_next_lt (n : Nat)
  shows (2 * n) choose (n + 1) < (2 * n) choose n
proof
  have next := choose.central_next at n
  have aNat := choose.natural at 2 * n, n
  have bNat := choose.natural at 2 * n, n + 1
  have positive := choose.central_positive at n
  have strict : n * ((2 * n) choose n) < (n + 1) * ((2 * n) choose n)
    have below : n < n + 1 by arith
    have nonzero := Less.ne_zero_of_positive with positive
    exact Less.mul_right with nonzero, below
  rw ← next at strict
  have gapPositive : 0 < n + 1 by arith
  have gap := Less.ne_zero_of_positive with gapPositive
  exact Less.mul_left_cancel_positive with gap, strict

theorem choose.central_monotone (n : Nat)
  shows (2 * n) choose n ≤ (2 * (n + 1)) choose (n + 1)
proof
  have step := choose.central_step at n
  have aNat := choose.natural at 2 * n, n
  have bNat := choose.natural at 2 * (n + 1), n + 1
  have coefficient : n + 1 ≤ 2 * (2 * n + 1) by arith
  have scaled := LessEqual.mul_right at n + 1, 2 * (2 * n + 1), (2 * n) choose n
    with coefficient
  rw ← step at scaled
  have nonzeroPositive : 0 < n + 1 by arith
  have nonzero := Less.ne_zero_of_positive with nonzeroPositive
  exact LessEqual.mul_left_cancel_positive with nonzero, scaled

theorem choose.central_strict (n : Nat)
  shows (2 * n) choose n < (2 * (n + 1)) choose (n + 1)
proof
  have step := choose.central_step at n
  have aNat := choose.natural at 2 * n, n
  have bNat := choose.natural at 2 * (n + 1), n + 1
  have positive := choose.central_positive at n
  have nonzero := Less.ne_zero_of_positive with positive
  have coefficient : n + 1 < 2 * (2 * n + 1) by arith
  have scaled := Less.mul_right at n + 1, 2 * (2 * n + 1), (2 * n) choose n
    with nonzero, coefficient
  rw ← step at scaled
  have gapPositive : 0 < n + 1 by arith
  have gap := Less.ne_zero_of_positive with gapPositive
  exact Less.mul_left_cancel_positive with gap, scaled

-- The Catalan numbers in closed form, 2n choose n − 2n choose n + 1.
def catalan (n : Nat) : Nat := ((2 * n) choose n) - ((2 * n) choose (n + 1))

theorem catalan.value (n : Nat)
  shows catalan(n) = ((2 * n) choose n) - ((2 * n) choose (n + 1))
proof
  simp [catalan]

theorem catalan.zero
  shows catalan(0) = 1
proof
  compute

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

theorem catalan.two
  shows catalan(2) = 2
proof
  compute

theorem catalan.three
  shows catalan(3) = 5
proof
  compute

theorem catalan.four
  shows catalan(4) = 14
proof
  compute

theorem catalan.five
  shows catalan(5) = 42
proof
  compute

theorem catalan.natural (n : Nat)
  shows Nat(catalan(n))
proof
  rw catalan.value
  have aNat := choose.natural at 2 * n, n
  have bNat := choose.natural at 2 * n, n + 1
  exact sub.closed at (2 * n) choose n, (2 * n) choose (n + 1)

-- (n + 1) · catalan(n) = 2n choose n.
theorem catalan.closed (n : Nat)
  shows (n + 1) * catalan(n) = (2 * n) choose n
proof
  rw [catalan.value, sub.mul_left, choose.central_next]
  have cNat := choose.natural at 2 * n, n
  have expand : (n + 1) * ((2 * n) choose n) =
    n * ((2 * n) choose n) + ((2 * n) choose n) by ring
  rw expand
  exact sub.add_left at (2 * n) choose n, n * ((2 * n) choose n)

theorem catalan.positive (n : Nat)
  shows 0 < catalan(n)
proof
  have closed := catalan.closed at n
  have central := choose.central_positive at n
  rw ← closed at central
  have cNat := catalan.natural at n
  have iff := mul.positive_iff at n + 1, catalan(n)
  have both := iff.forward with central
  exact both.right

theorem catalan.ge_one (n : Nat)
  shows 1 ≤ catalan(n)
proof
  have positive := catalan.positive at n
  have cNat := catalan.natural at n
  arith

theorem catalan.le_central (n : Nat)
  shows catalan(n) ≤ (2 * n) choose n
proof
  rw catalan.value
  have aNat := choose.natural at 2 * n, n
  have bNat := choose.natural at 2 * n, n + 1
  exact sub.le_self at (2 * n) choose n, (2 * n) choose (n + 1)

theorem catalan.le_pow (n : Nat)
  shows catalan(n) ≤ 4 ^ n
proof
  have first := catalan.le_central at n
  have second := choose.central_le_pow at n
  have cNat := catalan.natural at n
  have centralNat := choose.natural at 2 * n, n
  have powNat := pow.closed at 4, n
  exact LessEqual.transitive with first, second

-- Segner's recurrence in product form: (n + 2) · C(n + 1) = 2(2n + 1) · C(n).
theorem catalan.recurrence (n : Nat)
  shows (n + 2) * catalan(n + 1) = 2 * (2 * n + 1) * catalan(n)
proof
  have closedNext := catalan.closed at n + 1
  have closed := catalan.closed at n
  have step := choose.central_step at n
  rw [← closedNext, ← closed] at step
  have aNat := catalan.natural at n
  have bNat := catalan.natural at n + 1
  have balanced : (n + 1) * ((n + 2) * catalan(n + 1)) =
    (n + 1) * (2 * (2 * n + 1) * catalan(n)) by ring [step]
  have nonzeroPositive : 0 < n + 1 by arith
  have nonzero := Less.ne_zero_of_positive with nonzeroPositive
  exact mul.left_cancel_positive with nonzero, balanced

theorem catalan.monotone (n : Nat)
  shows catalan(n) ≤ catalan(n + 1)
proof
  have recurrence := catalan.recurrence at n
  have aNat := catalan.natural at n
  have bNat := catalan.natural at n + 1
  have coefficient : n + 2 ≤ 2 * (2 * n + 1) by arith
  have scaled := LessEqual.mul_right at n + 2, 2 * (2 * n + 1), catalan(n)
    with coefficient
  rw ← recurrence at scaled
  have nonzeroPositive : 0 < n + 2 by arith
  have nonzero := Less.ne_zero_of_positive with nonzeroPositive
  exact LessEqual.mul_left_cancel_positive with nonzero, scaled

theorem catalan.strict (n : Nat)
  shows catalan(n + 1) < catalan(n + 2)
proof
  have recurrence := catalan.recurrence at n + 1
  have aNat := catalan.natural at n + 1
  have bNat := catalan.natural at n + 1 + 1
  have positive := catalan.positive at n + 1
  have nonzero := Less.ne_zero_of_positive with positive
  have coefficient : n + 1 + 2 < 2 * (2 * (n + 1) + 1) by arith
  have scaled := Less.mul_right at n + 1 + 2, 2 * (2 * (n + 1) + 1),
    catalan(n + 1) with nonzero, coefficient
  rw ← recurrence at scaled
  have shape : n + 1 + 1 = n + 2 by ring
  rw shape at scaled
  have gapPositive : 0 < n + 1 + 2 by arith
  have gap := Less.ne_zero_of_positive with gapPositive
  exact Less.mul_left_cancel_positive with gap, scaled

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

theorem catalan.two_le (n : Nat)
  shows 2 ≤ catalan(n + 2)
proof
  have bound := catalan.le_of_le at 2, n
  have shape : 2 + n = n + 2 by ring
  rw [shape, catalan.two] at bound
  exact bound

-- The convolution ∑_{i < k} catalan(i) · catalan(n − i) of Segner's
-- recurrence; the instances below are checked by computation.
def catalanConvolution (n k : Nat) → Nat
  | n, zero => 0
  | n, succ(k) => catalanConvolution(n, k) + catalan(k) * catalan(sub(n, k))
  descends k

theorem catalanConvolution.zero (n : Nat)
  shows catalanConvolution(n, 0) = 0
proof
  simp [catalanConvolution]

theorem catalanConvolution.succ (n k : Nat)
  shows catalanConvolution(n, k + 1) =
    catalanConvolution(n, k) + catalan(k) * catalan(n - k)
proof
  have hk : k + 1 = succ(k) := add.right_one with *
  rw hk
  simp [catalanConvolution]

theorem catalanConvolution.natural (n k : Nat)
  shows Nat(catalanConvolution(n, k))
proof
  induction k
  | zero =>
    rw catalanConvolution.zero
    typecheck
  | j + 1 using ih =>
    rw catalanConvolution.succ
    have aNat := catalan.natural at j
    have subNat := sub.closed at n, j
    have bNat := catalan.natural at n - j
    typecheck

theorem catalan.convolution_two
  shows catalan(3) = catalanConvolution(2, 3)
proof
  compute

theorem catalan.convolution_three
  shows catalan(4) = catalanConvolution(3, 4)
proof
  compute

theorem catalan.convolution_four
  shows catalan(5) = catalanConvolution(4, 5)
proof
  compute