-- Divisibility by three is decided by the sum of the decimal digits
-- 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.NumberTheory.DigitSum
import Divisibility
import Core.List

-- A list of digits, least significant first, and the number it writes.
def digitsValue (ds : List(ℕ)) → Nat
  | [] => 0
  | d :: rest => add(d, mul(10, digitsValue(rest)))

def digitSum (ds : List(ℕ)) → Nat
  | [] => 0
  | d :: rest => add(d, digitSum(rest))

theorem digitsValue.nil
  shows digitsValue([]) = 0
proof
  simp

theorem digitsValue.cons (d : Nat) (rest : List(ℕ))
  shows digitsValue(d :: rest) = d + 10 * digitsValue(rest)
proof
  unfold digitsValue
  rfl

theorem digitSum.nil
  shows digitSum([]) = 0
proof
  simp

theorem digitSum.cons (d : Nat) (rest : List(ℕ))
  shows digitSum(d :: rest) = d + digitSum(rest)
proof
  unfold digitSum
  rfl

-- A number exceeds its digit sum by a multiple of three, because every power
-- of ten is one more than a multiple of three.
theorem digitsValue.digitSum_difference (ds : List(ℕ))
  shows ∃ k, Nat(k) ∧ digitsValue(ds) = digitSum(ds) + 3 * k
proof
  induction ds
  | List.nil =>
    have zeroNat : Nat(0) by typecheck
    refine ⟨0, zeroNat, ?_⟩
    rw [digitsValue.nil, digitSum.nil]
    compute
  | List.cons(d, rest) using ih =>
    obtain ⟨k, kNat, equation⟩ := ih
    have witnessNat : Nat(3 * digitSum(rest) + 10 * k) by typecheck
    refine ⟨3 * digitSum(rest) + 10 * k, witnessNat, ?_⟩
    rw [digitsValue.cons, digitSum.cons, equation]
    have ten : 10 = 3 * 3 + 1 by compute
    rw ten
    ring

-- Three divides a number exactly when it divides the sum of its digits.
theorem digitsValue.three_divides_iff (ds : List(ℕ))
  shows 3 ∣ digitsValue(ds) ↔ 3 ∣ digitSum(ds)
proof
  obtain ⟨k, kNat, equation⟩ := digitsValue.digitSum_difference at ds with *
  have self := divides.reflexive with *
  have multiple := divides.multiply_right with *
  rw equation
  constructor
  . intro whole
    exact divides.add_cancel_right at 3, digitSum(ds), 3 * k with *
  . intro digits
    exact divides.add with *