enumerate

Stream: lean4

[Adam Topaz]

What's the Lean4 idiomatic way to enumerate in a for loop (I'm thinking specifically of python's enumerate)?
The following feels too hacky!

#eval do
  let a := #["a","b","c"]
  for i in (List.range a.size).zip a.toList do
    IO.println i

[Gabriel Ebner]

You can do

for h : i in [:a.size] do
  have : i < a.size := h.2
  IO.println (i, a[i])

or

for elem in a, i in [:a.size] do
  IO.println (i, elem)

[Jannis Limperg]

What's the semantics of the second form if the two collections don't have the same size? Stop once the shorter one is exhausted?

[Adam Topaz]

Aha! I didn't know

for elem in a, i in [:a.size] do
  IO.println (i, elem)

was possible!

[Adam Topaz]

#eval do
  let a := #["a","b","c"]
  for i in a, j in [:a.size + 2] do
    IO.println (i, j)

stops at (c,2)

[Adam Topaz]

BTW, it seems that the two approaches that Gabriel mentioned cannot be combined!

#eval do
  let a := #["a","b","c"]
  for i in a, h : j in [:a.size] do
    IO.println (i, j)

[Adam Topaz]

That gives an error at h.

[Gabriel Ebner]

You can do for h : j in [:a.size], elem in a do.

[Andrés Goens]

huh, that's a strange h you get there though, I would have expected it to be the same h that you need for a[i] there, as in something like:

#eval do
  let a := #["a","b","c"]
  for h  : i in [:a.size] do
    IO.println a[i]'h

[Andrés Goens]

but there seems to be a new col : Std.range being created and no relation to a.size

[Andrés Goens]

what's the use of that h : i ∈ col?

[Mario Carneiro]

I'm getting a weird parse error there BTW, expected ':' or ']' at the i in a[i]'h. It seems to be a precedence issue, IO.println (a[i]'h) works

[Mario Carneiro]

Note that col in this example is actually a let binding, if you wrap the term in by exact you can see the value of the binding

[Gabriel Ebner]

@Andrés Goens The h here has type 0 ≤ i ∧ i < a.size (because [:a.size] means [0:a.size]).

[Mario Carneiro]

(I'm not a big fan of this pretty printing trick of making let bindings look like regular bindings. Having := ... would be better)

[Andrés Goens]

Mario Carneiro said:

Note that col in this example is actually a let binding, if you wrap the term in by exact you can see the value of the binding

I'm not sure I follow, where would I wrap it in a by exact?

[Mario Carneiro]

like by exact IO.println (a[i]'h)

[Andrés Goens]

Gabriel Ebner said:

Andrés Goens The h here has type 0 ≤ i ∧ i < a.size (because [:a.size] means [0:a.size]).

interesting, so this seems to work then from that type:

#eval do
  let a := #["a","b","c"]
  for h : i in [:a.size] do
    IO.println (a[i]'(by exact h.2))

definitely not the most intuitive tbh :sweat_smile:

[Mario Carneiro]

the reason this makes a difference is that the tactic mode uses a different pretty printing setting that shows let binding values

[Mario Carneiro]

Yes, proofs and do blocks don't play well together ATM. It needs some design work but I don't think it is a high priority right now

[Andrés Goens]

Mario Carneiro said:

the reason this makes a difference is that the tactic mode uses a different pretty printing setting that shows let binding values

Ahh, I see, that's interesting!

[Mario Carneiro]

you don't actually need the by exact for it to typecheck

[Mario Carneiro]

just if you want to see that col is actually a let binding

[Andrés Goens]

I guess you still need to know the instance : Membership Nat Range to know what h actually means, or chase it down with a bunch of unfolds, like

      unfold Membership.mem at h
      unfold inferInstance at h
      unfold Std.instMembershipNatRange at h
      simp at h

or is there a more idiomatic way to do this?

[Mario Carneiro]

you can use conv at h => whnf if you wanted to see that it is an /\ of something

[Andrés Goens]

Mario Carneiro said:

you can use conv at h => whnf if you wanted to see that it is an /\ of something

huh, that's some pretty cool black magic there :nerd:

[Andrés Goens]

thx for that one!