Idiomatic nestes for loops

Stream: lean4

[Alcides Fonseca]

I was doing the Advent of Code day 5, and I came across a problem where I would have to iterate a large board and compute something "heavy" for each pair (x, y). To avoid spoilers and simplify the problem, I am just computing if x = y for each position, and counting how many diagonals there are for x and y in [0:10000]. (For those who have done the problem, I know this is not the most efficient approach for the board given, but I don't care right now).

I've implemented three versions:

• a naive recursive function, which stacks overflow.
• a tail recursive function, which is faster
• an IO version that uses for _ in [1:100000+1], which is slightly faster than the tail recursive.

Source: https://gist.github.com/alcides/9fe28137561cca3fb708d1cb2ea8eeda

First of all, props to Leo&Cia for implementing the for in. But I was wondering if there is anyway I can do it without the function having the IO Monad, and if there was a more idiomatic/faster way of doing this.

Another question: is there anything like Haskell's trace for lean4, where we can print things without having to change everything up the stack to be IO?

[Marc Huisinga]

But I was wondering if there is anyway I can do it without the function having the IO Monad, and if there was a more idiomatic/faster way of doing this.

You should be able to use do, forand let mut even in pure functions. E.g.

def foo (n : Nat) : Nat := do
  let mut r := 1
  for i in [1:n+1] do
    r := r * i
  return r

#eval foo 3

is there anything like Haskell's trace for lean4

dbgTrace and dbgTraceVal are what you're looking for. If you're doing performance debugging, dbgTraceIfShared is also helpful.

[Alcides Fonseca]

Simpler than I thought. Now I went back to the docs to see how to improve them, but I found exactly that solution in sum'. Sorry for bothering with that.

And thanks for the dbgTrace, that's exactly what I was looking for. But since it breaks tail recursion, I can only use it in the base case. But it works wonders in the for-in version! Guess that's the one I'll be using in the future.

[Marc Huisinga]

One issue with using dbgTrace in for loops is that reassignments below the dbgTrace won't work anymore. I usually just use dbgTraceVal :)

[Sebastian Ullrich]

dbg_trace should fix that!

[Marc Huisinga]

That one doesn't show up in CTRL+Space autocomplete :grinning_face_with_smiling_eyes:

[Sebastian Ullrich]

True, macros do not show up there... yet. It is, however, mentioned in https://leanprover.github.io/lean4/doc/dev/debugging.html :) .