Need help to better understand recursors and eliminators

Stream: new members

[Kevin Cheung]

I have been reading Theorem Proving in Lean 4 Chapter 7 on inductive types. At various points, it talks about recursor and eliminator in a way that seems to assume prior knowledge of these concepts. I am new to dependent type theory and would like to read a bit more about these concepts that are foreign to me. Could anyone suggest some good introductory resources explaining recursors and eliminators? Any help is greatly appreciated.

[Patrick Massot]

It is not meant to assume prio knowledge of these concepts.

[Patrick Massot]

You can still read Chapter 4 of https://browncs1951x.github.io/static/files/hitchhikersguide.pdf for more information.

[Kevin Cheung]

Patrick Massot said:

You can still read Chapter 4 of https://browncs1951x.github.io/static/files/hitchhikersguide.pdf for more information.

Thanks. I felt it expected prior knowledge because it starts talking about these things before explaining what they are.

[Kevin Buzzard]

If you make a new type T then it's pretty clear that to be able to use it, you need to be able to (a) make elements of T and (b) make functions which start at T and end up somewhere else. Constructors are the fundamental examples of (a) things, and eliminators or recursors (these are the same thing, I think?) are examples of (b) things.

[Kevin Buzzard]

If you make the type using the inductive keyword then probably you just wrote all the constructors down, and the recursor is generated automatically by Lean

[Kevin Buzzard]

inductive MyNat
| zero : MyNat
| succ : MyNat → MyNat

#check MyNat -- the type
#check MyNat.zero -- a constructor
#check MyNat.succ -- another one
#check MyNat.rec -- the eliminator/recursor

Those are the things which are automatically generated by the system when you make a new inductive type.

[Kevin Cheung]

It's starting to make more sense. Thank you!

[Flo (Florent Schaffhauser)]

Kevin Buzzard said:

inductive MyNat
| zero : MyNat
| succ : MyNat → MyNat

#check MyNat -- the type
#check MyNat.zero -- a constructor
#check MyNat.succ -- another one
#check MyNat.rec -- the eliminator/recursor

Those are the things which are automatically generated by the system when you make a new inductive type.

Also useful, perhaps:

#check @MyNat.succ

(the same constructor as MyNat.succ, presented differently)