import Mathlib.Data.List.Basic
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic
/-!
A small, self-contained formalization of the arithmetic core of the ISIN/Luhn
check-digit rule.
Scope of the proof:
* We work on the already-expanded decimal digit payload.
* The theorem proves that the computed check digit always verifies.
This means: if the ISIN body has already been converted into a list of decimal
Digits (where letters A..Z have been expanded to 10..35 and then split into
individual decimal digits), then `computeCheckDigit` is correct w.r.t. `verify`.
The string/character parsing layer can be added on top later; the mathematically
relevant check-digit core is proved here.
-/
namespace ISIN
/-- Luhn doubling step on a single decimal digit. -/
def dblAdjust (d : Nat) : Nat :=
let m := 2 * d
if m < 10 then m else m - 9
/-- Alternating sum from left to right, with `b = true` meaning:
the current digit is processed by `dblAdjust`. -/
def altSum : Bool → List Nat → Nat
| _, [] => 0
| b, x :: xs => (if b then dblAdjust x else x) + altSum (!b) xs
/-- Starting flag for a payload of length `n` so that, after appending the
future check digit on the right, that check digit is *not* doubled and the
payload digits have exactly the correct Luhn parity. -/
def payloadStart (xs : List Nat) : Bool :=
xs.length % 2 = 1
/-- Luhn sum of the payload (already using the parity appropriate for a later
appended check digit). -/
def payloadSum (xs : List Nat) : Nat :=
altSum (payloadStart xs) xs
/-- The computed check digit. -/
def computeCheckDigit (xs : List Nat) : Nat :=
(10 - payloadSum xs % 10) % 10
/-- Verification predicate: append the candidate check digit and test whether
the total Luhn sum is divisible by 10. -/
def verify (xs : List Nat) (c : Nat) : Bool :=
decide ((altSum (payloadStart xs) (xs ++ [c])) % 10 = 0)
/-- Flag after toggling `n` times. -/
def afterFlag : Bool → Nat → Bool
| b, 0 => b
| b, n + 1 => afterFlag (!b) n
lemma afterFlag_eq_parity (b : Bool) : ∀ n : Nat,
afterFlag b n = if n % 2 = 0 then b else !b := by
intro n
induction n generalizing b with
| zero =>
simp [afterFlag]
| succ n ih =>
by_cases h : n % 2 = 0
· have h' : (n + 1) % 2 = 1 := by omega
simp [afterFlag, ih, h, h']
· have h1 : n % 2 = 1 := by omega
have h' : (n + 1) % 2 = 0 := by omega
simp [afterFlag, ih, h1, h']
lemma altSum_append_singleton (b : Bool) (xs : List Nat) (x : Nat) :
altSum b (xs ++ [x]) =
altSum b xs + (if afterFlag b xs.length then dblAdjust x else x) := by
induction xs generalizing b with
| nil =>
simp [altSum, afterFlag]
| cons y ys ih =>
simp [altSum, ih, afterFlag, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
lemma after_payloadStart_false_len (n : Nat) :
afterFlag (n % 2 = 1) n = false := by
rw [afterFlag_eq_parity]
by_cases h : n % 2 = 0
· simp [h]
· have h1 : n % 2 = 1 := by omega
simp [h1]
lemma after_payloadStart_false (xs : List Nat) :
afterFlag (payloadStart xs) xs.length = false := by
unfold payloadStart
exact after_payloadStart_false_len xs.length
lemma fullSum_eq_payload_plus_check (xs : List Nat) (c : Nat) :
altSum (payloadStart xs) (xs ++ [c]) = payloadSum xs + c := by
unfold payloadSum
rw [altSum_append_singleton]
simp [after_payloadStart_false]
lemma mod_add_checkDigit (s : Nat) :
(s + ((10 - s % 10) % 10)) % 10 = 0 := by
let r := s % 10
have hr : s % 10 = r := rfl
have hr_lt : r < 10 := by
dsimp [r]
exact Nat.mod_lt _ (by decide)
rw [Nat.add_mod, hr, Nat.mod_mod]
by_cases h0 : r = 0
· simp [h0]
· have hr_pos : 0 < r := Nat.pos_of_ne_zero h0
have hsub_lt : 10 - r < 10 := by omega
rw [Nat.mod_eq_of_lt hsub_lt]
have hsum : r + (10 - r) = 10 := by omega
rw [hsum]
theorem fullSum_compute_mod (xs : List Nat) :
(altSum (payloadStart xs) (xs ++ [computeCheckDigit xs])) % 10 = 0 := by
rw [fullSum_eq_payload_plus_check, computeCheckDigit]
exact mod_add_checkDigit (payloadSum xs)
theorem verify_compute_eq_true (xs : List Nat) :
verify xs (computeCheckDigit xs) = true := by
unfold verify
simp [fullSum_compute_mod]
/-!
Regression checks on a well-known example.
US0378331005 (Apple) has body US037833100.
Expanded decimal payload: [3,0,2,8,0,3,7,8,3,3,1,0,0].
-/
example : computeCheckDigit [3, 0, 2, 8, 0, 3, 7, 8, 3, 3, 1, 0, 0] = 5 := by
decide
example : verify [3, 0, 2, 8, 0, 3, 7, 8, 3, 3, 1, 0, 0] 5 = true := by
decide
end ISIN
