tip for nested/mutual inductive types?

Stream: lean4

[Andrew Kent]

We're trying to work with a datatype that looks roughly like the following:

inductive LLVMType
| alias (nm:String)
| array (n:Nat) (elt:LLVMType)
| struct (packed:Bool) (fields:List LLVMType)

However performing computation with such a type currently forces you to liberally apply partial or similar:

def hasAlias (nm : String) : LLVMType → Bool
  | LLVMType.alias nm' => nm == nm'
  | LLVMType.array sz elemTy => do
    hasAlias nm elemTy
  | LLVMType.struct packed fields => false
-- fail to show termination for
--  hasAlias
-- with errors
-- structural recursion cannot be used

-- well founded recursion has not been implemented yet

Any tips or tricks for how we might work with such a datatype in the near term that gives us the ability to reason about it at times? (i.e., we find ourselves occasionally wanting small propositions about computations with such a datatype and that is where the things get ugly and we're trying to decide what would be best/easiest for now).

Longer term, is this something we're hoping automation and well-founded recursion will make smoother or dare I say, pleasant? Or, will users more likely want to go the route of defining a monomorphic mutually dependent list datatype when they want to combine such types? (I do see in some of the Lean 4 tests at least manual/low level support seems to exist for the mutually recursive route, though we haven't tried that just yet).

Thanks!

[Andrew Kent]

Ah, I guess there is one other hacky workaround we could use for practical short-term purposes I can think of: just manually "unroll" our recursive functions if we really want to reason about them. While in theory an LLVM type can be arbitrarily complex... in our uses cases over the next six months, we can probably manually carve out non-recursive computations for all the LLVM types we'll see in practice.

[Mario Carneiro]

In lean 3, these kinds of lemmas are almost always proved using well founded recursion. Nested/mutual structural recursion was not supported by the lean 3 compilation strategy. In lean 4, correct nested/mutual recursors are generated by the kernel, but the equation compiler doesn't know how to detect that a mutual recursive definition can be compiled using mutual recursors, so it still falls back on well founded recursion.

I don't think that implementing well founded recursion in the same way as lean 3 should be especially difficult, especially if the has_well_founded clause is required. There is potentially room for bikeshedding the syntax though, lean 3's syntax is somewhat cumbersome. Supporting the default has_well_founded instance using the sizeof function is possible but complex, and will probably have to wait until at least some of the basic nat lemmas are available. It seems better suited to be outside the core.

[Mario Carneiro]

The strategy I always recommend in lean 3 is to avoid nested and mutual inductives and replace them with plain inductives. The reasons to do this in lean 4 are a bit different but I think the advice is still applicable, at least until all the unimplemented bits are filled in

[Mario Carneiro]

Since the kernel supports this recursion but not the equation compiler, it's also possible to compile the equations manually:

inductive LLVMType
| alias (nm:String)
| array (n:Nat) (elt:LLVMType)
| struct (packed:Bool) (fields:List LLVMType)

def hasAlias (nm : String) (ty : LLVMType) : Bool :=
  LLVMType.rec (motive_1 := λ _ => Bool) (motive_2 := λ _ => Bool)
    (λ nm' => nm == nm')
    (λ sz elemTy ih_elemTy => ih_elemTy)
    (λ packed fields ih_fields => false)
    false
    (λ hd tl ih_hd ih_tl => ih_hd || ih_tl)
    ty

Unfortunately this seems to hit yet another todo in the code, because this definition fails with

code generator does not support recursor 'LLVMType.rec' yet, consider using 'match ... with' and/or structural recursion

which is wonderfully circular. I guess you can get the best of both worlds by writing both versions:

partial def hasAlias_impl (nm : String) : LLVMType → Bool
  | LLVMType.alias nm' => nm == nm'
  | LLVMType.array sz elemTy => do
    hasAlias_impl nm elemTy
  | LLVMType.struct packed fields => false

@[implementedBy hasAlias_impl]
def hasAlias (nm : String) (ty : LLVMType) : Bool :=
  LLVMType.rec (motive_1 := λ _ => Bool) (motive_2 := λ _ => Bool)
    (λ nm' => nm == nm')
    (λ sz elemTy ih_elemTy => ih_elemTy)
    (λ packed fields ih_fields => false)
    false
    (λ hd tl ih_hd ih_tl => ih_hd || ih_tl)
    ty

which works, although it doesn't seem to suppress the code generation error

[Andrew Kent]

Ah - I searched Zulip but did not peruse the Github issues. My bad.

It looks like at least the "long term" part of my question (i.e., how would this smoothly work generally in the future) has been answered quite clearly here in case anyone is curious: https://github.com/leanprover/lean4/issues/262

TL;DR "The plan is to support mutual and nested inductive datatypes using well-founded recursion only." -- leodemoura