Zulip Chat Archive

Stream: new members

Topic: Mutual inductive families


Eric Wieser (Jul 19 2021 at 13:23):

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

Eric Wieser (Jul 19 2021 at 13:24):

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

Eric Wieser (Jul 19 2021 at 13:26):

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 (Jul 19 2021 at 17:39):

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 (Jul 19 2021 at 17:45):

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 (Jul 19 2021 at 17:46):

There are a lot of problems with this definition

Reid Barton (Jul 19 2021 at 17:47):

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 (Jul 19 2021 at 17:49):

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

Reid Barton (Jul 19 2021 at 18:10):

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 (Jul 19 2021 at 20:27):

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 (Jul 19 2021 at 20:29):

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 (Jul 19 2021 at 20:32):

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 (Jul 19 2021 at 20:34):

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 (Jul 19 2021 at 20:43):

@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 (Jul 19 2021 at 21:16):

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

Mario Carneiro (Jul 19 2021 at 21:26):

@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 (Jul 19 2021 at 21:31):

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 (Jul 19 2021 at 21:48):

Did you forget mutual?

Mario Carneiro (Jul 19 2021 at 22:31):

fixed

Bolton Bailey (Dec 24 2021 at 05:52):

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 (Dec 24 2021 at 06:17):

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

Bolton Bailey (Dec 24 2021 at 06:23):

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 (Dec 24 2021 at 06:26):

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

Reid Barton (Dec 24 2021 at 06:33):

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

Marcus Rossel (Dec 24 2021 at 08:42):

@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.


Last updated: Dec 20 2023 at 11:08 UTC