Defining an dependently-typed recursive inductive data type

Stream: lean4

[Andrew]

Hi everyone! I am trying to define an inductive datatype that represents natural-number literals an n-ary operators on them. However, Lean is rejecting my datatype with the error message (kernel) invalid nested inductive datatype 'Vector', nested inductive datatypes parameters cannot contain local variables.. I've attached an #mwe here. Could anyone give a suggestion on how to make this type work?

[Kenny Lau]

@Andrew you can include the code using #backticks, which already generates a link to the website (on the top right hand corner of the code block)

[Andrew]

import Mathlib.Data.Vector.Basic

inductive NumericExpression where
  | numericLiteral : Nat -> NumericExpression
  | operation : (n : Nat) -> (Vector Nat n -> Nat) -> (Vector NumericExpression n) -> NumericExpression

[Andrew]

Even more minimal #mwe here:

import Mathlib.Data.Vector.Basic

inductive NumericExpression where
  | operation : (Vector NumericExpression 3) -> NumericExpression

[Kenny Lau]

you forgot to include the definition of MyVector

[Andrew]

Just changed it, I'm using the standard library vector, MyVector was just for debugging

[Jovan Gerbscheid]

It works with List, and I think also with Array, but Vector is not supported yet for constructing inductive types through it. This is a limitation in the current implementation of inductive types. In the new year 3 roadmap it says that inductive will be fixed so that HashMap and TreeMap are supported here. I assume that this will also fix it for Vector.

[Andrew]

Thanks!

[Phil Nguyen]

I ran into a similar problem a while ago. It turns out Vector or refined types aren't supported yet. A current suggested solution would be something like Fin n -> NumericExpression:

inductive NumericExpression where
| numericLiteral : Nat -> NumericExpression
| operation : (n : Nat) -> (Vector Nat n -> Nat) -> (Fin n → NumericExpression) -> NumericExpression

But if you'd prefer a first-order, more readily inspectable representation, you could also try mutually defining NumericExpressionList : Nat -> Type:

mutual
inductive NumericExpression : Type u where
| numericLiteral : Nat -> NumericExpression
| operation : (n : Nat) -> (Vector Nat n -> Nat) -> NumericExpressionList n -> NumericExpression
inductive NumericExpressionList : Nat → Type u where
| nil : NumericExpressionList 0
| cons : NumericExpression → NumericExpressionList n → NumericExpressionList (n + 1)
end

These solutions are sub-optimal (e.g. boilerplate, poor locality, etc.). But I think they'll improve this coming year.

[Jovan Gerbscheid]

(Note also that you don't need to import Mathlib.Data.Vector.Basic, as Vector is defined in Std)