Array and other beginner questions

Stream: new members

[Tom]

Hi,

After a couple of years, I finally have time to come back to Lean. I'm re-reading the docs and David Christiansen's FPiL and just experimenting with some trivial code. I would appreciate any help with my questions below:

1) Why does the for syntax require a Nat rather than just a numeric type? (And I would hope/expect ii to be of that type).

def fill_arr1 (n : UInt64) : Id (Array UInt64) := do
  let mut a := Array.mkEmpty (α := UInt64) n.toNat
  for i in [0:n.toNat] do                  --< Here - why can't I say `n`
    a := a.push (UInt64.ofNat i)   --< ... and now I have to do a conversion
  pure a

2) Speaking of for, my understanding is that this is just a syntax /macro. Is there a way to jump to its definition (VS Code)? I don't seem to be able to find it.

I also added the following (somewhat non-sensical) code:

def fill_arr2 (n : UInt64) : Id (Array UInt64) := do
  let mut a := fill_arr1 n
  for i in [0:a.size] do
    if h: i < a.size then
      let jj : Fin a.size := ⟨i, h⟩;
      a := a.set jj 10
  pure a

3) Why does a.size return a Nat rather than a Fin a.size type? That way (and in combination with the for question) I seem to be forced to do unnecessary checking and conversions.

4) Is there a way to "hoist" the a.size check outsize of the loop rather than doing it on every element access? I understand perhaps I could use a higher-order approach like a fold etc, but I can't see how to do it with this style of programming.

5) Is there a way to "reuse" a.size, e.g.

def fill_arr3 (n : UInt64) : Id (Array UInt64) := do
  let mut a := fill_arr1 n
  let as := a.size
  for i in [0:as] do
      if h: i < as then
        let jj : Fin as := ⟨i, h⟩;
        a := a.set jj 10  --< This line is not happy
  pure a

I kind of "get" why this doesn't work but this makes me think of something like abbrev at the top level.

Sorry for all the questions and thank you for your help!

Tom

[Eric Wieser]

Tom said:

Why does a.size return a Nat rather than a Fin a.size type? That way (and in combination with the for question) I seem to be forced to do unnecessary checking and conversions.

This wouldn't make sense, because Fin a.size only goes up to a.size - 1. Perhaps you want the for h : i in [0:a.size] do syntax instead, but I think in your example you're still in trouble because the a.size in the first loop might not be the same as the next loop

[Eric Wieser]

This works:

import Batteries

def fill_arr1 (n : UInt64) : Id (Array UInt64) := do
  let mut a := Array.mkEmpty (α := UInt64) n.toNat
  for i in [0:n.toNat] do                  --< Here - why can't I say `n`
    a := a.push (UInt64.ofNat i)   --< ... and now I have to do a conversion
  pure a

def fill_arr2 (n : UInt64) : Id (Array UInt64) := do
  let mut a : Batteries.Vector _ _ := ⟨fill_arr1 n, rfl⟩
  for h : i in [0:a.size] do
    let jj : Fin a.size := ⟨i, h.2⟩
    a := a.set jj 10
  pure a.toArray

[Eric Wieser]

The trick here is that Batteries.Vector promises up front that the size remains unchanged on each loop iteration

[Tom]

Hi @Eric Wieser ,

Thank for your help. I appreciate you pointing out the fallacy with Fin. I guess I confused myself wondering about my question 2) about the return type of for (e.g. returning Fin instead of Nat) and then trying to shoe-horn that in.

I was not aware of the for h:... syntax, thanks for pointing that out.

because the a.size in the first loop might not be the same as the next loop

I am not sure if you mean this "in general" (in which case I agree), or in the specific example of my original fill_arr2 (in which case I'm not sure I understand).

Thank you!

[Eric Wieser]

I indeed mean in general, but if you want to tell Lean that in your specific example it's fine, you need to bundle that proof with a, which is exactly what you get from Vector there