rules of inductive types

Stream: general

[Leonard Wiechmann]

hey all, I've been studying the rules of inductive types.
in particular, I wanted to test my understanding of 2 rules, but found some unexpected things:

1) recursive arguments may not be used in types of other arguments.

-- this is fine.
inductive t1: Type
| i1 (a: nat) (aa: a = a) (x: t1) : t1

-- same as t1, but with `x` first.
-- why does this not work?
-- error: "invalid occurrence of recursive arg#2 of 'foo_1.t2.i1', the body of the functional type depends on it."
-- this works if I remove `aa`.
inductive t2: Type
| i1 (x: t2) (a: nat) (aa: a = a) : t2

-- same as t1, but with something using `x`.
-- expected to not work, because recursive arguments may not be used.
-- the error however does not really suggest that to me: "nested occurrence 'eq.{1} foo_1.t3 x' contains variables that are not parameters" (it does not come from inductive.cpp)
inductive t3: Type
| i1 (a: nat) (aa: a = a) (x: t3) (xx: x = x) : t3

2) the sort levels of the constructor arguments must be less than or equal to the sort level of the inductive type, unless it lives in Prop.
here, I think there is a mistake in the paper:
image.png
shouldn't that also use imax?
this code works, but shouldn't according to my understanding of the formula:

def      T0: Sort 0 := ∀ (n: nat), n = n
def      T1: Sort 1 := nat -> nat
def      T2: Sort 2 := nat -> Sort 1

inductive t1: Sort 2
| i0 (a: T0) : t1
| i1 (a: T1) : t1
| i2 (a: T2) : t1

inductive t2: Sort 0
| i0 (a: T0) : t2
| i1 (a: T1) : t2  -- these should not work,
| i2 (a: T2) : t2  -- because not {1,2} <= 0

[Leonard Wiechmann]

(re rule #2): this comment from the code suggests that both rules use the same condition (with imax) to me:
"The universe levels of arguments b and u must be smaller than or equal to l_k in I.
When the environment is marked as impredicative, then l_k must be 0 (Prop) or must be different from zero for any instantiation of the universe level parameters (and global level parameters)."
though, to be honest, I don't really understand it either: isn't "(l_k must be 0 or must be different from zero) for any ..." just equivalent to `true for any ..."

[Mario Carneiro]

Yes, that is a typo in the paper. The actual code uses the condition $\ell'\le \ell \lor \ell\le 0$, which can be equivalently written $imax(\ell',\ell)\le\ell$

[Patrick Massot]

We urgently need a new emoji

[Patrick Massot]

The one we use when someone actually read that paper (and even finds a typo :open_mouth: )

[Mario Carneiro]

Regarding (1), lean has some slightly more restrictive rules for recursive arguments to the left of non-recursive arguments, likely due to historical factors (this was not originally allowed). I think the check is just buggy here.

The t3 example is triggering the nested inductive compiler, which is an additional feature supported by the lean elaborator which is not covered in the paper because nested inductives are compiled to regular inductives for consumption by the kernel. The nested inductive compiler can't handle dependencies like this, but since it's the last system to take a crack at the inductive spec you get that error instead of the one coming from the kernel.

[Mario Carneiro]

though, to be honest, I don't really understand it either: isn't "(l_k must be 0 or must be different from zero) for any ..." just equivalent to `true for any ..."

No. This can be expressed in the paper notation as $\ell\le 0\lor 1\le \ell$, and it is not unconditionally true because $\ell$ is an expression which can contain universe variables, while the $\ell \le \ell'$ relation is universally closed over those variables. So an expression like $u$ or $max(u, v)$ (where $u$ and $v$ are variables) is a counterexample, because $u$ is neither always 0 nor always nonzero.

[Leonard Wiechmann]

Mario Carneiro said:

The t3 example is triggering the nested inductive compiler

oh, yeah! I didn't realize that eq would of course be given t3 implicitly.
I tried to "use" a recursive argument somehow. I guess this is why doing so is disallowed: because applying is never strictly positive? (edit: and applying is the only way I can think of using a recursive argument)

[Leonard Wiechmann]

Mario Carneiro said:

$max(u, v)$ (where $u$ and $v$ are variables) is a counterexample, because $u$ is neither always 0 nor always nonzero.

I see, that's a good example!

[Leonard Wiechmann]

wow, this is the clearest explanation i've found so far, props to whoever wrote it: https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#axiomatic-details