Define an inductive type within a proof?

Stream: lean4

[Heather Macbeth]

Is it possible to define an inductive type on the fly within a def/theorem?

For example, here is a working snippet:

def Foo : Nat → Type
  | 0 => Empty
  | n + 1 => Option (Foo n)

Suppose I wanted to do the same thing but with a custom Option-like type which I define on the fly, like this (which doesn't compile):

def Foo : Nat → Type
  | 0 => Empty
  | n + 1 =>
    | myNone : Foo (n + 1)
    | mySome (i : Foo n) : Foo (n + 1)

Is there a syntax for this?

[Reid Barton]

This seems sort of awkward, e.g., what would the name of the recursor for this new type be (imagine that there are several of these, in different branches)

[Heather Macbeth]

OK, so no :-) Thanks!

[Reid Barton]

In this case you could also use an inductive family, but maybe you have good reasons to prefer a recursive definition.

[Heather Macbeth]

I'm not sure what you mean by an inductive family (here) -- can you explain?

[Reid Barton]

inductive Foo : Nat → Type
| myNone : (n : Nat) → Foo (n + 1)
| mySucc : (n : Nat) → Foo n → Foo (n + 1)

[Heather Macbeth]

Ah! In fact I was asking this question to think about variants on docs4#Fin2, and it seems that you have just explained how one would invent that definition.

[Adam Topaz]

Another natural variant is the inductive def of docs#vector which is very similar to this version of fin, as follows:

inductive Vector (α : Type u) : Nat → Type u
  | nil : Vector _ 0
  | cons : α → Vector α n → Vector α (n+1)

[Adam Topaz]

If I understand correctly, we avoid such defs because they're not as (computationally) efficient as the def in terms of subtypes? Is that right?

[Reid Barton]

Well to be fair, Peano numerals and (to a lesser extent) linked lists are not that computationally efficient in the first place.

[Reid Barton]

Another downside of these inductive families is that the representation of the "data" (like a natural number) is so tightly coupled to the "property" (like being less than n). For example if you want to do fin.cast_succ on Foo, you need to do recursion (and it takes $O(m)$ time, where $m$ is the number).

[Reid Barton]

In some contexts that tight coupling could be a good thing, but mostly it seems like a bad thing.