Mutual inductive families

Stream: new members

[Eric Wieser]

mk : ∀ d, list (reactor d) → network d.succ
is probably what you want there

[Eric Wieser]

Your problem is that you're using list inside your definition which is itself inductive, and this isn't well-supported

[Eric Wieser]

This works:

mutual inductive network, reactor
with network : ℕ → Type u
| empty : network 0
-- copy the list constructors here
| nil : ∀ d : ℕ, network d.succ
| cons : ∀ {d}, reactor d → network d.succ → network d.succ
with reactor : ℕ → Type u
| mk : ∀ d, network d → reactor d

-- shorthand to build up the list constructors
def network.mk {d : ℕ} : list (reactor d) → network d.succ
| [] := network.nil d
| (x :: xs) := network.cons x (network.mk xs)

-- or: @list.rec _ (λ _, network d.succ) (network.nil d) (λ x _, network.cons x)

[Marcus Rossel]

Hm, that's too bad.

Also, how do I solve this universe issue?

universe u

mutual inductive network, reactor (d : ℕ) (α : Type*)
with network : ℕ → Type* → Type u
| empty : network 0 α
| mk (r : reactor d α) : network (d + 1) α
with reactor : ℕ → Type* → Type u
| mk (n : network d α) (o : option α) : reactor d α

It's telling me:

mutually inductive types compiled to invalid basic inductive type
nested exception message:
universe level of type_of(arg #4) of 'network._mut_.mk_1' is too big for the corresponding inductive datatype

But I don't know what network._mut_.mk_1 or arg #4 actually refer to.

[Kevin Buzzard]

In general it might be unwise to mix Type* and Type u. The latter says "I know what I'm doing and will name universes myself", the former says "I will let Lean figure universes out for me". Which one are you?

[Reid Barton]

There are a lot of problems with this definition

[Reid Barton]

universe u

mutual inductive network, reactor (α : Type u)
with network : ℕ → Type u
| empty : network 0
| mk (d : ℕ) (r : reactor d) : network (d + 1)
with reactor : ℕ → Type u
| mk (d : ℕ) (n : network d) (o : option α) : reactor d

[Reid Barton]

Parameters (stuff before with) shouldn't be repeated later. And d is not a parameter of the inductive families, it varies.

[Reid Barton]

Also, I don't know whether these examples are minimized from your real application, and inductive families are nice, but you might consider whether you can use a recursively-defined family of types instead. That works better than you might think.

[Marcus Rossel]

Kevin Buzzard said:

In general it might be unwise to mix Type* and Type u. The latter says "I know what I'm doing and will name universes myself", the former says "I will let Lean figure universes out for me". Which one are you?

I belong to the "I will let Lean figure universes out for me" group. But Lean complained that mutually inductive types must live in the same universe, so declaring them Type* didn't work.

[Kevin Buzzard]

I see! I know nothing about mutual inductives, I have always gone by the maxim that they are to be avoided in Lean 3.

[Marcus Rossel]

Kevin Buzzard said:

I see! I know nothing about mutual inductives, I have always gone by the maxim that they are to be avoided in Lean 3.

How do you avoid them?
My problem is that a reactor is supposed to contain a graph of reactors (called network here). I felt like the only way to achieve this was to define reactor and network at the same time. But it sounds like this isn't actually the case.

[Kevin Buzzard]

My understanding is that Lean internally unravels the mutual inductives into one big inductive, and that in practice it's best that the human does the unravelling themselves. You could define both functions at once by defining a term of the product of the function spaces, for example, but there could well be slicker ways. I am certainly not an expert.

[Marcus Rossel]

@Reid Barton Is there some sort of document that explains the syntax for inductive definitions? I find myself winging it most of the time, because TPIL Chapter 7 doesn't explain it clearly enough for me.

[Mario Carneiro]

You usually can't omit the universes in inductive types, unless the inductive is not universe polymorphic and everything is in Type

[Mario Carneiro]

@Marcus Rossel I don't have any document to point to, but the syntax of an inductive definition looks like this:

DOC? ATTR* (private|protected)? noncomputable? meta?
class? inductive {UNIV*}? NAME BINDER* (: TYPE)?
LOCAL_NOTATION?
(| CONSTR INFER_KIND? BINDER* : TYPE)*

and a mutual inductive looks like this

DOC? ATTR* (private|protected)? noncomputable? meta?
mutual class? inductive {UNIV*}? NAME,* BINDER*
LOCAL_NOTATION?
(
  with ATTR* NAME : TYPE
  (| CONSTR INFER_KIND? BINDER* : TYPE)*
)*

[Mario Carneiro]

Here's an example using a gratuitous number of those slots:

/-- Foo and bar -/
@[interesting] protected noncomputable meta
class inductive {u v} foo, bar (α : Type u) (β : Type v)
notation `X` := nat
with foo : X → Type
| a : foo 0
| b {} (n : X) : n < 3 → foo 1

with bar : nat → Type
| c (n) : foo n → bar n

[Reid Barton]

Did you forget mutual?

[Mario Carneiro]

fixed

[Bolton Bailey]

I was trying to define mu-recursive functions and ran into the same error as Marcus.

import data.vector.basic

/-- μ-recursive algorithms for functions from ℕ^k to ℕ -/
inductive μ_recursive : ℕ -> Type -- nested occurrence 'list.{0} (μ_recursive k)' contains variables that are not parameters
| const {k : ℕ} {n : ℕ} : μ_recursive k
| succ : μ_recursive 1
| proj {i k : ℕ} (h : i < k) : μ_recursive k
| comp {m k : ℕ} (h : μ_recursive m) (g : vector (μ_recursive k) m) : μ_recursive k
| ρ {k : ℕ} (g : μ_recursive k) (h : μ_recursive (k + 2)) : μ_recursive (k + 1)
| μ {k : ℕ} (f : μ_recursive (k + 1)) : μ_recursive k

Just to clarify @Eric Wieser 's comment about using inductive types inside definitions of other inductive types: Is there just no way to use vector here and I should just define a mutually-inductive μ_rec, μ_rec_vec, or is there a workaround that will let me use vector in the definition?

[Reid Barton]

Are you particularly attached to vector? How about fin m -> μ_recursive k?

[Bolton Bailey]

fin m -> μ_recursive k works fine, thanks. I guess I didn't expect that to work any better than what I had. Is it that nat is fine and all other inductive types choke? What's so special about nat?

[Bolton Bailey]

I guess it's a universe issue, as Marcus said above. I just wasn't getting that from the error message, sorry.

[Reid Barton]

With fin m -> it becomes a regular inductive type rather than one which is recursive through vector

[Marcus Rossel]

@Bolton Bailey
Side Note: This thread on (painful) inductives (in Lean 4) might be interesting for you, too.

And to elaborate on what Reid wrote:
In Lean's underlying theory (#leantt) we can only have constructors for inductive types which are "positive" - that is, if a constructor of an inductive type I takes a parameter p whose type also refers to I (thereby making I recursive), then the type of p has to have the form α₁ → α₂ → ... → I. That is, recursive appearances of I are only allowed in the form that I is the final output of some function (if that function has zero input parameters, then p simply has type I).

So it's not nat being magical that makes the reformulation work, but rather the restructuring of type of your parameter such that mu_recursive appears on the very right.