Prove that inside list.foldl the item is a member of list?

Stream: new members

[aron]

How can I prove that if I am folding over a list, that the 2nd param in the fold must be a member of the list we're folding over?

I'm trying to do something like list.foldl (fun acc item => ...) init -> item ∈ list but I don't know how to write a proposition about a parameter of a function about the data structure the function should be called on

[Ruben Van de Velde]

Maybe something with List.attach

[aron]

Ah nice, yes that's exactly what I needed!

Now is there any way to do the same for a Std.HashMap?

[aron]

hm actually I might have a go at attempting this myself... hopefully it won't be too complicated

[Johannes Tantow]

m.toList.attach.foldl ?

[aron]

that gets me to k ∈ m.toList not to k ∈ m itself

[aron]

I figured it out!

import Std.Data.HashMap
open Std

def HashMap.attach {k v : Type u} [DecidableEq k] [Hashable k] (map : HashMap k v) : List {key : k // key ∈ map} := by
  have l := map.keys.attach
  let l' : List {key : k // key ∈ map} := l.map fun ⟨key, hkey⟩ => ⟨key, HashMap.mem_keys.mp hkey⟩
  exact l'

[Johannes Tantow]

aron schrieb:

that gets me to k ∈ m.toList not to k ∈ m itself

There shoulld be lemmas simplifying this.