Define type of trees of fixed depth

Stream: lean4

[Vasilii Nesterov]

Hi there! I'm trying to define an inductive type of trees with fixed depth like this:

inductive MyTree : ℕ → Type where
| leaf : MyTree 0
| node {n : ℕ} : List (MyTree n) → MyTree (n + 1)

Lean complains about:

(kernel) invalid nested inductive datatype 'List', nested inductive datatypes parameters cannot contain local variables.

I also feel that there's something wrong because I want to use the inductive structure of ℕ while defining MyTree, and I don't know how to acheive this. Are there good ways to overcome this problem?

[Daniel Weber]

You could define general trees then take a subtype

[Daniel Weber]

inductive MyTree : ℕ → Type where
| leaf : MyTree 0
| node {n c : ℕ} : (Fin c → MyTree n) → MyTree (n + 1)

this also works

[Thomas Murrills]

You could also define your own List specialized to MyTree:

mutual

  inductive MyTree : ℕ → Type where
  | leaf : MyTree 0
  | node {n : ℕ} : MyForest n → MyTree (n + 1)

  inductive MyForest : ℕ → Type where
  | nil {n : ℕ} : MyForest n
  | cons {n : ℕ} : MyTree n → MyForest n → MyForest n

end

Though I suspect that if you want them to actually have depth n in a nontrivial sense, you might want a "list that always has at least one element", i.e.

  inductive MyForest : ℕ → Type where
  | single {n : ℕ} : MyTree n → MyForest n
  | cons {n : ℕ} : MyTree n → MyForest n → MyForest n

instead? (Alternatively, that requirement could be bundled into the .node constructor for MyTree by giving it a MyTree n argument in addition to the MyForest n argument)

[Joachim Breitner]

Your first attempt fails due to https://github.com/leanprover/lean4/issues/1964. @Arthur Adjedj has a solution on a branch, but it's not clear when and if that will make it into lean. If this is blocking you, feel free to describe your use case on the issue.