Grace/Cumulus/NumberTheory/DigitSum.g17

Open in Workbench Download source

Imports

Divisibility · Core.List

Declarations

• digitsValue def
• digitSum def
• digitsValue.nil theorem derivation
• digitsValue.cons theorem derivation
• digitSum.nil theorem derivation
• digitSum.cons theorem derivation
• digitsValue.digitSum_difference theorem derivation
• digitsValue.three_divides_iff theorem derivation

Source

1-- Divisibility by three is decided by the sum of the decimal digits2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.NumberTheory.DigitSum8import Divisibility9import Core.List1011-- A list of digits, least significant first, and the number it writes.12def digitsValue (ds : List(ℕ)) → Nat13  | [] => 014  | d :: rest => add(d, mul(10, digitsValue(rest)))1516def digitSum (ds : List(ℕ)) → Nat17  | [] => 018  | d :: rest => add(d, digitSum(rest))1920theorem digitsValue.nil21  shows digitsValue([]) = 022proof23  simp2425theorem digitsValue.cons (d : Nat) (rest : List(ℕ))26  shows digitsValue(d :: rest) = d + 10 * digitsValue(rest)27proof28  unfold digitsValue29  rfl3031theorem digitSum.nil32  shows digitSum([]) = 033proof34  simp3536theorem digitSum.cons (d : Nat) (rest : List(ℕ))37  shows digitSum(d :: rest) = d + digitSum(rest)38proof39  unfold digitSum40  rfl4142-- A number exceeds its digit sum by a multiple of three, because every power43-- of ten is one more than a multiple of three.44theorem digitsValue.digitSum_difference (ds : List(ℕ))45  shows ∃ k, Nat(k) ∧ digitsValue(ds) = digitSum(ds) + 3 * k46proof47  induction ds48  | List.nil =>49    have zeroNat : Nat(0) by typecheck50    refine ⟨0, zeroNat, ?_⟩51    rw [digitsValue.nil, digitSum.nil]52    compute53  | List.cons(d, rest) using ih =>54    obtain ⟨k, kNat, equation⟩ := ih55    have witnessNat : Nat(3 * digitSum(rest) + 10 * k) by typecheck56    refine ⟨3 * digitSum(rest) + 10 * k, witnessNat, ?_⟩57    rw [digitsValue.cons, digitSum.cons, equation]58    have ten : 10 = 3 * 3 + 1 by compute59    rw ten60    ring6162-- Three divides a number exactly when it divides the sum of its digits.63theorem digitsValue.three_divides_iff (ds : List(ℕ))64  shows 3 ∣ digitsValue(ds) ↔ 3 ∣ digitSum(ds)65proof66  obtain ⟨k, kNat, equation⟩ := digitsValue.digitSum_difference at ds with *67  have self := divides.reflexive with *68  have multiple := divides.multiply_right with *69  rw equation70  constructor71  . intro whole72    exact divides.add_cancel_right at 3, digitSum(ds), 3 * k with *73  . intro digits74    exact divides.add with *75