In do-notation for lists, providing a proof of existance

Stream: new members

[vgarzareyna]

Hi, I'm a relatively new user to Lean 4.
Recently I found myself in the situation where I want to use do-notation to act on the elements of a list. The problem is that, one of the theorems that I need to prove that the function terminates requires me to be able to show that the elements I'm working on do exist.

Here's a minimal reproduction of the situation I'm in:

def minimal_ex {α β} (as : List α) (f : List α → (a : α) → (a ∈ as) → β )  : List β
  := do
    let a <- as
    let h : a ∈ as := sorry
    pure (f as a h)

I thought it might be difficult to tackle this from a different perspective, so I tried to figure out if there was a recursive function I could define that would take a list as : List a and return a list with the same elements and a proof that the element itself exists (ahs : List (a \x h) where h would have type a ∈ as). Unfortunately I wasn't able to define the type of this function in a way that the compiler was happy with :(

Can y'all think of a way of doing this? Or is that not possible withing Lean 4's limitations.

[Aaron Liu]

Try let a <- as.attach? (docs#List.attach)

[vgarzareyna]

hahha, i guess i should've seen that coming. thanks a lot!