# Zulip Chat Archive

## Stream: new members

### Topic: Understanding the eliminator for equality

#### Vivek Rajesh Joshi (Dec 13 2023 at 12:44):

I recently started learning inductive types from TPIL, and I'm starting to get a hang of the "constructors" part. The "eliminators" part is a bit harder to grasp for me, but I have understood it for Nat and Lists. The eliminator for equality is proving to be a hassle:

```
universe u v
#check (@Eq.rec : {α : Sort u} → {a : α} → {motive : (x : α) → a = x → Sort v}
→ motive a rfl → {b : α} → (h : a = b) → motive b h)
```

This hasn't been elaborated in TPIL. Can someone explain to me how this works, and how it is supposed to build a function with domain a = b?

#### Joachim Breitner (Dec 13 2023 at 12:55):

To answer your immediate question: Notice that the last parameter to `Eq.rec`

is of type `(h : a = b) → …`

, so if you use `@Eq.rec α a motive p b`

, then this has type `a = b → …`

, so it is a function with domain `a = b`

.

#### Joachim Breitner (Dec 13 2023 at 12:56):

But even then the eliminator for equality is still a hassle :-). It may help to walk through using it for a concrete function, maybe `a = b → b = a`

. In that case, what is your `motive`

? And what role does the forth argument to `Eq.rec`

, the type of `motive a rfl`

, then play.

#### Riccardo Brasca (Dec 13 2023 at 13:02):

It is probably the most difficult eliminator to understand. I usually try to explain it as follows: instead of saying `a = b`

I will say "`a`

and `b`

are friends" (since `=`

is so deeply rooted in our brain that it is difficult to have a good intuition).

Start with a type `α`

and a term `(a : α)`

. Suppose you want to do "something" for all `b`

(of type `α`

) that are friends with `a`

. This "something" can be proving a proposition (so proving that all friends of `a`

have some property) or construct a natural number or whatever, depending on the friend. Then it is enough to do this something for `a`

.

Note two things:

- often (but not always!) this "something" is defined for all
`(b : α)`

, but it is enough that is is well defined for the friends of`a`

. - On the other hand, it
*has to be defined*. Contrary to other eliminators, this is usually the tricky part, you have to specify what you want to do in general before saying "it is enough to do it for`a`

.

#### Kevin Buzzard (Dec 13 2023 at 13:03):

I wrote a blog post here about the recursor for equality -- all Lean 3 but probably this doesn't matter for your question.

#### Riccardo Brasca (Dec 13 2023 at 13:10):

Concerning my last point, a very good exercise is to understand why "the uniqueness of `refl`

" is a serious problem in type theory. The question is the following: suppose that `(a b : α)`

and that `(h₁ : a = b)`

and `(h₂ : a = b)`

. Does it follow that `h₁ = h₂`

?

Of course in Lean the answer is yes (because of proof irrelevance, `h₁`

and `h₂`

are proofs of the same proposition so they're definitionally equal), but it is interesting to try to prove it *without* using proof irrelevance. `Eq.rec`

allows you to reduce the problem to prove that if `(h : a = a)`

then `h = Eq.refl a`

, but then you're stuck, and the problem is exactly that you don't find a good motive to use again `Eq.rec`

.

#### Vivek Rajesh Joshi (Dec 14 2023 at 06:58):

Thanks @Joachim Breitner , @Riccardo Brasca . I think I understood what Eq.rec says.

Correct me if I'm wrong, but it says "Suppose you have a type `\a`

and an element `a : \a`

, suppose you have a function that can map all `b : \a`

that are equal to `\a`

to something (say, of Type k), and suppose you can map `a`

to something (same/different thing) of Type k. Then you can construct a function that can take a proposition of some element in `\a`

being equal to `a`

, and map it to something of Type k. (For clarity, Sort v has been reduced to k)"

Noe that I have written it down, I realise that it is almost the same thing that @Riccardo Brasca has said, and @Kevin Buzzard has written in his blog post.

However, what I still struggle to understand, is how this sort of a statement guarantees that `refl`

is the only element in `Eq a a`

. I know that this follows from a statement in @Kevin Buzzard 's blog post:

"“Let’s say that for every element x of X we have a set C(x), and let’s say we have an element of C(p). Then we have a method of constructing an element of C(x) for all x \in X.” This looks like a rather long-winded way of saying that p is the only element of X. "

But I cannot grasp how the 2nd sentence here follows from the first one either.

#### Arthur Adjedj (Dec 14 2023 at 07:19):

However, what I still struggle to understand, is how this sort of a statement guarantees that refl is the only element in Eq a a

It isn't the case, in many other type theories, that this eliminator implies the uniqueness of identity proof (the fact that all proofs of `Eq a a`

are equal to `refl`

). In univalent type theories such as CubicalTT, it is in fact explicitly not the case. In Lean, this property is true because `Eq`

lives in the `Prop`

universe, which is proof-irrelevant (read, any two proofs of a given proposition are equal).

#### Vivek Rajesh Joshi (Dec 14 2023 at 07:22):

I see, thanks a lot. Regardless, how do the eliminators for other types imply that the only elements residing in that type are the constructors?

#### Kevin Buzzard (Dec 14 2023 at 07:25):

The elimination rule says "if it's true for all terms made using constructors then it's true for all terms" and you can prove that all terms of the type are made from one of the constructors very easily from this.

#### Arthur Adjedj (Dec 14 2023 at 07:47):

You may learn this by example. Take the type of booleans `Bool`

, made of two constructors. It's eliminator, `Bool.rec`

, has type:

```
Bool.rec.{u} {motive : Bool → Sort u} (false : motive false) (true : motive true) (t : Bool) : motive t
```

if we take `fun _ => Prop`

as a motive, we may use the recursor to map `true`

to the `True`

type, and `false`

to `False`

. In order to prove that `true != false`

, you now only need to prove that `True != False`

. Furthermore, if `True = False`

, then you can inhabit `False`

by transporting `True.intro`

through your equality. That's how you generally prove that two constructors are different.

#### Vivek Rajesh Joshi (Dec 14 2023 at 08:35):

Kevin Buzzard said:

The elimination rule says "if it's true for all terms made using constructors then it's true for all terms" and you can prove that all terms of the type are made from one of the constructors very easily from this.

Is the proof basically to take the special case of the "true thing" being "this term can be made using constructors"? Sorry if this is a very trivial doubt, I haven't learnt anything like type theory before and my experience with Lean is relatively short, around 5 months.

#### Ruben Van de Velde (Dec 14 2023 at 08:37):

Yes, basically

#### Siddhartha Gadgil (Dec 14 2023 at 08:39):

As an example:

```
theorem nat_from_constructors (n: Nat) :
n = Nat.zero ∨ ∃ m, n = Nat.succ m := by
cases n with
| zero => left; rfl
| succ m => right; use m
```

#### Riccardo Brasca (Dec 14 2023 at 10:51):

Can you please open a new thread and write a #mwe?

#### Riccardo Brasca (Dec 14 2023 at 10:53):

Concerning again the equality I have somewhere an exercice sheet with several examples. @Vivek Rajesh Joshi if you want I can share it.

#### Vivek Rajesh Joshi (Dec 14 2023 at 10:54):

Sure, you can share it to me. Thanks a lot!

#### Riccardo Brasca (Dec 14 2023 at 10:59):

```
open Nat
namespace ex
universe u v
section equality
inductive Eq {A : Sort u} : A → A → Prop
| refl (a : A) : Eq a a
open Eq
infix:50 " ≃ " => Eq
section eliminator
#check @Eq.rec
variable (A : Sort u) (a b : A) (h : a ≃ b)
#check @Eq.rec A a
variable (P : A → Prop) (ha : P a)
#check @Eq.rec A a (fun b _ ↦ P b)
#check @Eq.rec A a (fun b _ ↦ P b) ha b h
end eliminator
section equivalence
variable (A : Sort u)
theorem reflexivity (a : A) : a ≃ a := by
exact refl a
theorem symmetry (a b : A) (h : a ≃ b) : b ≃ a := by
let P : A → _ := fun x ↦ x ≃ a
exact Eq.rec (motive := fun x _ ↦ P x) (reflexivity A a) h
theorem transitivity (a b c : A) (hab : a ≃ b) (hbc : b ≃ c) : a ≃ c := by
let P : A → _ := fun x ↦ a ≃ x
exact Eq.rec (motive := fun x _ ↦ P x) hab hbc
end equivalence
variable (A : Sort u)
theorem substitution (B : Type v) (f : A → B) (a b : A) (h : a ≃ b) :
f a ≃ f b := by
let P : A → _ := fun x ↦ f a ≃ f x
exact Eq.rec (motive := fun x _ ↦ P x) (reflexivity B (f a)) h
example (R : A → A → Prop) (hrefl : ∀ a, R a a) (a b : A) (h : a ≃ b) : R a b := by
let P : A → Prop := fun x ↦ R a x
exact Eq.rec (motive := fun x _ ↦ P x) (hrefl a) h
noncomputable
example : ∀ (x : Nat), x ≃ x + 0 := by
apply Nat.rec
· exact Eq.refl _
· intro d h
have : succ (d + 0) ≃ succ d + 0 := Eq.refl _
refine transitivity _ _ _ _ ?_ this
apply substitution
exact h
noncomputable
example : ∀ (x : Nat), x ≃ x + 0 := by
apply Nat.rec
· exact Eq.refl 0
· intro d h
have : succ d + 0 ≃ succ (d + 0) := Eq.refl _
refine Eq.rec (motive := fun n _ ↦ succ d ≃ n) ?_ this
exact Eq.rec (motive := fun n _ ↦ succ d ≃ succ n) (Eq.refl _) h
example (a b : A) (h h' : a ≃ b) : h ≃ h' := by
exact Eq.refl _
noncomputable
example (a b : A) (h h' : a ≃ b) : h ≃ h' := by
let M := fun (x : A) (e : a ≃ x) ↦ ∀ (e' : a ≃ x), e ≃ e'
apply Eq.rec (motive := M)
intro e'
sorry
end equality
end ex
```

I redefine equality and I prove basic properties (that is an equivalence relation + substitution).

Something interesting you can do is to modify the definition as follows

```
inductive Eq {A : Sort u} : A → A → Type
| refl (a : A) : Eq a a
```

so it takes values in `Type`

rather than in `Prop`

. Nothing breaks util the uniqueness of `refl`

. Of course the proof in line 79 does not work anymore, but the example in line 82 still works. The difference is that before it was easy to finish the proof, and now it's not.

#### Igor Khavkine (Dec 14 2023 at 11:01):

Riccardo Brasca said:

Can you please open a new thread and write a #mwe?

Sorry, I may have posted here by accident. This was my first message. I'm not sure how to ask a new question.

Last updated: Dec 20 2023 at 11:08 UTC