proof of for loop idx bound

Stream: lean4

[Quinn]

I can write

Id.run do for i in [0:10] do ...

is there a way to name the fact, which lean presumably knows, that 0<=i<10?

I can explore the ForIn construct, but I thought I'd check if anyone has some code lying around that does this. I'm accessing and updating an array inside the for loop, and trying to eliminate !

[Kim Morrison]

for h : i in [0:10] do

[Quinn]

oh that's so cool

[Quinn]

having a bunch of trouble converting the context which says that col : Std.Range := { start, stop, step } and i \in col into the Fin constructor.

[Kim Morrison]

Note sure what you are saying. Could you post a #mwe?

[Quinn]

yes, sry

[Quinn]

def f := Id.run do
  let mut result := Array.mkArray 10 0
  for h : i in [0:10] do
    have ifin : i < result.size := by
      sorry
    let fini : Fin result.size := ⟨i, ifin⟩
    result := result.set fini i

[Quinn]

the sorry

[Quinn]

my usual have trick for getting col out of grey'd out dagger notation isn't working

[Quinn]

rather, I do

      have ⟨start, stop, step⟩ := col
      have result : Array Nat := mkArray 10 0

but result is grey'd out / dagger so I can't show that stop = result.size

[Kim Morrison]

The problem here is that as soon as you use Array.set, you need a lemma to know the size is the same as before.

[Kim Morrison]

Consider using Vector here. (You may need to be on a nightly release, or otherwise import Batteries.)