Array bounds in for loops

Stream: lean4

[Frédéric Dupuis]

In the following code, I get an error because Lean can't get a proof that the array index i is within the bounds:

def doNothing [Inhabited α] (as : Array α) : Array α := Id.run do
  let mut r := #[]
  for i in [0:as.size] do
    r := r.push as[i]
  return r

Is there a way to gain access to some h : i ∈ [0:as.size] in that loop?

[Kyle Miller]

def doNothing [Inhabited α] (as : Array α) : Array α := Id.run do
  let mut r := #[]
  for h : i in [0:as.size] do
    r := r.push (as[i]'h.2)
  return r

[Kyle Miller]

I feel like r := r.push as[i] should work without needing to give a proof, but at least there's a way to write it.

[Frédéric Dupuis]

Yeah, it seems like this should be added to the default tactic somehow.

[Alex J. Best]

If you don't need the index for something else you can also do

def doNothing [Inhabited α] (as : Array α) : Array α := Id.run do
  let mut r := #[]
  for a in as do
    r := r.push a
  return r

btw

[Frédéric Dupuis]

I do need the index for my real application though!

[Patrick Massot]

Note that if this becomes annoying you can extend the tactic that tries to discharge those side conditions.

[Thomas Murrills]

This thread is relevant and has a specific partial solution for this case by extending that tactic!

[Min-Hsien Weng]

Alex J. Best said:

def doNothing [Inhabited α] (as : Array α) : Array α := Id.run do
  let mut r := #[]
  for a in as do
    r := r.push a
  return r

Good example.
I'm curious if the doNothing function can accept a mutable reference to the input array as, similar to Rust. This would allow us to directly modify the input array as instead of creating a new one. :thinking:

Does the mut in Lean have a similar meaning to mut in Rust that refer to mutable variable or mutable references?

[Alex J. Best]

mut in a do block indeed marks a variable as mutable, but do blocks like this are really syntactic sugar for more fundamental functional operations like a fold, so what happens under the hood may not exactly be a mutable variable, see https://lean-lang.org/papers/do.pdf.
As for marking a variable input to a function as mutable thats also not really possible in a functional language strictly speaking, what lean 4 does make use of is tracking reference counts to avoid reallocating objects, which can acheive a lot of the benefits of using mutable variables, https://arxiv.org/pdf/1908.05647.pdf, its up to the programmer to try and debug whether this is happening though if things are performance critical

[Min-Hsien Weng]

Alex J. Best said:

mut in a do block indeed marks a variable as mutable, but do blocks like this are really syntactic sugar for more fundamental functional operations like a fold, so what happens under the hood may not exactly be a mutable variable, see https://lean-lang.org/papers/do.pdf.
As for marking a variable input to a function as mutable thats also not really possible in a functional language strictly speaking, what lean 4 does make use of is tracking reference counts to avoid reallocating objects, which can acheive a lot of the benefits of using mutable variables, https://arxiv.org/pdf/1908.05647.pdf, its up to the programmer to try and debug whether this is happening though if things are performance critical

Awesome! Thanks for sharing great papers. Indeed, Lean is designed to produce purely functional code that can be easily reasoned and verified. Reference counting (RC) is a good fit for Lean because it is a purely functional programming language. Since variables are immutable, RC can be easily optimized to improve performance.

[Joachim Breitner]

Patrick Massot said:

Note that if this becomes annoying you can extend the tactic that tries to discharge those side conditions.

I RFC’ed this at https://github.com/leanprover/lean4/issues/3032