Inductive type nesting

Stream: new members

[Marcus Rossel]

The following inductive type definition works just fine:

inductive lthing
  | mk (l : list lthing) : lthing

This one on the other hand ...

import data.finmap

inductive fthing
  | mk (f : finmap (λ _ : ℕ, fthing)) : fthing

... produces an error:

inductive type being declared can only be nested inside the parameters of other inductive types

How are these two definitions different, and what does the error mean?

[Mario Carneiro]

An open secret about lean 3 is that it doesn't actually support nested inductives. It has a mechanism for simulating some nested inductives but there are lots of limitations and you are best off avoiding them entirely. (The situation is quite different in lean 4, which has kernel support for nested inductives. However, I think this example would still not work, because finmap is not an inductive type, it is a quotient of an inductive type.)

[Marcus Rossel]

What exactly is a nested inductive?

[Mario Carneiro]

Inductive types have some pretty restrictive conditions about the shape of the constructors. The rule for regular inductives, the only kind that lean supports natively, is that every constructor must have the type arg1 -> arg2 -> .. -> T where T is the type being defined, and each argi either doesn't mention T at all, or has the form arg1 := arg1_1 -> arg1_2 -> .. -> T where each arg_i_j does not mention T. In other words, T can't appear on the left of the left of an arrow, and it can't appear nested in any way with other type constructors

[Mario Carneiro]

Types like fthing involve a mutual combination of an inductive type and a quotient type, and these are very difficult to specify in general. It is possible to simulate them in many cases by lifting the quotient operation to the top level

[Mario Carneiro]

So in this case, we have a tree, where at each level the children can be permuted. So we would define what it means for two trees to be related by a permutation at all levels, and then quotient the type of trees (a pure inductive type) with the permutation relation (the quotient) to make a quotient of an inductive, as opposed to a quotient/inductive combined thing

[Mario Carneiro]

In most cases I would just skip the quotient part unless I really need it though

[Mario Carneiro]

here's a simple inductive type that is equivalent to fthing without the quotient:

inductive fthing
| nil : fthing
| cons : ℕ → fthing → fthing → fthing

[Marcus Rossel]

So if the constructor for fthing was actually supposed to take many more parameters, this approach becomes really infeasible right?

[Mario Carneiro]

Parameters usually aren't a problem, although you might be using that word in a different way than me

[Mario Carneiro]

it might help to more concretely explain what you are trying to do

[Marcus Rossel]

Ah yes, I mean it in a "regular" programming language kind of way. So e.g. if fthing was actually ...

inductive fthing
  | mk (f : finmap (λ _ : ℕ, fthing)) (g : finmap (λ _ : int, fthing)) (h : fthing) (i : nat) (j : nat) (k : nat) (l : nat) : fthing

... then I'm guessing that the "unrolling" of nested inductives becomes a real pain, right?

[Mario Carneiro]

The idea is that you think of fthing here as being either a thing or a list of things, and then you would write that as

inductive fthing
  | mk (f g h : fthing) (i j k l : nat) : fthing

with an extra two constructors at the end for nil and cons

[Mario Carneiro]

If necessary you can even make the types of "thing" and "list of thing" different, using an indexed inductive:

inductive fthing : bool → Type
| nil : fthing ff
| cons : ℕ → fthing tt → fthing ff → fthing ff
| mk (f g : fthing ff) (h : fthing tt) (i j k l : nat) : fthing tt

Here fthing ff means "list of thing" and fthing tt means "thing"

[Mario Carneiro]

the complexity of this approach scales with how many "syntactic classes" are needed for your description. In this case there are two: one for things and one for lists of things. If there are more constructors like mk that isn't too much of a problem as long as they only need to talk about things and lists of things; if you need more things (for example json needs "json value", "json array" and "json object" as syntactic classes in this description) then you add all of the constructors for all of those into a single inductive family

[Marcus Rossel]

Mario Carneiro said:

it might help to more concretely explain what you are trying to do

In my real project I have five types which are in a big dependency cycle:
deps.png

That is, each of those types' constructors has some argument that refers to the type it points to in the graph:
I tried to define them as mutual inductives first, but now opted for the manual approach:

inductive label
  | mut_out | mut | rcn | rtr | network : label

inductive {u v} component (ι : Type u) (υ : Type v) : label → Type (max u v)
  | empty_mutation_output :component label.mut_out
  | mutation_output (r: component label.rtr) (...) (...) (...) : component label.mut_out
  | mutation (f : ι → component label.mut_out) (...) (...) (...) : component label.mut
  | reaction (m : component label.mut) (...) (...) (...) : component label.rcn
  | reactor (r : ι → component label.rcn) (m : ι → component label.mut) (n : component label.network d) : component label.rcn
  | empty_network : component label.network
  | network (g : finmap (λ _ : ι, component label.rtr)) : component label.network

[Mario Carneiro]

In this thread I'm talking about performance problems with this approach performed at a much larger scale, to describe the entire syntax of lean 3 as a nested mutual inductive type. There are about 60-70 syntactic classes involved there

[Mario Carneiro]

I wouldn't even attempt that in lean 3, but I have done similar things at a smaller scale in lean 3. 5 types should be doable

[Mario Carneiro]

Your example encoding is just what I would recommend in this setting

[Marcus Rossel]

I'll have to read that thread to see how you unfold all the nested inductives.

[Mario Carneiro]

In Lean 4 I don't have to for the most part, I can just write nested inductives and it just works

[Mario Carneiro]

Oh, I would modify your example in order to eliminate the finmap in the network constructor, by adding a 6th type "rtr_map"

[Marcus Rossel]

Hmmm, so could it possibly be a better option to just formalize this in Lean 4, than going through the pain of doing this manually? (The project for which I need this doesn't rely much on Mathlib)

[Mario Carneiro]

you could try, it does seem to handle these kinds of projects rather better than lean 3, although I think the proof side isn't yet up to scratch

[Marcus Rossel]

"the proof side isn't yet up to scratch"
... could you elaborate (if there's anything concrete)?

[Mario Carneiro]

most tactics are still missing. There is cases and induction which is like 90% of CS formalizations though

[Marcus Rossel]

Perfect, the proofs I'm doing are very CS-y :D