-----Description----- 
This task requires writing a Lean 4 method that generates all possible letter combinations from a string of digits based on the traditional telephone keypad letter mappings.

-----Input-----
The input consists of a string (String). The string may be empty.

-----Output-----
The output is a list of strings (List String) where each string represents a unique combination of letters corresponding to the input digits. If the input string is empty or contains any invalid digit (not 2-9), the output is an empty list.

-----Note-----

Here is the mapping from the number to possible letters:
2: a or b or c
3: d or e or f
4: g or h or i
5: j or k or l
6: m or n or o
7: p or q or r or s
8: t or u or v
9: w or x or y or z
other number or not a number: no letters
Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux
def digitToLetters (c : Char) : List Char :=
  match c with
  | '2' => ['a', 'b', 'c']
  | '3' => ['d', 'e', 'f']
  | '4' => ['g', 'h', 'i']
  | '5' => ['j', 'k', 'l']
  | '6' => ['m', 'n', 'o']
  | '7' => ['p', 'q', 'r', 's']
  | '8' => ['t', 'u', 'v']
  | '9' => ['w', 'x', 'y', 'z']
  | _ => []
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def letterCombinations_precond (digits : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
-- !benchmark @end code_aux


def letterCombinations (digits : String) (h_precond : letterCombinations_precond (digits)) : List String :=
  -- !benchmark @start code
  let chars := digits.toList
  -- Return [] if any invalid digit exists
  if chars.any (fun c => digitToLetters c == []) then []
  else go chars
  where
    go : List Char → List String
    | [] => []
    | (d :: ds) =>
      let restCombinations := go ds
      let currentLetters := digitToLetters d
      match restCombinations with
      | [] => currentLetters.map (λ c => String.singleton c)
      | _ => currentLetters.flatMap (λ c => restCombinations.map (λ s => String.singleton c ++ s))
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def letterCombinations_postcond (digits : String) (result: List String) (h_precond : letterCombinations_precond (digits)) : Prop :=
  -- !benchmark @start postcond
  if digits.isEmpty then
    result = []
  else if digits.toList.any (λ c => ¬(c ∈ ['2','3','4','5','6','7','8','9'])) then
    result = []
  else
    let expected := digits.toList.map digitToLetters |>.foldl (λ acc ls => acc.flatMap (λ s => ls.map (λ c => s ++ String.singleton c)) ) [""]
    result.length = expected.length ∧ result.all (λ s => s ∈ expected) ∧ expected.all (λ s => s ∈ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem letterCombinations_spec_satisfied (digits: String) (h_precond : letterCombinations_precond (digits)) :
    letterCombinations_postcond (digits) (letterCombinations (digits) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: digits: 2
digits: 9
digits: 23
digits: 27
digits: 0
digits: 21
expected: a, b, c
w, x, y, z
ad, ae, af, bd, be, bf, cd, ce, cf
ap, aq, ar, as, bp, bq, br, bs, cp, cq, cr, cs
unexpected: a
b
a
b
c
w
x
y
z
a
b
c
p
q
r
s
a
b
a
b

Inputs rejected by the precondition: