Constructing a function on Lists in terms of length

Stream: mathlib4

[Connor Gordon]

For a type α (that is a metric space), I am currently trying to construct a function g : List Bool → Set α such that for any two lists l1 and l2, if l1 is a prefix of l2, then g l2 ⊆ g l1 (the outputs should all be nonempty and two distinct lists of the same length should map to disjoint sets, among a couple other conditions).

I currently have the machinery to, given a Finset (Set α) meeting the conditions above, I can split it into another Finset (Set α) with twice as many elements, also meeting the conditions and having two subsets of each of the elements in the original Finset (or well, I have the preliminary results to prove that splitting lemma once I know exactly how to formulate it to solve this problem.

Does anyone have any ideas how I should formulate the splitting lemma and/or go about the construction once I have it? I'd imagine I'd have to do it by induction/recursion but I don't know how.

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

What's your maths proof that such a function exists? In fact, in this generality such a function doesn't always exist (for example if alpha is finite).

[Kevin Buzzard]

If alpha is infinite, then choose an injection from the naturals into alpha and then define $g$ by sending $[a_0,a_1,\ldots,a_{n-1}]$ to the image under the injection of all the naturals congruent to $\sum_i a_i2^i$ mod $2^n$, where you identify Bool with $\{0,1\}$.

[Felix Weilacher]

I think what Connor is asking is how to define a function f : List Bool \to X inductively where f of a list a :: s of length n+1 does not just depend on f s (as in the default List.rec), but on f t for all lists t of length n.

[Felix Weilacher]

(I also would like to know how to do this)

[Felix Weilacher]

One option is to define functions (f n) : {s : List Bool | s.length = n} \to X by induction on n. I am not sure if this is the cleanest way to do it though.

[Connor Gordon]

Felix is correct, this is what I am looking for. The full context can be found in this conversation, but right now I'm trying to compartmentalize the remainder of the proof into pieces that I could feasibly work on, and figuring out how to get this definition right is an important one.

[Kevin Buzzard]

You can make your own recursors, like this:

def List.rec_on_length (α β : Type _)
    (IH : ∀ L : List α, (∀ M : List α, M.length < L.length → β) → β) : List α → β :=
  fun L ↦ IH L (fun M _ ↦ M.rec_on_length α β IH)
  termination_by L => List.length L

I'm no expert in this though. That should be something which, given a "recipe" IH which takes as input a list L, and an element of beta attached to every list of length less than L's length, returns an element of beta, will give you the recursively-defined function to beta defined by the recipe.

[Adam Topaz]

you can just define your function recursively and prove termination as needed.