definining lists in Lean 4

Stream: new members

[Ben Nale]

Hi
How do I define a list of length n in Lean 4 if I know each element in terms of its index? I asked chatGPT and I got something that doesn't quite work :|. It said def list_of_length_n (x : nat) (n : nat) : list nat := [x | _ in 1..n].
I can do it inductively but I believe there's a better way. Also, for questions like this what reference can I look at in the future so that I don't have to bug y'all?

[Ben Nale]

this can't be that hard :eyes:

[Johan Commelin]

Do you mean that you want to turn a function Fin n -> X into a List X?

[Ben Nale]

I want to do something like def list_foo (n : nat) : list nat := [2^i | i in 1..n]

[Ben Nale]

oh yes , I get you! that is what i want

[Johan Commelin]

docs4#List.ofFn

[Ben Nale]

cheers!

[Arthur Paulino]

Another option:

@[specialize] def mkListWith (n : Nat) (f : Nat → α) : List α :=
  List.range n |>.map f

[Ben Nale]

nice. Since I'm not using mathlib I'll go with this option :)

[Ben Nale]

what's a good resource for learning things like this btw?

[Johan Commelin]

Probably this stream on Zulip (-;

[Arthur Paulino]

The version Johan linked is from std4, so if you're already able to import Std... that will be in import Std.Data.List.Basic

[Ben Nale]

thanks so much

[Chris Miller]

Like in the example above I tried to define a list, but the problem I get that it doesn't seem to accept the function I would like to use.

ConFracDenom ξ definitely returns an element of ℤ.

It underlines "expansion" and says IR check failed at 'expansion', error: unknown declaration 'aux'

What am I doing wrong?

noncomputable def aux (ξ : ℝ) : ℕ → ℤ := ConFracDenom ξ

variable (r : ℝ)
#check aux r -- ℕ → ℤ

def expansion' (n : ℕ) (f : ℕ → ℤ) : List ℤ :=
  List.range n |>.map f

def expansion (ξ : ℝ) (n : ℕ) : List ℤ :=
  expansion' n (aux ξ)

[Ruben Van de Velde]

Sounds like you need to add more noncomputable keywords

[Ruben Van de Velde]

It is known that this error is bad

[Chris Miller]

Thank you, that worked.
I thought it had a problem with aux itself...
What does IR check mean?

[Ruben Van de Velde]

IR is "intermediate representation", which is a step in compiling the definition to machine code. But because aux is not compiled, it can't be used from compiled code

[Kevin Buzzard]

lean4#1785 tracks this issue.

[Kevin Buzzard]

@Alex J. Best should you change the title of the issue so that it doesn't mention find any more? This threw me off the scent when I was searching for the issue.

[Alex J. Best]

Done. I'm not sure I have a better name for it though