Zulip Chat Archive

Stream: new members

Topic: inductive types recursive


J. O. (Jan 30 2022 at 17:51):

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

J. O. (Jan 30 2022 at 17:52):

i didnt really understand the explanation image.png

Marc Huisinga (Jan 30 2022 at 17:58):

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 (Jan 30 2022 at 17:58):

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. (Jan 30 2022 at 18:12):

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

Marc Huisinga (Jan 30 2022 at 18:19):

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. (Jan 31 2022 at 02:01):

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)

Last updated: Dec 20 2023 at 11:08 UTC