Trying to understand recursors

Stream: new members

[Matthias Geier]

A few weeks ago I've asked a question here (#new members > How to reason about the proof for Eq.symm? ), where I learned about "inaccessible patterns". Today I have a few follow-up questions ...

Last time, I learned that when I write this:

example {a b : Nat} (h : a = b) : b = a :=
  match h with
  | Eq.refl _ => Eq.refl _

... Lean turns it into something like this (using the inaccessible pattern .(a)):

example {a b : Nat} (h : a = b) : b = a :=
  match b, h with
  | .(a), Eq.refl a => Eq.refl a

I tried to understand this by finding a more fundamental proof term that doesn't need pattern matching, and this is what I came up with:

example {a b : Nat} (h : a = b) : b = a :=
  Eq.rec (Eq.refl a) h

I guess the motive is relevant, this seems to be what Lean uses implicitly in this case:

example {a b : Nat} (h : a = b) : b = a :=
  Eq.rec (motive := fun x _ => x = a) (Eq.refl a) h

Now my questions:

Is this equivalent to the inaccessible pattern in the match expression?

And if yes, how?

How can I get some intuition about what the recursor Eq.rec actually does?

How can I get Lean to show me the implementation of Eq.rec?
I tried #print Eq.rec, but that only shows the function signature.

How is the motive chosen when I don't specify it?

Any additional hints that might help me understanding would be appreciated! Please note that I'm not a mathematician nor a functional programmer, so I have about zero knowledge about recursors and how they work.

[Henrik Böving]

Is this equivalent to the inaccessible pattern in the match expression?

You can check this by inspecting the pattern match:

theorem test {a b : Nat} (h : a = b) : b = a :=
  match b, h with
  | .(a), Eq.refl a => Eq.refl a

#print test
#print test.match_1_1

as you can see the term that Lean generates is a bit crazier but that is because the mechanism here is able to handle a couple of other situations. Its indeed very similar to recursor applications in the end.

How can I get Lean to show me the implementation of Eq.rec?

You can't, they are axiomatized symbols with axiomatized rules, they have no implementation.

How can I get some intuition about what the recursor Eq.rec actually does?

I would say to a first approximation you can think of it as "rewriting with the equation in the target term". If you want to know the precise theoretical underpinnings of recursors and what their automatically derived rules are consider #leantt

How is the motive chosen when I don't specify it?

There is a dedicated mechanism in Lean's elaborator specifically for figuring out motives automatically. I unfortunately don't know the details but it is indeed a non trivial process.

[Matthias Geier]

You can check this by inspecting the pattern match

Yes, thanks, I actually did that, but it was indeed crazy. It has like 3 nested applications of Eq.rec in it, and some HEq in addition to Eq. I was glad that I found a shorter proof term. But I'm not sure if "shorter" means "better intuition".

If you know a different proof term that is easier to understand, please let me know!

I would say to a first approximation you can think of it as "rewriting with the equation in the target term".

I know most of those words, but I have no clue what you are talking about. Could you please elaborate? Rewriting what? What equation? What is the "target term"?

If you want to know the precise theoretical underpinnings of recursors and what their automatically derived rules are consider #leantt

I'll have a look, but it might be a bit too heavy for my knowledge level.

[Henrik Böving]

Eq.rec (motive := fun x _ => x = a) (Eq.refl a) h

this rewrites with h in (Eq.refl a)

[Matthias Geier]

OK, thanks! So you mean something like: it rewrites the first a in a = a with a = b, which results in b = a? But on the level of terms, not types, I guess. If it would rewrite Eq.refl a, this would lead to Eq.refl b, which is of type b = b, which wouldn't really help me ... I'm very likely misunderstanding ...

[Robin Arnez]

Well, in general, recursors are induction principles. Take this inductively defined predicate:

inductive Something : (n : Nat) → Prop where
  | one : Something 1
  | two : Something 2
  | three : Something 3
  | mul_two (x : Something n) : Something (n * 2)

with the recursor

recursor Something.rec
  {motive : (n : Nat) → Something n → Prop}
  (one : motive 1 Something.one)
  (two : motive 2 Something.two)
  (three : motive 3 Something.three)
  (mul_two : ∀ {n : Nat} (x : Something n), motive n x → motive (n * 2) (Something.mul_two x))
  {n : Nat} (t : Something n) : motive n t

What it says is that for any predicate motive of natural numbers (that maybe also use the proof of Something n), if you can prove that it's true for 1, 2 and 3 and it being true for n implies it being true for n * 2 then it is true for all natural numbers n where Something n is true (in other words, it states that Something is the smallest predicate that is true for 1, 2 and 3 and is closed under multiplication by two).
The equality recursor Eq.rec is no different. Remember, Eq is defined as

inductive Eq {α : Sort u} (a : α) : (b : α) → Prop where
  | refl : Eq a a

in other words, given a type α and a value a : α, Eq a is the smallest predicate that is true for a. In recursor form:

recursor Eq.rec {α : Sort u} {a : α}
  {motive : (b : α) → Eq a b → Sort u_1}
  (refl : motive a (Eq.refl a))
  {b : α} (t : Eq a b) : motive b t

Read: when you have a predicate motive of values in α (that potentially depends on the proof that Eq a b), and it is true for a, then it is true for all b where Eq a b is true. The fact that Eq.rec "rewrites" types here can be thought of as a side effect that comes from the fact that if you give it a proof of something with a + a proof that a = b and it gives you a proof of something with b.