Advice on writing idiomatic Lean4

Stream: new members

[Will Bradley]

How close are each of these small programs to idiomatic Lean? One I wrote like I would in C (imperatively), the other functionally. Thanks so much

Program 1:

-- count six-digit numbers whose digits sum to 10
def main : IO Unit := do
  let mut count := 0
  for n in [100000 : 1000000] do
    let mut n' := n
    let mut sum := 0
    while n' ≠ 0 do
      sum := sum + n' % 10
      if sum > 10 then break
      n' := n' / 10
    if sum = 10 then
      count := count + 1
  IO.println count

Program 2:

-- [start, stop)
def List.range2 (start stop: Nat): List Nat :=
  List.range (stop - start) |>.map (. + start)

-- count six-digit numbers whose digits sum to 10
def main : IO Unit :=
  let answer := List.range2 (Nat.pow 10 5) (Nat.pow 10 6)
    |>.filter (
      fun n =>
        let digits_sum := Nat.toDigits 10 n
          |>.map (Char.toNat . - '0'.toNat)
          |>.foldl Nat.add 0
        digits_sum = 10)
    |>.length
  IO.println answer

[Kyle Miller]

Instead of Nat.pow, it's customary to use ^.

For style, I probably would format the second one like

def main : IO Unit :=
  let answer :=
    List.range2 (10 ^ 5) (10 ^ 6)
    |>.filter (fun n =>
        let digits := Nat.toDigits 10 n |>.map (Char.toNat · - '0'.toNat)
        digits.foldl (· + ·) 0 = 10)
    |>.length
  IO.println answer

I feel like it's better to name intermediate results rather than using long pipelines. I could have also named digits_sum here, but digits.foldl (· + ·) 0 is a clear enough fold.

That said, it's better to make small helper functions. Mathlib has functions such as docs#Nat.digits and docs#List.sum already, and you could define these too.

[Kyle Miller]

Here's how you can avoid turning digits into characters and back:

def main : IO Unit :=
  let answer := List.range2 (10 ^ 5) (10 ^ 6) |>.map digitSum |>.filter (· = 10) |>.length
  IO.println answer
where
  digitSum (n : Nat) : Nat :=
    if n = 0 then
      0
    else
      (n % 10) + digitSum (n / 10)

[Kyle Miller]

Or rather than filtering and taking the length, there's docs#List.count from std:

def main : IO Unit :=
  let answer := List.range2 (10 ^ 5) (10 ^ 6) |>.map digitSum |>.count 10
  IO.println answer
where
  digitSum (n : Nat) : Nat :=
    if n = 0 then
      0
    else
      (n % 10) + digitSum (n / 10)

[Kyle Miller]

Though you could make digitSum be tail recursive by having it accumulate:

  digitSum (n : Nat) (acc : Nat := 0) : Nat :=
    if n = 0 then
      acc
    else
      digitSum (n / 10) (acc + n % 10)