Zulip Chat Archive

Stream: general

Topic: rules of inductive types


Leonard Wiechmann (Feb 16 2022 at 14:54):

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 (Feb 16 2022 at 15:01):

(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 (Feb 16 2022 at 15:11):

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

Patrick Massot (Feb 16 2022 at 15:11):

We urgently need a new emoji

Patrick Massot (Feb 16 2022 at 15:12):

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

Mario Carneiro (Feb 16 2022 at 15:17):

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 (Feb 16 2022 at 15:20):

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 01\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 uu or max(u,v)max(u, v) (where uu and vv are variables) is a counterexample, because uu is neither always 0 nor always nonzero.

Leonard Wiechmann (Feb 16 2022 at 16:18):

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 (Feb 16 2022 at 16:18):

Mario Carneiro said:

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

I see, that's a good example!

Leonard Wiechmann (Feb 16 2022 at 16:32):

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


Last updated: Dec 20 2023 at 11:08 UTC