Prove element of list is in list

Stream: new members

[Curious Joe]

Hi everyone

I want to construct a list from n : Nat using List.range n and return
a List of type List (Fin n).
I am getting stuck on proving that a given i of the list is in the range.
In particular, how to prove that i ∈ List.range n when using map on the range?

I have the theorem:

theorem mem_range_right {m n : Nat} : m ∈ List.range n → m < n := by
  simp[*]

and thus the structure:

def range_fin' (n : Nat) : List (Fin n) :=
  let range := List.range n
  range.map (
    λ i =>
      have h : i ∈ range := sorry
      ⟨i, mem_range_right h⟩
  )

Does anyone know how to prove that i ∈ range in the above code?
It should be trivial ;D

[Edward van de Meent]

do you know about List.finRange?

[Edward van de Meent]

(since that seems to be your end goal)

[Curious Joe]

oh wow; no I didn't; can't believe neither moogle.ai nor ChatGPT told me about that one!! :D

but thanks a lot, that is literally the end goal I wanted :)

[Edward van de Meent]

if you're doing this as an exercise, you might be interested in List.attach

[Curious Joe]

thanks a lot! I did indeed not want to use mathlib; this worked for me:

def range_fin (n : Nat) : List (Fin n) :=
  let range := List.range n
  let out := range.attach.map (
    λi => ⟨i, mem_range_right i.property⟩
  )
  out

[Edward van de Meent]

(neither of those are defined in mathlib)

[Curious Joe]

okay sorry; my LSP showed me when searching for List.finRange and I don't have mathlib so I thought it was there.
It is in the docs, though?

[Edward van de Meent]

it is, but the docgen also docs all things used by mathlib, so upstream things. at the top of the page, you can see that it is defined in Init.Data.List.FinRange, however, which is not Mathlib.Foo

[Curious Joe]

Ah yes, thanks for teaching me, it pays well to be part of the community here at Zulip :=)