self reference in inductive

Stream: lean4

[Paige Thomas]

I recall being told at some point in Lean 3 that something like this doesn't work:

inductive LabeledTree (α : Type)
| mk (root : Option α) (descendent_list : List (LabeledTree α)) : LabeledTree α

because the type being defined is referenced in another inductive type, the List. I was wondering if this is still the case. Lean 4 accepted this definition, but I'm not sure what issues I may end up running into.

[Paige Thomas]

Also, if I want to refer to the items in the constructor, is this the canonical way to do so?

inductive LabeledTree (α : Type)
| mk (root : Option α) (descendent_list : List (LabeledTree α)) : LabeledTree α

compile_inductive% LabeledTree

def LabeledTree.root
  {α : Type} :
  LabeledTree α → Option α
  | mk root _ => root

def LabeledTree.descendent_list
  {α : Type} :
  LabeledTree α → List (LabeledTree α)
  | mk _ descendent_list => descendent_list

[Paige Thomas]

Or is there another way to make it builtin, like with the dot notation of structures.

[Kyle Miller]

There's no built-in way to generate accessor functions at the moment (though it occurred to me that I have a not-so-tested-one lying around: https://gist.github.com/kmill/f83401e20bc9e36624086c8eceb5b157)

[Kyle Miller]

You shouldn't need compile_inductive% unless you're using LabeledTree.rec directly to make definitions.

[Paige Thomas]

I see. Thank you.

[Paige Thomas]

Is it possible to use the self reference like that now, or is this still to be avoided?

[Kyle Miller]

My understanding is that nested inductive types are supported by the kernel now. I haven't noticed any issues with them myself.

[Kyle Miller]

A case study is that this recursive function on your tree appears to work fine and have reasonable equation lemmas:

def LabeledTree.sum {α : Type} [Add α] [Zero α] : LabeledTree α → α
  | mk root [] => root.getD 0
  | mk root (child :: descendent_list) => child.sum + LabeledTree.sum (mk root descendent_list)

#check LabeledTree.sum.eq_1
/-
LabeledTree.sum.eq_1 {α : Type} [Add α] [Zero α] (root : Option α) :
  (LabeledTree.mk root []).sum = root.getD 0
-/
#check LabeledTree.sum.eq_2
/-
LabeledTree.sum.eq_2 {α : Type} [Add α] [Zero α] (root : Option α)
  (child : LabeledTree α) (descendent_list : List (LabeledTree α)) :
  (LabeledTree.mk root (child :: descendent_list)).sum = child.sum + (LabeledTree.mk root descendent_list).sum
-/

[Paige Thomas]

What is an equation lemma?

[Paige Thomas]

Is this an issue due to the self reference in the List?
'induction' tactic does not support nested inductive types, the eliminator 'LabeledTree.rec' has multiple motives

[Paige Thomas]

cases works here, but induction gives the error.

instance (α : Type) (T : LabeledTree α) : Decidable T.isLeaf :=
  by
    cases T
    simp only [LabeledTree.isLeaf]
    infer_instance

[Paige Thomas]

Or maybe it is because there is only one constructor and no base constructor?

[Paige Thomas]

Hmm, no, it doesn't work with this either

inductive LabeledTree (α : Type)
| nil : LabeledTree α
| mk : Option α → List (LabeledTree α) → LabeledTree α

[Joachim Breitner]

Kayla Thomas said:

Is this an issue due to the self reference in the List?
'induction' tactic does not support nested inductive types, the eliminator 'LabeledTree.rec' has multiple motives

Yes. A nested inductive data type will have a recursor with one motive for LabeledTree and one for List LabeledTree. Your options are, I think,

• Define your theorem recursively

• Instantiate the second inductive motive explicitly
  induction T using LabeledTree.rec (motive2 := fun TS => … TS …)

• Don’t use tactics, but write := LabeledTree.rec (motive1 := …) (motive2 := …) … explicitly.

Probably the first one is simplest.

[Paige Thomas]

I see. What goes in the ...s?

[Edward van de Meent]

• use match T with <- i recommend this one

[Edward van de Meent]

possibly use a mutual block

[Paige Thomas]

That won't be recursive on the structure of T will it?

[Edward van de Meent]

it will if you refer to the statement in the statement.

[Paige Thomas]

Oh, you are referring to the first one that Joachim listed?

[Edward van de Meent]

ah, yes. my bad.

[Paige Thomas]

I see.

[Paige Thomas]

No problem.

[Paige Thomas]

Is there any chance it is possible to make this work more simply with the induction tactic at some point in the future?

[Floris van Doorn]

Note that one thing that doesn't work well with these nested inductive types is to use List-operations in recursive definitions. For example, the following is reasonable to write, but Lean doesn't support it (yet?):

import Mathlib.Algebra.BigOperators.Group.List

inductive LabeledTree (α : Type) where
  | mk (root : Option α) (descendents : List (LabeledTree α)) : LabeledTree α

def LabeledTree.sum {α : Type} [Add α] [Zero α] : LabeledTree α → α
  | mk root [] => root.getD 0
  | mk root l => l.map LabeledTree.sum |>.sum

[Jakob von Raumer]

Would be cool if that would work some day. I have a lot of metaprogramming stuff that's recursive in that way and needs to be made partial right now

[Daniel Weber]

You can show that this terminates by mapping on l.attach