Inverse direction of `List.ofFn`

Stream: Is there code for X?

[Xavier Roblot]

We have docs#List.ofFn that can turn Fin n → α into List α, but is there an easy way to go in the other direction that is, from a List α to construct a Fin n → α either by truncating the list if it is too long or by appending, say, copies of a fixed element of α, if it's too short.

For my application , α would be ℕ, all the lists I consider are of length ≤ n and I'd like to
append some 0's to turn them into Fin n → ℕ. To #xy, I need to do computations with digits of some natural numbers in base b. We have for that the very nice docs#Nat.digits but my life would be a lot easier if the list of digits where all of the same (fixed) length.

[Bhavik Mehta]

This isn't quite what you're looking for, but docs#List.get is worth knowing about. It requires you have the right length (ie not too short or too long), but still might be helpful.

[Kenny Lau]

It would be easier for everyone if you could include #mwe, so that someone who knows the solution can fill in the blank very easily without having to write the whole thing from scratch:

import Mathlib

example {α : Type*} (x : List α) : Fin x.length → α :=
  x.get

[Bhavik Mehta]

In combination with docs#Fin.take, actually this covers the "too long" case, see eg docs#Fin.ofFn_take_get and docs#Fin.get_take_ofFn_eq_take_comp_cast

[Kenny Lau]

In other words, if you had included the following in your question:

import Mathlib

example {α : Type*} (x : List α) : Fin x.length → α :=
  sorry

then I would have been able to answer your question in 10 seconds.

[Kenny Lau]

or rather,

import Mathlib

example (x : List ℕ) (n : ℕ) (h : x.length ≤ n) : Fin n → ℕ :=
  fun i ↦ x[i]?.getD 0

(again, importance of including code so I don't have to guess)

[Bhavik Mehta]

Xavier Roblot said:

To #xy, I need to do computations with digits of some natural numbers in base b. We have for that the very nice docs#Nat.digits but my life would be a lot easier if the list of digits where all of the same (fixed) length.

It may be useful to look at https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Additive/AP/Three/Behrend.html#Behrend.map_apply, which is also about computations with digits of natural numbers in an arbitrary base. But perhaps your application is different enough that this isn't useful

[Xavier Roblot]

Bhavik et Kenny, thanks for the answers. I'll have a look at Mathlib.Combinatorics.Additive.AP.Three.Behrend which may provide an easy solution for my problem, otherwise I'll try Kenny's solution.

[Bhavik Mehta]

I don't think my example will completely solve your problem, to be clear! It was designed to be for this specific proof (where the idea is specifically to think about the digits of a natural), rather than be a general API for digits.

[Xavier Roblot]

Well, in the end, I used Kenny's suggestion to create a Fin version of Nat.digits and use that to prove the result I need: #31468