Zulip Chat Archive

Stream: general

Topic: Mutual induction problem


view this post on Zulip Neil Strickland (Nov 02 2018 at 17:08):

Here is an attempt at a mutually inductive definition, which is a bit more intricate than the ones in the book.

open nat

mutual inductive partition,blocks
with partition :  (n : ), Type
| null : partition 0
| add (n : ) (p : partition n) : partition (succ n)
| join (n : ) (p : partition n) (b : blocks n p) : partition (succ n)
with blocks :  (n : ),  (p : partition n),Type
| old_block (n : ) (p : partition n) (b : blocks n p): blocks (succ n) (add n p)
| new_block (n : ) (p : partition n) : blocks (succ n) (add n p)
| join_block (n : ) (p : partition n) (b : blocks n p) (c : blocks n p) :
                blocks (succ n) (join n p b)

Lean rejects it with the following message:

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

Is there a way to fix this? I have not really absorbed much of the story about universe levels so I do not know whether this is hard or not.

(The intended interpretation is as follows. partitions n is supposed to represent the set of partitions of the set {0,,n1}\{0,\ldots,n-1\}, and blocks n p is supposed to represent the set of blocks of the partition p. Obviously n should be implicit here but I am leaving it explicit until I have fixed the other issues. In the case n=0n=0 there is a unique partition which we call null. One way to partition {0,,n}\{0,\ldots,n\} is to take a partition p of {0,,n1}\{0,\ldots,n-1\} and add {n}\{n\} as an extra block; we call this add n p. Another way is to take p and a block b of p and use b{n}b \cup \{n\} as one block of a new partition which we call join n p b. )

view this post on Zulip Reid Barton (Nov 02 2018 at 17:18):

I think this is an inductive-inductive type, which I think Lean doesn't support.
Sometimes you get that error about universe levels when the real issue is that Lean got confused for another reason--here there's also an error on the use of partition in the declaration of blocks; it looks like Lean doesn't know what partition is yet.

view this post on Zulip Reid Barton (Nov 02 2018 at 17:23):

A less innocuous-looking example of an inductive-inductive type:

mutual inductive code,el
with code : Type
| cempty : code
| cnat : code
| csigma (a : code) (b : el a  code) : code
| cpi (a : code) (b : el a  code) : code
with el : Π (c : code), Type
| enat (n : ) : el cnat
| esigma (a : code) (b : el a  code) (x : el a) (y : el (b x)) : el (csigma a b)
| epi (a : code) (b : el a  code) (x : Π (i : el a), el (b i)) : el (cpi a b)

view this post on Zulip Reid Barton (Nov 02 2018 at 17:31):

Though my example involves recursion in negative positions in a few places, so maybe I've got the example wrong

view this post on Zulip Reid Barton (Nov 02 2018 at 18:03):

I tried defining partition and blocks by mutual recursion, rather than making them inductive types, but Lean wasn't happy with my attempt either.

view this post on Zulip Reid Barton (Nov 02 2018 at 18:04):

I think the best you can do is define the types by some other means and then try to approximate the interface you would get from an inductive definition, for example by defining your own "induction principle".

view this post on Zulip Mario Carneiro (Nov 02 2018 at 19:35):

@Neil Strickland Another way to read "this is inductive-inductive" is "lean does not have the axioms to justify that this is a valid construction". So you have to find another way to justify it to lean. In this case, the important part is that n increases in all the constructors, so this is actually a mutually recursive definition of a family of types, which lean can do well enough. We have

partition 0 = unit
partition (succ n) = partition n + Σ p : partition n, blocks n p
blocks 0 p = empty
blocks (succ n) (inl p) = blocks n p + 1
blocks (succ n) (inr <p, b>) = blocks n p

view this post on Zulip Reid Barton (Nov 02 2018 at 19:40):

This looks a lot like my attempt which Lean rejected, so I'm curious to see how you convince it the definition is valid...

view this post on Zulip Mario Carneiro (Nov 02 2018 at 19:40):

and you can define the pair <partition n, blocks n> by plain primitive recursion

view this post on Zulip Neil Strickland (Nov 02 2018 at 19:52):

Thanks, I will try that approach.

view this post on Zulip Mario Carneiro (Nov 02 2018 at 19:55):

def partblock :   Σ T : Type, T  Type
| 0 := unit, λ _, empty
| (n+1) := (partblock n).1  Σ p : (partblock n).1, (partblock n).2 p,
  λ x, sum.cases_on x
    (λ p, option ((partblock n).2 p))
    (λ p, (partblock n).2 p.1)

def partition (n : ) := (partblock n).1
def blocks {n : } : partition n  Type := (partblock n).2
def partition.null : partition 0 := unit.star
def partition.add {n} : partition n  partition (n+1) := sum.inl
def partition.join {n} (p : partition n) (b : blocks p) : partition (n+1) := sum.inr p, b
def old_block {n} {p : partition n} : blocks p  blocks p.add := option.some
def new_block {n} {p : partition n} : blocks p.add := option.none
def join_block {n} {p : partition n} (b : blocks p) : blocks p  blocks (p.join b) := id

view this post on Zulip Mario Carneiro (Nov 02 2018 at 19:55):

the recursion principle is left as an exercise for the reader ;)

view this post on Zulip Reid Barton (Nov 02 2018 at 19:56):

Interesting--I wonder if eliminating the mutual recursion by hand is essential, then

view this post on Zulip Mario Carneiro (Nov 02 2018 at 19:57):

Unfortunately, since blocks n refers to partitions n the default well founded metric for mutual recursion fails

view this post on Zulip Mario Carneiro (Nov 02 2018 at 19:58):

you can hack together the right well founded relation, but dealing with that relation will dominate the size of the definition itself


Last updated: May 12 2021 at 04:19 UTC