kernel extension: refining inductives?

Stream: lean4

[Joachim Breitner]

I should probably write these ideas down more properly and work through them to find the flaws myself, but maybe you’ll excuse me conveying half-baked ideas in order to be told why it can’t be done :-)

Goals

I have three goals in mind here

• Right now the kernel has built-in support for nested recursion. It would be desirable to pull most of that complexity out of the kernel, leaving only in the kernel what really needs to be there.
• If what’s left in the kernel is simpler, maybe it can be reasonably made to support nested recursion with indices.
• If the stars align well, we might actually get recursion through List.map or so (this is the part that I didn’t think through yet)

Prelude: refining axioms

To warm up, I’d like to pose this question: Can we “safely” refine an axiom to a definition after the fact?

Say we define axiom foo : ty, then do some more declaration, and then tell the kernel: “Actually, here is a definition for foo; def foo : ty := e, just forget that it was an axiom before and from now on consider it a definition.

It seems to me that this operation might be safe, after all, nothing in the environment could depend on a property of foo that will be no longer true, won't it?

Probably to preserve certain metatheoretical properties of the system, the kernel should check that e does not (transitively) depend on foo itself, to avoid cyclical definitions. That’s fine.

Refining inductives

Assuming the above holds water, and thinking of the inductive command as morally introducing a bunch of axioms (the type former, the constructors, the recursor), I wonder: Can we do a similar environment surgery with inductives?

Maybe something like this: For an inductive T, given proposed definition values for the “axioms” T, T.con and T.rec (say, T', con' and rec') such that

• the types of T and T' agree
• the type of T.con with T' substituted for T' agrees with the type of con'
• the type of T.rec with T' substituted for T' agrees with the type of rec'
• the iota-rule for T.rec, which states that T.rec … T.con = e, still holds definitionally: T.rec' … T.con' = e (probably under suitable substitutions)
• some more conditions to avoid cyclic definitions
  it we can replace the inductive definition of T, T.con and T.rec with plain definitions.

Intuitively it feels sounds, and a soundness proof that constructs a model of our types should hopefully still go through when we give a model of the type explicitly (and later).

Silly example

For example, presumably we could add the definitions (modulo typos)

def Nat := List ()
def Nat.zero := @List.nil ()
def Nat.succ := fun (xs : List ()) => @List.cons () () xs
def Nat.rec := @List.rec () -- in general this may be more involved

to subsume the existing Nat, could we?

Why the bother?

As alluded to above, my hope would be that we can move the kernel's construction for nested inductives out of the kernel and leave only code to check and perform this surgery. For an inductive like

data Tree where | node : List Tree → Tree

we’d first generate a mutual inductive involving Tree and ListTree (like the kernel internally already does), and then afterwards replace ListTree with List Tree. In particular ListTree.rec would be replaced with a suitable application of List.rec, and than in tern might allow us to actually allow

def Tree.size : Tree → Nat
  | node ts => ts.foldl (. + .size) 0

as a structural definition, as long as the List.fold itself is defined in terms of Tree.rec. (Ah, I should think if this still holds with the .brecOn instead of .rec).

(If this holds, maybe we could even go further and let the kernel only support non-mutual inductives, and let the elaborator perform the necessary encoding to define a non-mutual type first (using idices?), and then use this kind of post-hoc surgery to recover the definitions that the user wrote, including nice definitional properties.)

So?

Very likely someone has thought about this before and found good reasons why it just doesn’t work. Does someone here know more?

[Arthur Adjedj]

While I don't know the specifics of the kernel at the time, I believe Lean 3's kernel did not handle mutual/nested inductives by itself (according to this comment), but instead relied on a translation to indexed inductive types like the one you're describing. Regarding the handling of the recursor, a first look at the code makes me believe this sort of axiomatic juggling wasn't really necessary. Since the recursor between the base mutual type and the indexed encoding are different (namely, the indexed version has only one motive), the "new" recursor is instead written as a def using the indexed version. As for nested inductive types, It looks like the whole reduction strategy was made using sizeofs. I am not sure how this implementation would handle i.e reflexive nested datatypes such as

inductive Tree (α : Type u) : Type u
  | node : (ℕ → list Tree) → Tree

Trying this on the online Lean 3 web editor, it seems to be looping indefinitely ?

In any case, I think the main reason to avoid using the encodings (and possibly the main reason why they were ditched in the first place ?) is performance. This seems to be shortly described here, but I think there should be more to the story.

[Arthur Adjedj]

If what’s left in the kernel is simpler, maybe it can be reasonably made to support nested recursion with indices.

As for this, my opinion is that a working solution to handle this would be to modify the kernel's internal translation layer between nested and mutual types to handle these cases. To be more precise, after having experimented on this some time ago, it looks like any such nested inductive can be encoded as a mutual type by having the free variables present in the nested occurence become indices of the nested translation.
For example, this (nonsensical) nested indexed inductive

inductive Foo : Type → Type 1
  | mk : Option (Foo (Unit × α)) → Foo α

Could be encoded as

mutual
inductive OptionFoo : Type → Type 1
  | none {α} : OptionFoo α
  | some {α} (x : Foo α) : OptionFoo α

inductive Foo : Type → Type 1
  | mk : OptionFoo (Unit × α) → Foo α
end

I have an experiment fork here which aims to add this "management of free variables" feature to the nested -> mutual preprocessor. It doesn't work (yet) on any truly complex examples, but this basic implementation, and the examples I've met along the way make me confident that this translation can be done in most, of not all cases.

[Joachim Breitner]

Thanks for digging up that commend and the other references!

The performance problem mentioned in that comment (simp only indexing on the head symbol) should no longer be the case with the discrimination tree of lean4).

Just adding this feature to the kernel is of course an option, if extending the trust base is fine, or if it's needed for performance, and it’s good to see that you seem to have figured out most of it.

Although that would not provide the other benefit, namely allowing nested recursion in the form of

def Tree.size : Tree → Nat
  | node ts => ts.foldl (. + .size) 0

would it?

[Arthur Adjedj]

Just adding this feature to the kernel is of course an option, if extending the trust base is fine

I think such a modification to the kernel wouldn't have a big impact on the size of the TCB. After all, all important checks (namely universe sizes, strict positivity, the generation of recursors etc...) are made after the translation into mutual types, which means that, as long as the translation doesn't produce an ill-formed inductive type (which would i.e contain fvars/mvars in its type and whatnot) (which would throw an error at that point), and as long as the translation back from mutual to nested doesn't change much (and, from my experiment, it looks like it would be largely the same), then the code could be just as trustable IMO.

Although that would not provide the other benefit

It wouldn’t, no. I don’t see any obvious way to manage these things, let alone a solution that would imply tinkering with the kernel.

[Joachim Breitner]

Yes, kernel tinkering would be required in any case for that.

[Joachim Breitner]

If we allow ourselves more kernel tinkering, then we could achieve that by extending the “translation back” to not just replace OptionFoo α with Option (Foo α) in the types of the constructors and the recursors, but also in the reduction rules for Foo.rec replace OptionFoo.rec with a suitable instantiation of Option.rec (withFoo.rec appearing in the minor premises). If finding this instantiation is of manageable complexity for doing it in kernel, this would maybe admit the definitional equalites we’d need for nested recursion.

[Mario Carneiro]

I would prefer we have a better soundness story for kernel extensions than "it seems like it should work". At the very least, there should be a precise description of the semantics and ideally a proof of soundness of the reduction relative to other things we understand. Certainly keep me in the loop for any kernel changes, because this will significantly impact lean4lean (both the kernel and the theorem statements).

[Mario Carneiro]

I would love to see nested inductives removed from the kernel, but adding definitional equalities after the fact is problematic because it affects the overall rewrite system, and the wrong things can cause normalization to diverge.

[Mario Carneiro]

Arthur Adjedj said:

As for nested inductive types, It looks like the whole reduction strategy was made using sizeofs. I am not sure how this implementation would handle i.e reflexive nested datatypes such as

inductive Tree (α : Type u) : Type u
  | node : (ℕ → list Tree) → Tree

The lean 3 implementation was both buggy and incomplete, but the correct mutual encoding for that example is:

mutual
inductive Tree (α : Type u) : Type u
  | node : (ℕ → ListTree α) → Tree α

inductive ListTree (α : Type u) : Type u
  | nil : ListTree α
  | cons : Tree α → ListTree α → ListTree α
end

which itself can be reduced to

inductive TreeKind | Tree | ListTree

inductive TreeGen (α : Type u) : TreeKind → Type u
  | node : (ℕ → TreeGen α .ListTree) → TreeGen α .Tree
  | nil : TreeGen α .ListTree
  | cons : TreeGen α .Tree → TreeGen α .ListTree → TreeGen α .ListTree

def Tree (α : Type u) := TreeGen α .Tree

[Joachim Breitner]

Mario, no worries, this is me musing on a weekend, so no changes imminent :-). And I absolutely agree that “it seems it should work” is the beginning, not the end - hence me asking the experts here.

What is your sense of the simpler “Prelude” suggestion above, about replacing axioms with compatible definitions? Would that be sound?

In which formal setting would one try a soundness proof, or are we not there yet where we can formally proof soundness of extensions?

(My reduction argument at least for the axiom replacement would be to relate it to the environment produces when it was a definition from the start, trying to show that all typing judgments still hold with the axiom instantiated. For refining a non-mutual inductive the same might work; for refining one of a mutual inductive the argument might need to be more involved, and could maybe be based on a soundness proof that constructs a model, by choosing the “right” model initially.)

[Joachim Breitner]

So, looking at this from the angle that making the in-kernel translation of nested inductives more powerful, I do wonder:
Isn’t it a bit inconsistent that when rewriting back from the auxillary type (ListTree) to the desired type (List Tree), we rewrite the type and the constructors, but we don’t rewrite the recursor?

More concretely:

import Lean.Elab.Command

inductive Tree where | node : List Tree → Tree

open Lean Meta

set_option pp.explicit true
set_option pp.funBinderTypes true

-- This the generated rule's RHS.
-- The type and constructors of the auxillary `ListTree` have been replaced
-- by their `List Tree` counterpats, but we still see `Tree.rec_1`.
-- Can we replace that with `List.rec`?

/--
info: fun
    (motive_1 : Tree → Sort u)
    (motive_2 : List Tree → Sort u)
    (node : (a : List Tree) → motive_2 a → motive_1 (Tree.node a))
    (nil : motive_2 (@List.nil Tree))
    (cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (@List.cons Tree head tail))
    (a : List Tree) =>
  node a (@Tree.rec_1 motive_1 motive_2 node nil cons a)
-/
#guard_msgs(whitespace:=lax) in
run_meta do
  let recVal ← getConstInfoRec ``Tree.rec
  logInfo recVal.rules[0]!.rhs

-- Here is a definition with the same type as `Tree.rec_1`, but referring to `List.rec` instead.

noncomputable
def Tree.rec_1_impl
    {motive_1 : Tree → Sort u}
    {motive_2 : List Tree → Sort u}
    (node : (a : List Tree) → motive_2 a → motive_1 (Tree.node a))
    (nil : motive_2 (@List.nil Tree))
    (cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (@List.cons Tree head tail))
    (ts : List Tree) :=
  @List.rec Tree motive_2 nil (fun (head : Tree) (tail : List Tree) ih_tail => cons head tail (@Tree.rec motive_1 motive_2 node nil cons head) ih_tail) ts


-- With this, I could imagine the following rule RHS'

noncomputable
def proposedRuleRHS
    (motive_1 : Tree → Sort u)
    (motive_2 : List Tree → Sort u)
    (node : (a : List Tree) → motive_2 a → motive_1 (Tree.node a))
    (nil : motive_2 (@List.nil Tree))
    (cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (@List.cons Tree head tail))
    (a : List Tree) :=
    node a (@Tree.rec_1_impl motive_1 motive_2 node nil cons a)

I wonder if this rewriting (if done correctly) was sound? And if so, whether it's within the complexity budget we have for the kernel.

So what is this rewriting? Vaguely, pass the motives corresponding to the desired type to its recursor, and and F-args for its constructor, with every x_ih parameter that isn't provided by the new desired recursor, i.e. for a new type, instantiated with that type’s .rec and full set of motives/F-args.

After this there should be no more auxillary types, constructors or recursors visible.

@Arthur Adjedj maybe something to try on your various experimental branches :)

(I’m recording this idea at https://github.com/leanprover/lean4/issues/4749 for posterity.)

[Arthur Adjedj]

To give an update on this: I have experimented more with nested indexed inductive types at the kernel level, and am confident I have a robust implementation here. The main changes in this branch are as described previously: the kernel now collects all bvars present in the parameters of a nested occurrences, and adds them as indices of the auxiliary inductive associated with the nested occurrence, as well as carry this information around to ensure the translation back to be correct. One major change induced by this is that the recursors' shape changes slightly in nested indexed inductive types. I'll show it through an example:
Consider the following type:

/- Trees of depth at most n-/
inductive Test : Nat → Type
  | foo {n : Nat} :List (Test n) → Test n.succ

Because n appears freely in the parameter of List, the auxiliary translation now needs to take this into account, producing the following mutual inductive:

mutual
inductive Test : Nat → Type
  | foo {n : Nat}: ListTest n → Test n.succ

inductive ListTest : Nat → Type
  | nil {n : Nat} : ListTest n
  | cons {n : Nat} : Test n → ListTest n → ListTest n
end

All well and good. This leads to the following (mutual) recursor:

ListTest.rec.{u} {motive_1 : (a : Nat) → Test a → Sort u} {motive_2 : (a : Nat) → ListTest a → Sort u}
  (foo : {n : Nat} → (a : ListTest n) → motive_2 n a → motive_1 n.succ (Test.foo a))
  (nil : {n : Nat} → motive_2 n ListTest.nil)
  (cons :
    {n : Nat} → (a : Test n) → (a_1 : ListTest n) → motive_1 n a → motive_2 n a_1 → motive_2 n (ListTest.cons a a_1)) :
  {a : Nat} → (t : ListTest a) → motive_2 a t

However, the translated recursor now looks like this:

Test.rec_1.{u} {motive_1 : (a : Nat) → Test a → Sort u} {motive_2 : {n : Nat} → List (Test n) → Sort u}
  (foo : {n : Nat} → (a : List (Test n)) → @motive_2 n a → motive_1 n.succ (@Test.foo n a))
  (nil : {n : Nat} → @motive_2 n (@List.nil (Test n)))
  (cons :
    {n : Nat} →
      (head : Test n) →
        (tail : List (Test n)) → motive_1 n head → @motive_2 n tail → @motive_2 n (@List.cons (Test n) head tail))
  {n : Nat} (t : List (Test n)) : @motive_2 n t

Notice that despite the List type not having indices, the recursor's shape now looks like it does. Because of this, it is necessary that the reduction algorithm for recursors now handle a notion of "added indices" (implementation here, which makes use of lean4#5679). Another solution would be to implement Joachim's lean4#4749, so that these auxiliary recursor would be rewritten into the right recursors.

The branch currently compiles all of lean core and passes all tests. One remaining issue is that the generation of SizeOf instances currently doesn't work on nested indexed inductives, probably because of the change in shape of the auxiliary recursors. Other than that, all other helper definitions such as below, brecOn, casesOn, noConfusion etc... all work as expected. Examples of inductive types that used to not be handled can be found here.

[Joachim Breitner]

That’s exciting! Do we have an RFC or issue describing your design here, just to have something more discoverable than a zulip thread?

I assume these “extra recursors” will also have t be taken into account in other places in lean, so maybe lean4#4749 would be a nice alternative that keep the complexity a bit more isolated.

Overall the complexity of this feature is a bit scary. If I’d have to bet on where an unsoundness bug (due to a kernel programming oversight, not fundamentally) would be found, the mutual inductive handling would be high on my list.

[Arthur Adjedj]

Do we have an RFC or issue describing your design here, just to have something more discoverable than a zulip thread?

I don't believe so, though there is an issue linked to this feature, namely lean4#2195. I can write a more detailed description in an RFC.

I assume these “extra recursors” will also have t be taken into account in other places in lean, so maybe lean4#4749 would be a nice alternative that keep the complexity a bit more isolated.

I do agree that translating auxiliary recursors would be ideal.

If I’d have to bet on where an unsoundness bug would be found, the mutual inductive handling would be high on my list.

I must agree with this. The most complex part of the kernel is certainly the handling/checking of inductive types. It has to manage many different elements and it's easy to get lost in the details.
One big issue I have seen when working on the kernel is that despite inductive types and their constructors being checked to be type-correct during their constructions (namely here and here), recursors (and their reduction rules) never get type-checked, and the kernel is happy to add a possibly ill-typed recursor to the environment. I believe the kernel would benefit from checking those things before adding them to the environment, and throw an error if something wrong happened there.

[Joachim Breitner]

I believe the kernel would benefit from checking those things before adding them to the environment, and throw an error if something wrong happened there.

That would just be a sanity check against implementation bugs, right? There is no way a user can somehow make the kernel construct an ill-typed constructor?

[Arthur Adjedj]

It would be yes. I am arguing that if a kernel programming oversight was to produce an ill-typed recursor, the kernel would still add it to the environment, and that checking this would add more trust to the system.

[Joachim Breitner]

Yes, that shouldn't hurt and not be too expensive either.

[Arthur Adjedj]

To test the limits of my implementation, I've tried to see if any "beefy" nested indexed inductive would work on that branch. I've decided to formalize a logical relation for Martin-Löf Type Theory (this is a direct port of the logrel-coq formalization described in Martin-Löf à la Coq) which is an indexed inductive which relies on nested packings to function. I am happy to say that the following definition compiles locally with no issue.

[Mario Carneiro]

Just a reminder to relevant parties: Please ping me when anything in the kernel changes. I am maintaining a carbon copy of the C++ code in lean and I want to make sure it stays that way

[Mario Carneiro]

Re: type-incorrect recursors, proving these types are correct is of course on the agenda for lean4lean, although it might be a while before the project gets that far

[Max Nowak 🐉]

For the last few months' spare time, I have been working on giving a model to a rather complicated inductive type, which involves induction-induction, induction-recursion, and recursion-recursion (so, an "IIRRT" I guess?). The approach I am pursuing to make this possible in Lean, is to split the IIRRT up into a type-index-erased (E) half and a wellformedness (W) half, and then at the very end stitch those together using subtypes. Then you can define a recursor for this IIRRT, and prove iota rules for it, which miiiiiight (not sure) even hold definitionally but would be extremely non-performant either way. In order to provide a model, you have to prove things about the E half before you can even state the corresponding W half, i.e. your IIRRT-mutual block would have to also contain theorems inside the mutual block; but this is not a problem if you split it up into E and W halves. At the very end you end up with a whole bunch of defs for the type former(s), your recursive functions, the recursor, and theorems about the recursor.

I would love to be able to use this IIRRT in a comfortable way, that is: Users should never see the inner workings of it (the E and W halves), users should be able to use pattern matching using the derived recursor, and iota rules should hold definitionally without a big performance hit.

It sounds like refining inductives might provide a way to make this possible?

If this is possible, we could add induction-induction and (small) induction-recursion to Lean, and make it actually pleasant to use! All while actually making the kernel smaller.

[Max Nowak 🐉]

Basically I want Lean to trust me and give me definitional iota rules, because I can provide a model for it. And then I want Lean to forget the model.

[Joachim Breitner]

Max Nowak 🐉 said:

Basically I want Lean to trust me and give me definitional iota rules, because I can provide a model for it. And then I want Lean to forget the model.

That sounds useful! It’s not quite what I suggested in the present thread, which goes the other way: Let the kernel construct an inductive type (with all the limitations this has), then give a model of this type using other types, and then make the first type disappear (by making the type former, constructor and recursors definitions).

That’s probably too limited for what you want, which is from a model create a type that the kernel wouldn’t create itself otherwise.

[Max Nowak 🐉]

I think it makes sense to first provide a model (which you can do already), and then have the ability to wave a magic wand and enchant it into a proper inductive(-recursive) type.

[Joachim Breitner]

I’m not disagreeing

[Max Nowak 🐉]

Neither am I. But yeah it's a slightly different approach.

[Max Nowak 🐉]

This would be super cool

[Max Nowak 🐉]

You could strip mutual inductive types from the kernel entirely this way, and only have indexed W-types as the foundation. Then build your ladder into more and more complicated inductive types, but none of that is part of the trusted code base now, and it would only use the kernel's magic wand, provided you can give it a model.

[Zhanrong Qiao]

I guess this might be understood like this: axioms are actually assumptions (like the assumptions the variable command introduces), which turn into additional lambdas before every subsequent definition, and "refining axioms" corresponds to applying concrete arguments to the lambdas.

However, this still does not allow additional definitional equalities to be introduced; at the very least, constraints must be added to preserve confluence and therefore subject reduction, otherwise it can go wild even when those are valid propositional equalities...? (Though the examples in this paper all involve additional assumptions...)

[Zhanrong Qiao]

(unless those are defeqs derivable from existing defeqs, in which case the refined axioms are more like additional lets prefixed to every definition)