Asserting that `x ∈ ls` for `x` in `ls.map fun x =>`

Stream: new members

[Ayhon]

I've found myself in the need to prove that, inside a function passed to List.map, the elements passed to the function belong to the list. This could be achieved using the auxiliary lemma List.exists_of_mem_map: ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {l : List α} {b : α_1}, b ∈ List.map f l → ∃ a ∈ l, f a = b, except that I need this fact to be true and accessible from whithin the function itself.

For a simplified example, consider the implementation of the following function.

import Batteries.Data.Vector.Basic
open Batteries

variable{size: Nat}{α : Type}

def collectEven(v: Vector α (2*size)): Vector α size :=
  let indices := List.range size
  let data := indices.map fun i =>
    v[2*i] -- map_function
  Vector.mk ⟨data⟩ $ by sorry

Ignoring the sorry at the end, Lean4 refused to accept the current execution since it's unable to ascertain that the elements in indicesare in fact less than size. We can obtain ∀ i, i ∈ List.range size -> i < size from List.mem_range, but I'm unsure of how to obtain that i ∈ indices from within the function marked as map_function in the code.

Am I approaching this the wrong way? Is there an easier way to solve this problem?

[Kyle Miller]

docs#List.attach is useful here

def collectEven (v: Vector α (2*size)): Vector α size :=
  let indices := List.range size
  let data := indices.attach.map fun i =>
    v[2*i.1]'(by have := i.2; simp [indices] at this; omega)
  Vector.mk ⟨data⟩ $ by simp [data, indices]

[Ayhon]

This is it! Thanks a lot!

[Ayhon]

Out of curiosity, how could I have found this method on my own? I tried using Loogle or simply looking at the List implementation, but couldn't find anything relevant. Is this simply due to inexperience?

[Kyle Miller]

I learned about .attach at some point by seeing it used, maybe here on Zulip.

[Kyle Miller]

I first saw docs#Finset.attach and figured List would have it too.

[Eric Wieser]

Was having x ∈ ls available as an argument to ls.map ever considered? If so, it might make sense for the docstring of List.map to explain why that turned out to be a bad idea, and to point to List.attach and List.map_congr.

[Ayhon]

Eric Wieser said:

Was having x ∈ ls available as an argument to ls.map ever considered? If so, it might make sense for the docstring of List.map to explain why that turned out to be a bad idea, and to point to List.attach and List.map_congr.

I think that's a good idea. I know I would have appreciated it. Should I open an issue / PR in GitHub?

[Kyle Miller]

That makes map much more dependent, and you can't rewrite ls. The zen of attach is that ls.attach.map is how you get this dependent version — you can opt-in to the additional difficulty.

It would be great if List.map mentioned List.map_congr and List.attach

[Eric Wieser]

You can rewrite ls in the non-dependent case, right?

def List.map' {α β} (l : List α) (f : (a : α) → a ∈ l → β) : List β :=
  match l with
  | [] => []
  | x :: xs => f x (mem_cons_self _ _) :: xs.map' fun a ha => f a <| mem_cons_of_mem _ ha

example (l₁ l₂ : List Nat) (h : l₁ ++ l₂ = l₂ ++ l₁) :
    (l₁ ++ l₂).map' (fun a _ => a*a) = (l₂ ++ l₁).map' (fun a _ => a*a) := by
  rw [h]

[Eric Wieser]

That is, it's not clear that making map dependent incurs any costs for non-dependent uses, besides downstream churn and an extra underscore.

[Eric Wieser]

It's possible that the zen ofl.attach.map fun a => f a.val a.prop instead of l.map' fun a ha => f a ha is a historical artifact caused by the fact that map lived in core and was effectively immutable, while docs3#list.attach lived in mathlib

[Daniel Weber]

Eric Wieser said:

Was having x ∈ ls available as an argument to ls.map ever considered? If so, it might make sense for the docstring of List.map to explain why that turned out to be a bad idea, and to point to List.attach and List.map_congr.

Isn't that docs#List.pmap ?