iterator over list is an element of the list (lean4)

Stream: Program verification

[morphism]

Hello everyone! I am new to the lean and I am trying to prove the correctness of a simple sorting algorithm. I ran into a problem with the for loop and I hope you can point me in the right direction.

Smallest example:

def sum' (xs : List Nat) := Id.run <| do
  for x in xs do
    have h: x ∈ xs := by
      sorry -- how do I prove this?

Extended example:

def sink (xs : Array Nat) : Array Nat := Id.run <| do
  for i in [0:xs.size - 1] do
    have h: i < xs.size := by
      sorry
    have g: i + 1 < xs.size := by
      sorry
    if xs[i]'h > xs[i + 1]'g then
      let xs' := xs.swap ⟨i, h⟩ ⟨i + 1, g⟩
  return xs

My attempts

• I found some proofs of sorting algorithms, for instance in Functional Programming in Lean, this github repo or this verification course. However they do not used for loops, and I would like to learn to prove the correctness of the algorithms with for loops since it increases the readability of the definitions a lot.
• I found the doc file of do notation in lean4 but this did not help me.

My background in lean

I am a complete noob, I have just finished the numbers game and started reading Functional Programming in Lean. I would highly appreciate any help and support (including emotional since I am trying to understand this second day in a row and I feel like my hands are tied behind the back with no particular reason :sweat_smile: ). Particularly this would be perfect if you could point me to some courses/examples that cover proofs with the for loops this would be great.

P.S.
I apologize if this is not the right place to ask this type of questions if this is the case could you please point me to the right channel/website?

[Andrés Goens]

It looks like you're looking for docs#List.attach

[Daniel Weber]

You can also do

def sum' (xs : List Nat) := Id.run <| do
  for h : x in xs do
    have h: x ∈ xs := h

[Daniel Weber]

And for the extended example you can use

def sink (xs : Array Nat) : Array Nat := Id.run <| do
  for h : i in [0:xs.size - 1] do
    have f : i < xs.size - 1 := h.upper
    have h : i < xs.size := by omega
    have g : i + 1 < xs.size := by omega
    if xs[i] > xs[i + 1] then
      let xs' := xs.swap ⟨i, h⟩ ⟨i + 1, g⟩
  return xs

[morphism]

Daniel Weber писал/а:

You can also do

def sum' (xs : List Nat) := Id.run <| do
  for h : x in xs do
    have h: x ∈ xs := h

Great, thank you for this!

[morphism]

Andrés Goens писал/а:

It looks like you're looking for docs#List.attach

Thank you, will read it!