Refactor to use `list_blank`

Stream: general

[Praneeth Kolichala]

We have an important data structure in mathlib hiding here called list_blank, which is essentially a list with an infinite tail of default's at the end.

We know that list_blank α is equivalent to ℕ →₀ α. Moreover, list_blank is the natural list-like structure to return for many functions which need to return what is essentially a finitely supported function on ℕ, but also want computability and nice definitions for operations like cons, head, and tail. Examples include:

- digits: https://github.com/leanprover-community/mathlib/blob/e3d2f74c0a460f65bf3529632dc142ce0854615c/src/data/nat/digits.lean
Any number can be thought of as having an infinite list of trailing 0's at the end. Maybe we should refactor digits/prove that digits factors through list_blank. Presumably this would give many lemmas (like last_digit is nonzero) for free.

- nat.bits: Same as above, but we can imagine an infinite trail of ff's.
- polynomial: This captures the general case; a polynomial has an infinite trailing list of 0 coefficients. Indeed, this topic came up in the PR to make a computable implementation of polynomials.

One stumbling block is that the current list_blank implementation fills the blanks with default, whereas some of these require 0 from has_zero. Should we refactor list_blank to take an explicit default value, so that we can use list_blank in these places?

[Bolton Bailey]

I don't think it would be good to use 0 as the default value, since I think it's probably mostly used for Turing machine tapes, which might want to use zero as something distinct from blank.

[Bolton Bailey]

I would be fine with a refactor, but then I have never used this def, and I don't know how much additional effort it would impose on people trying to use the code. Perhaps what would be best would be to define a new data structure that specifies an element, and then redefine list_blank in terms of that with an inhabited argument.

[Bolton Bailey]

Regardless of how we decide to refactor, I think it probably makes sense to split this initial segment of the file off of turing_machine.lean, since it seems like there are other use cases

[Bolton Bailey]

I’ll write a PR for this if you haven’t, will report back

[Bolton Bailey]

#16160 I made the mistake of touching a low file, so I'm going to wait for CI to compile this before trying to work more on it.

[Praneeth Kolichala]

This looks great. Possibly headd could be written as nthd 0 or head'.get_or_else if you want to avoid touching low level files.

I’ll eventually try havé digits have a lemma showing that it factors through list_blank.