inductive types recursive

Stream: new members

[J. O.]

what does it for an inductive type to have recursive arguments? could you give an example?

[J. O.]

i didnt really understand the explanation image.png

[Marc Huisinga]

The following is an example for two recursive arguments (using Lean 4 syntax):

inductive Foo
  -- (d : δ) = (d1 : Nat) (d2 : Nat)
  | foo (bj : ∀ (d1 : Nat) (d2 : Nat), Foo) : Foo
  | bar (bj : Foo) : Foo

[Marc Huisinga]

But, more generally, the description of inductive types in the manual is very technical and difficult to understand. You might want to read the respective section in TPIL instead: https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html

[J. O.]

thnks. im curious, how is you example recursive? like, how do recursive inductive types really work?

[Marc Huisinga]

It's recursive because the argument to the constructor of Foo contains Foo again.
These are two more concrete examples of inductive types with recursive arguments:

inductive List' (α : Type u)
  | nil : List' α
  -- `tail` is recursive
  | cons (value : α) (tail : List' α) : List' α

inductive Nat'
  | zero : Nat'
  -- `n` is recursive
  | plus_one (n : Nat') : Nat'

To construct a List' via List'.cons, you need to pass in a value and a smaller List'. This gives you a List' with one more element (value).

[J. O.]

i see. mutual recursion in iductive types works sortof the same, right?

mutual inductive even, odd
with even : Nat → Prop
| even_zero : even 0
| even_succ : ∀ n, odd n → even (n + 1)
with odd : Nat → Prop
| odd_succ : ∀ n, even n → odd (n + 1)