Complicated induction: documentation?

Stream: lean4

[Siddhartha Gadgil]

Lean 4 seems to support a very general form of induction, strictly more general than HoTT. I ran into this because Syntax nodes involve Array Syntax, and trepplein 3 does not support this.

My question is whether recursors of inductive types of a general form are documented anywhere. I looked at Mario's thesis and the section was not detailed enough for me to understand the following rather gothic example (or even the more modest one with Array Syntax.

inductive MyList (α : Type u) where
  | nil : MyList α
  | cons (head : α) (tail : MyList α) : MyList α

inductive MyListTree (α : Type u) where
  | leaf (a: α) : MyListTree α
  | node (children: MyList (MyListTree α))(family : Nat → List (MyListTree α )) : MyListTree α

#check MyListTree.rec /- {α : Type u} →
  {motive_1 : MyListTree α → Sort u_1} →
    {motive_2 : MyList (MyListTree α) → Sort u_1} →
      {motive_3 : List (MyListTree α) → Sort u_1} →
        ((a : α) → motive_1 (MyListTree.leaf a)) →
          ((children : MyList (MyListTree α)) →
              (family : ℕ → List (MyListTree α)) →
                motive_2 children → ((a : ℕ) → motive_3 (family a)) → motive_1 (MyListTree.node children family)) →
            motive_2 MyList.nil →
              ((head : MyListTree α) →
                  (tail : MyList (MyListTree α)) → motive_1 head → motive_2 tail → motive_2 (MyList.cons head tail)) →
                motive_3 [] →
                  ((head : MyListTree α) →
                      (tail : List (MyListTree α)) → motive_1 head → motive_3 tail → motive_3 (head :: tail)) →
                    (t : MyListTree α) → motive_1 t
      -/

I can try to work this out and document it, but if there is someplace I can look up that would be useful.

[Mario Carneiro]

My thesis does not cover nested inductives, as they were not primitive in lean 3

[Mario Carneiro]

I believe Sebastian's thesis has a section on nested inductives, but IIRC it does not go into enough detail to work as a spec

[Mario Carneiro]

Probably the best precise source at the moment is https://github.com/digama0/lean4lean/blob/master/Lean4Lean/Inductive/Add.lean#L473-L672 (I intend to add comments once the bugs are ironed out, there are also some comments in the original source). My intention is to unpack this code into a spec sometime soon

[Mario Carneiro]

In other words, no there is no documentation

[Mario Carneiro]

I can give the gist of the algorithm though. It helps if you are familiar with the nested inductive algorithm from lean 3. The first pass is to collect all the mutual inductives needed. We walk the inductive specification looking for inductive types with our inductive(s) in the parameters, and add them to a list. We also have to recursively walk the specifications of these inductives (after applying our instantiation) looking for more inductive types involving our types. Once the list reaches a fixed point, we construct a mutual inductive with all of these inductive specifications and defer to the regular mutual inductive mechanism. But we intercept the resulting inductive type and edit the constructors and recursor to remove references to the auxiliary mutual inductive types we created.

[Mario Carneiro]

In your example, we walk the inductive specification looking for occurrences of inductive types containing MyListTree in the parameters, and we find two: MyList (MyListTree α), and later List (MyListTree α). We then walk the inductive spec of MyList with the parameter substituted for α, but we only find MyList (MyListTree α) again. Similarly, we walk List (MyListTree α) and find MyListTree α and List (MyListTree α), nothing new. So the first pass terminates with the following auxiliary types:

• MyListTree α
• MyListTree.aux_1 α := MyList (MyListTree α)
• MyListTree.aux_2 α := List (MyListTree α)

We construct the following mutual inductive:

mutual
inductive MyListTree (α : Type u) where
  | leaf (a: α) : MyListTree α
  | node (children: MyList.aux_1 α) (family : Nat → MyListTree.aux_2 α) : MyListTree α

inductive MyListTree.aux_1 (α : Type u) where
  | nil : MyListTree.aux_1 α
  | cons (head : MyListTree α) (tail : MyListTree.aux_1 α) : MyListTree.aux_1 α

inductive MyListTree.aux_2 (α : Type u) where
  | nil : MyListTree.aux_2 α
  | cons (head : MyListTree α) (tail : MyListTree.aux_2 α) : MyListTree.aux_2 α
end

This is passed to the add_inductive function, which constructs three types, 6 constructors and 3 recursors for the 3 mutual inductive types. This is added to an environment aux_env, but this is not the real environment we will be using. The recursor for MyListTree looks something like this:

recursor MyListTree.rec : {α : Type u} →
  {motive_1 : MyListTree α → Sort u_1} →
    {motive_2 : MyListTree.aux_1 α → Sort u_1} →
      {motive_3 : MyListTree.aux_2 α → Sort u_1} →
        ((a : α) → motive_1 (MyListTree.leaf a)) →
          ((children : MyListTree.aux_1 α) →
              (family : ℕ → MyListTree.aux_2 α) →
                motive_2 children → ((a : ℕ) → motive_3 (family a)) → motive_1 (MyListTree.node children family)) →
            motive_2 MyListTree.aux_1.nil →
              ((head : MyListTree α) →
                  (tail : MyListTree.aux_1 α) → motive_1 head → motive_2 tail → motive_2 (MyListTree.aux_1.cons head tail)) →
                motive_3 MyListTree.aux_2.nil →
                  ((head : MyListTree α) →
                      (tail : MyListTree.aux_2 α)) → motive_1 head → motive_3 tail → motive_3 (MyListTree.aux_2.cons head tail)) →
                    (t : MyListTree α) → motive_1 t

(Note that there are two other recursors, at MyListTree.rec_1 and MyListTree.rec_2.) We now postprocess this term to replace all occurrences of MyListTree.aux_1 α with MyList (MyListTree α), using the mapping generated at the beginning, and similarly replace MyListTree.aux_2 α with List (MyListTree α). The constructors are just replaced by corresponding (instantiated) constructors from the original inductive. The result is the recursor that you have shown.

[Siddhartha Gadgil]

Thanks @Mario Carneiro I will work with the above description, and the Lean4Lean source and "follow my nose" to try to implement this.

[Siddhartha Gadgil]

In the case of Syntax, whose node has Array Syntax, I take it that there are auxiliary inductive types for Array Syntax and then List Syntax. We have recursors for each of these from which the big one is built.

[Mario Carneiro]

yes

[Siddhartha Gadgil]

One further question about the reduction rules. To be concrete, let me consider a simpler example:

inductive ArrayTree where
  | leaf (n: Nat) : ArrayTree
  | node (node: Array ArrayTree) : ArrayTree

where we have

#check ArrayTree.rec /- {motive_1 : ArrayTree → Sort u} →
  {motive_2 : Array ArrayTree → Sort u} →
    {motive_3 : List ArrayTree → Sort u} →
      ((n : ℕ) → motive_1 (ArrayTree.leaf n)) →
        ((node : Array ArrayTree) → motive_2 node → motive_1 (ArrayTree.node node)) →
          ((data : List ArrayTree) → motive_3 data → motive_2 { data := data }) →
            motive_3 [] →
              ((head : ArrayTree) → (tail : List ArrayTree) → motive_1 head → motive_3 tail → motive_3 (head :: tail)) →
                (t : ArrayTree) → motive_1 t -/

Am I correct that we have reduction rules corresponding to tuples of constructors. For example, in the above we will have a reduction rule corresponding to ArrayTree.node (Array.mk (head :: tail))?

[Trebor Huang]

HoTT is not a single formal system. Some varieties have nested inductives too, such as Agda. Agda doesn't generate recursors at all though.

[Siddhartha Gadgil]

Trebor Huang said:

HoTT is not a single formal system. Some varieties have nested inductives too, such as Agda. Agda doesn't generate recursors at all though.

By "HoTT" I meant "book HoTT", the foundations in the HoTT book. This is where I first learnt type theory.

[Mario Carneiro]

@Siddhartha Gadgil said:

Am I correct that we have reduction rules corresponding to tuples of constructors. For example, in the above we will have a reduction rule corresponding to ArrayTree.node (Array.mk (head :: tail))?

No, reduction rules apply only to single constructors. In this example there are 5 reduction rules for 3 recursors:

ArrayTree.rec leaf node mk nil cons (.leaf n)
  = leaf n
ArrayTree.rec leaf node mk nil cons (.node a)
  = node a (ArrayTree.rec_1 leaf node mk nil cons a)
ArrayTree.rec_1 leaf node mk nil cons (.mk data)
  = mk data (ArrayTree.rec_2 leaf node mk nil cons data)
ArrayTree.rec_2 leaf node mk nil cons .nil
  = nil
ArrayTree.rec_2 leaf node mk nil cons (.cons head tail)
  = cons head tail (ArrayTree.rec leaf node mk nil cons head) (ArrayTree.rec_2 leaf node mk nil cons tail)

[Siddhartha Gadgil]

Thanks @Mario Carneiro - without the auxiliary recursors I could not figure out any valid simplification rules except of the form I mentioned. But now it is all clear.

[Siddhartha Gadgil]

I was trying to work out what to do with the following example, and found that it is forbidden. So I assume that we cannot have families and nested types together. I am pasting the example for the record and so someone who knows can confirm.

inductive VectorTree where
  | leaf (n: Nat) : VectorTree
  | node (n: ℕ) (branches: Vector VectorTree n) : VectorTree

[Mario Carneiro]

nested inductives don't support definitions at all

[Mario Carneiro]

even just

def List' (α : Type) := List α
inductive T where
  | node : List' T → T

fails

[Mario Carneiro]

if you inline the definition you get a different error:

inductive VectorTree where
  | leaf (n: Nat) : VectorTree
  | node (n: ℕ) (branches: { l : List VectorTree // l.length = n }) : VectorTree

(kernel) invalid nested inductive datatype 'Subtype', nested inductive datatypes parameters cannot contain local variables.

[Mario Carneiro]

However, if you use the classic inductive definition of Vector then it works:

inductive Vector' (α : Type) : Nat → Type
  | nil : Vector' α 0
  | cons {n} : α → Vector' α n → Vector' α (n + 1)

inductive VectorTree where
  | leaf (n: Nat) : VectorTree
  | node (n: ℕ) (branches: Vector' VectorTree n) : VectorTree

[Mario Carneiro]

which is to say, inductive families are allowed

[Siddhartha Gadgil]

Thanks. Indeed I just tried the classical definition and got this:

inductive Vec (α : Type) : Nat → Type where
  | nil : Vec α 0
  | cons (n: ℕ)(head : α) (tail : Vec α n) : Vec α  (n + 1)

inductive VectorTree where
  | leaf (n: Nat) : VectorTree
  | node (n: ℕ) (branches: Vec VectorTree n) : VectorTree


#check VectorTree.rec /-
{motive_1 : VectorTree → Sort u} →
  {motive_2 : (a : ℕ) → Vec VectorTree a → Sort u} →
    ((n : ℕ) → motive_1 (VectorTree.leaf n)) →
      ((n : ℕ) → (branches : Vec VectorTree n) → motive_2 n branches → motive_1 (VectorTree.node n branches)) →
        motive_2 0 Vec.nil →
          ((n : ℕ) →
              (head : VectorTree) →
                (tail : Vec VectorTree n) → motive_1 head → motive_2 n tail → motive_2 (n + 1) (Vec.cons n head tail)) →
            (t : VectorTree) → motive_1 t
-/

[Siddhartha Gadgil]

I am concerned that in translation to mutual inductives we end up with Vec VectorTree n which has an n that has no meaning except when associated to a constructor. Have not thought through this but any clarification is welcome.

[Mario Carneiro]

not sure what you mean by that, the mutual inductive in question is the Vec VectorTree family itself

[Mario Carneiro]

Note that the self type is only allowed to appear in the parameters, it is rejected if it is in an index

inductive Vector' : (α : Type) → Nat → Prop
  | nil : Vector' Nat 0
  | cons {α n} : α → Vector' α n → Vector' α (n + 1)

inductive VectorTree where
  | leaf (n: Nat) : VectorTree
  | node (n: ℕ) (branches: Vector' VectorTree n) : VectorTree

(kernel) arg #2 of 'VectorTree.node' contains a non valid occurrence of the datatypes being declared

[Siddhartha Gadgil]

Ah thanks. I see that the indices in the family like n become indices of the type. That makes sense.

[Joachim Breitner]

(Just a comment from the sidelines that this is a very interesting thread, and the patient and careful explanations by Mario a good example of why the lean/mathlib community is so pleasant and welcoming.)