trying to understand inductive types (Xena blog)

Stream: new members

[rzeta0]

I've returned to untangling my thinking around inductive types, and am re-reading the previously recommended Xena blog post on the subject: https://xenaproject.wordpress.com/2021/04/03/induction-and-inductive-types/

I won't ask all my questions right now, I'll do that step-by-step as this thread progresses.

---

The following code declares X as a type, and in fact an inductive type. It also establishes a single element of that type, p.

import Mathlib.Tactic

inductive X : Type
  | p : X

I'm new to this so I did a #check X which returns X : Type as expected. All good so far.

Now, the blog suggests that all inductive types automatically come with the machinery of induction.

So I tried `#check X.rec which gave me the following:

X.rec.{u} {motive : X → Sort u} (p : motive p) (t : X) : motive t

Question 1: How I interpret this? Sadly the blog was too advanced for me. What is motive ?

Let me try anyway. I expect Lean to create an "iterator" for elements of X, allowing me to select all elements of X, albeit using a recursive method rather than an actual (possibly) infinite enumeration. I'm thinking of the constructor of the definition of inductive Nat.

This is different from what the blog has, notice there is no motive:

X.rec : ∀ {C : X → Sort u}, C p → (∀ (x : X), C x)

Question 2: Why is the output different in the blog?

I did try #check @X.rec but I don't know what @ really does. Here's the different output:

@X.rec : {motive : X → Sort u_1} → motive p → (t : X) → motive t

Question 3: What is @ and why is the output different?

---

As further experimentation with Nat, because it is more familiar, I tried #check Nat.rec:

Nat.rec.{u} {motive : ℕ → Sort u} (zero : motive Nat.zero) (succ : (n : ℕ) → motive n → motive n.succ) (t : ℕ) :
  motive t

I'm still struggling to interpret this, despite having the advantage of knowing how induction on natural numbers is supposed to work.

[Kevin Buzzard]

Q1: motive is the same as C and this is probably just a Lean 3 / Lean 4 issue. X.rec says "if you have a family of types C_x (or motive(x)) parametrised by x in X, and you have an element of C_p (which unfortunately for you is also called p) then for any t in T you can get an element of C_t

Q2: probably a Lean 3 v Lean 4 issue?

Q3 @ just means "don't attempt to fill in any implicit arguments, tell me all the inputs, even the ones I'm supposed to be guessing"

[Kevin Buzzard]

Nat.rec says "given a family motive(n) of types or theorem statements, i.e. motive(0), motive(1), motive(2), ..., given an element of motive(0), and a way to get an element of motive(n+1) from motive(n), then for any t we can get an element of motive(t)"

[Kevin Buzzard]

This covers both recursion and induction. For induction motive(n) is a theorem statement about n (e.g. "sum of i from 0 to n-1 is n(n-1)/2"), and then the element of motive(0) is a proof of motive(0) and the way to get an element of motive(n+1) from an element of motive(n) is just a proof that motive(n) implies motive(n+1).

[rzeta0]

Thanks Kevin - your reply filled in some gaps in my knowledge. I will go back and re-read the blog with this added information.

I've set myself a goal to understand this machinery of induction/recursion even if it is outside my comfort zone.

(The other goal I've set myself is to get at least a surface understanding of what dependent type theory is, and I'm going to read your blog https://www.ma.imperial.ac.uk/~buzzard/lean_together/source/appendix/type_theory.html and the TPIL chapter again )