Code reviews

Stream: general

[Vincent Beffara]

Hi,
Is there a natural place here on the Zulip server to post requests for comments on lean code? I'm thinking of things longer than a few lines, but not yet suitable for a PR.

[Alex J. Best]

Posting here would be fine, you can always open a draft PR though and link to it from here asking for comments, that might be easier for people to comment on then

[Johan Commelin]

@Vincent Beffara If it's related to a PR, then the #PR reviews stream might also be a good fit

[Cole Shepherd]

I've written a simple number guessing game in Lean 4 in the imperative style. Does anyone have suggestions for improvements? I wanted to use a repeat do block in readGuess but I couldn't get it to work (I have another post about this). I also would like to use a bounded natural number type for the guess & answer, but Fin doesn't support arbitrary lower bounds (I want a Fin minAns maxAns) and I don't know enough about programming with dependent types to implement this yet.

def minAns := 1
def maxAns := 100

mutual

partial def main : IO Unit := do
  IO.println "Number Guessing Game in Lean 4"
  IO.println "==============================\n"

  let ans <- IO.rand minAns maxAns
  let mut numGuesses := 0

  repeat do
    IO.println s!"Guess a number from {minAns} to {maxAns}."
    let guess <- readGuess
    IO.println ""

    numGuesses := numGuesses + 1

    if guess == ans then
      IO.println s!"Congratulations, you're correct! You guessed {numGuesses} times.\n"
      break
    else if guess < ans then
      IO.println "Your guess is too low.\n"
    else
      IO.println "Your guess is too high.\n"

partial def readGuess : IO Nat := do
  let stdin <- IO.getStdin

  let guess? :=
       (<- stdin.getLine)
    |> String.dropRightWhile (p := Char.isWhitespace)
    |> String.toNat?

  if let some guess := guess? then
    if guess >= minAns && guess <= maxAns then
      return guess

  IO.println "Your guess is invalid.\n"
  readGuess

end

[Kyle Miller]

I made some small changes, partly to show some features, partly out of personal style.

1. There's a nice chained method notation you can use for guess?
2. I like to avoid mutual blocks involving partial functions since it can be less clear if there's accidentally an infinite loop somewhere.
3. I moved the minAns/maxAns constants into main and passed them as parameters to readGuess. Global constants aren't as bad as global variables, but this lets you more easily play the game with different bounds at runtime.
4. As an example of a dependent type, I made readGuess take in a proof that minAns <= maxAns. It doesn't use the proof, but it guarantees that anyone who calls readGuess must prove that there's a number the user can actually provide that will leave the loop.

/-- Takes a proof that `minAns ≤ maxAns` to guarantee the user can provide some answer! -/
partial def readGuess (minAns maxAns : Nat) (h : minAns ≤ maxAns) : IO Nat := do
  let stdin ← IO.getStdin

  let guess? := (← stdin.getLine) |>.dropRightWhile Char.isWhitespace |>.toNat?

  if let some guess := guess? then
    if guess >= minAns && guess <= maxAns then
      return guess

  IO.println s!"Your guess should be in the range {minAns} to {maxAns}.\n"
  readGuess minAns maxAns h

partial def main : IO Unit := do
  let minAns := 1
  let maxAns := 100

  IO.println "Number Guessing Game in Lean 4"
  IO.println "==============================\n"

  let ans ← IO.rand minAns maxAns

  let mut numGuesses := 0

  repeat do
    IO.println s!"Guess a number from {minAns} to {maxAns}."
    let guess ← readGuess minAns maxAns (by simp)
    IO.println ""

    numGuesses := numGuesses + 1

    if guess == ans then
      IO.println s!"Congratulations, you're correct! You guessed {numGuesses} times.\n"
      break
    else if guess < ans then
      IO.println "Your guess is too low.\n"
    else
      IO.println "Your guess is too high.\n"

[Kyle Miller]

Here's an implementation that uses a type NatRange lo hi for natural numbers in the range lo .. hi inclusive:

/-- Natural numbers that must be in the range `lo .. hi` inclusive. -/
structure NatRange (lo hi : Nat) where
  n : Nat
  lo_le : lo ≤ n
  le_hi : n ≤ hi

instance : BEq (NatRange lo hi) where
  beq r1 r2 := r1.n == r2.n

instance : LT (NatRange lo hi) where
  lt r1 r2 := r1.n < r2.n

instance : LE (NatRange lo hi) where
  le r1 r2 := r1.n ≤ r2.n

-- Copied these incantations from `Fin`.
-- These make it so that you can use `<` and `≤` in `if` statements.
instance (a b : NatRange lo hi) : Decidable (LT.lt a b) := Nat.decLt ..
instance (a b : NatRange lo hi) : Decidable (LE.le a b) := Nat.decLe ..

/-- Try to make a `NatRange` in the given range, returning `none` otherwise. -/
def NatRange.mk? {lo hi : Nat} (n : Nat) : Option (NatRange lo hi) :=
  if h : lo ≤ n ∧ n ≤ hi then
    some { n, lo_le := h.left, le_hi := h.right }
  else
    none

/-- The lower bound of the range. -/
def NatRange.lower {lo hi : Nat} (h : lo ≤ hi) : NatRange lo hi :=
  { n := lo, lo_le := by simp, le_hi := h }

def NatRange.rand (lo hi : Nat) (h : lo ≤ hi) : IO (NatRange lo hi) := do
  let n ← IO.rand lo hi
  -- The `IO.rand` function doesn't have any proofs that its result is
  -- in the correct range, so just in case it's out of range we return some default value.
  return (NatRange.mk? n).getD (NatRange.lower h)

/-- Takes a proof that `minAns ≤ maxAns` to guarantee the user can provide some answer! -/
partial def readGuess (minAns maxAns : Nat) (h : minAns ≤ maxAns) : IO (NatRange minAns maxAns) := do
  let stdin ← IO.getStdin

  let guess? := (← stdin.getLine) |>.dropRightWhile Char.isWhitespace |>.toNat?

  if let some guess := guess? then
    -- Showing off that the expected type can be used to fill in the implicit arguments to `NatRange.mk?`:
    if let some (n : NatRange minAns maxAns) := NatRange.mk? guess then
      return n

  IO.println s!"Your guess should be in the range {minAns} to {maxAns}.\n"
  readGuess minAns maxAns h

partial def main : IO Unit := do
  let minAns := 1
  let maxAns := 100

  IO.println "Number Guessing Game in Lean 4"
  IO.println "==============================\n"

  let ans ← NatRange.rand minAns maxAns (by simp)

  let mut numGuesses := 0

  repeat do
    IO.println s!"Guess a number from {minAns} to {maxAns}."
    let guess ← readGuess minAns maxAns (by simp)
    IO.println ""

    numGuesses := numGuesses + 1

    if guess == ans then
      IO.println s!"Congratulations, you're correct! You guessed {numGuesses} times.\n"
      break
    else if guess < ans then
      IO.println "Your guess is too low.\n"
    else
      IO.println "Your guess is too high.\n"

[Cole Shepherd]

This is really great, thank you!!