Understanding the eliminator for equality

Stream: new members

[Vivek Rajesh Joshi]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

Yes, basically

[Siddhartha Gadgil]

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]

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

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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]

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.