working with `filterMap` and `attach`

Stream: lean4

[Logan Murphy]

I have some non-structurally recursive code, and eventually I use a function looking like this:

def myMapFn
  {α β : Type}
  (l : List α)
  (f : {x // x ∈ l} → β)
  (P : β → Bool)  : List β :=
  l.attach |> List.filterMap (fun x ↦ if P (f x) then f x else none)

Now, I feel like I should be able to prove something akin to the following :

theorem aux {α : Type} {h : α} {t : List α} : h ∈ h::t := (List.mem_cons_self h t)
theorem aux' {α : Type} {h : α} {t : List α} (x : { x // x ∈ t }) : ↑x ∈ h :: t :=  by apply List.mem_cons_of_mem ; apply x.property

theorem attach_map_cons_pos
  {α β : Type}
  (h : α)
  (t : List α)
  (f : {x // x ∈ h::t} → β)
  (P : β → Bool)
  (h': P (f ⟨h, aux⟩)) :
  myMapFn (h::t) f P =
  f ⟨h,aux⟩ :: myMapFn t (λ x => f ⟨x, aux' x⟩) P :=

proving this gets a little messy, but I'm able to reduce it to the following goal :

α β : Type
h : α
t : List α
f : { x // x ∈ h :: t } → β
P : β → Bool
h' : P (f ⟨h, aux⟩) = true
x tail : List { x // x ∈ h :: t }
val : α
property : val ∈ h :: t
heq : (h :: t).attach = ⟨val, property⟩ :: tail
x_1 : Option β
left : P (f ⟨val, property⟩) = true
⊢ List.filterMap (fun x ↦ if P (f x) = true then some (f x) else none) tail =
  List.filterMap (fun x ↦ if P (f ⟨↑x, aux' x⟩) = true then some (f ⟨↑x, aux' x⟩) else none) t.attach

but I seem to be stuck here. Am I barking up the wrong tree? Is this even provable?

[Floris van Doorn]

This was definitely more painful than it should be. I was missing lemmas like attach_cons, so I unfolded stuff, but then I was still missing lemmas.

import Mathlib.Data.List.Basic

open List

def myMapFn
    {α β : Type}
    (l : List α)
    (f : {x // x ∈ l} → β)
    (P : β → Bool)  : List β :=
  l.attach |> List.filterMap (fun x ↦ if P (f x) then f x else none)

theorem aux {α : Type} {h : α} {t : List α} : h ∈ h::t := (List.mem_cons_self h t)
theorem aux' {α : Type} {h : α} {t : List α} (x : { x // x ∈ t }) : ↑x ∈ h :: t := by
  apply List.mem_cons_of_mem ; apply x.property

theorem filterMap_id_map {α β} (f : α → Option β) (l : List α) :
    filterMap id (map f l) = filterMap f l :=
  filterMap_map ..

theorem attach_map_cons_pos
    {α β : Type}
    (h : α)
    (t : List α)
    (f : {x // x ∈ h::t} → β)
    (P : β → Bool)
    (h': P (f ⟨h, aux⟩)) :
    myMapFn (h::t) f P =
    f ⟨h,aux⟩ :: myMapFn t (λ x => f ⟨x, aux' x⟩) P := by
  simp_rw [myMapFn, attach, attachWith, pmap, filterMap_cons, h']
  simp (config := {singlePass := true}) only [← filterMap_id_map]
  simp_rw [map_pmap]
  congr 2
  exact pmap_congr t fun a _ h₁ => congrFun rfl

[Logan Murphy]

Brilliant! Thanks a ton Floris