feat: enable recursive structure command

[kmill]

Now that the elaborator supports primitive projections for recursive inductive types (#5822), enable defining recursive inductive types with the structure command, which was set up in #5842.

Example:

structure Tree where
  n : Nat
  children : Fin n → Tree

def Tree.size : Tree → Nat
  | {n, children} => Id.run do
    let mut s := 0
    for h : i in [0 : n] do
      s := s + (children ⟨i, h.2⟩).size
    pure s

Note for kernel re-implementors: recursive structures are exercising the kernel feature where primitive projections are valid for one-constructor inductive types in general, so long as the structure isn't a Prop and doesn't have any non-Prop fields, not just ones that are non-indexed and non-recursive.

Closes #2512

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5783 build failed against this PR. (2024-10-21 03:45:58) View Log
• 💥 Mathlib branch lean-pr-testing-5783 build failed against this PR. (2024-10-22 03:22:39) View Log
• 💥 Mathlib branch lean-pr-testing-5783 build failed against this PR. (2024-10-22 03:42:47) View Log
• 💥 Mathlib branch lean-pr-testing-5783 build failed against this PR. (2024-10-25 18:26:46) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 03c6e99ef7fcde86aa1843ff4dac7d581cb4e830 --onto 38c39482f40536b864a9b43c718e10e8413b26e5. (2024-10-31 05:27:23)

[digama0]

I want to try putting the breaks on this, at least as far as the kernel is concerned. The kernel notion of isStructureLike really needs to imply non-recursive, although it's fine if this is just an elaborator thing. Primitive projections are fine-ish (they are already allowed on some non-structures, although this was the source of a soundness bug in the past), but structure eta is not feasible.

[kmill]

@digama0 This is not touching the kernel. This is just making it possible to use the structure elaborator to define one-constructor inductive types, since it gives convenient notations. Do you still have any objections?

Edit: This is certainly stress-testing mkProjections though. Something I'm considering is also having inductive register types as being structures in the elaborator when it makes sense to do so, and use mkProjections.

[nomeata]

So maybe the title could be “feat: structure syntax in mutual datatype definitions”

[tydeu]

@kmill

Something I'm considering is also having inductive register types as being structures in the elaborator when it makes sense to do so, and use mkProjections.

If this feature is added, I would hope it can be toggled. I sometimes use inductive rather than structure for structure-like types specifically when I don't want the auto-generated projections.

[digama0]

@digama0 This is not touching the kernel. This is just making it possible to use the structure elaborator to define one-constructor inductive types, since it gives convenient notations. Do you still have any objections?

No objections.

Edit: This is certainly stress-testing mkProjections though. Something I'm considering is also having inductive register types as being structures in the elaborator when it makes sense to do so, and use mkProjections.

By the way, the thing I'm most specifically worried about is the overloaded meaning of isStructureLike, which is currently being used in a bunch of ways: by both the kernel and the elaborator, for structure, projections (both projection functions and primitive projections), structure instance syntax, and structure eta. I suggest making these into clearly separate functions so that there will not be unintended fallout where changes to one of these use cases impacts another one.

[kmill]

@digama0 Isn't the kernel only using is_structure_like for a couple applications of eta? I see just try_eta_struct (used by is_def_eq_core), is_def_eq_unit_like, and to_cnstr_when_structure (used by inductive_reduce_rec). Primitive projections don't use it, and this is why this PR works without making any changes to is_structure_like/isStructureLike (notably mk_projections just checks for an non-indexed one-constructor inductive type). There are still some places that break in the elaborator though because of misuse of isStructureLike.

Notice that I did not change isStructureLike in this PR. It is important for it to reflect the kernel implementation, and you can rest assured that it it will remain that way. (It would be nice to figure out some better naming so that people don't get confused about isStructureLike vs inductive types created by the structure command.)