Trouble with `(eq.rec_on (eq.refl α) a : α) = a'`

Stream: new members

[garySebastian]

I'd appreciate it if someone could break down this bit from eq_of_heq in core a little bit; in the context, (α : Sort u) (a : α). I understand the idea being conveyed, but I'm not sure how (eq.rec_on (eq.refl α) a : α) can be of type α. I think my main confusion is what constitutes the (C : α -> Sort l) part in this use eq.rec_on. The whole thing for context is :

lemma eq_of_heq {α : Sort u} {a a' : α} (h : a == a') : a = a' :=
have ∀ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from
  λ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl),
show (eq.rec_on (eq.refl α) a : α) = a', from
this α a' h (eq.refl α)

[Mario Carneiro]

eq.rec_on (eq.refl α) a is defeq to a by the reduction rule for inductive types

[Mario Carneiro]

If you use

set_option pp.implicit true
#print eq_of_heq

to view the implicit stuff, you will see that the motive in this case is just (λ (_x : Sort u), _x)

[Mario Carneiro]

In other words, it is using the fact that α = α to transfer a : α to α. Because the proof is reflexivity (and it always is because of proof irrelevance), this is just an identity cast and the result is defeq to a.

[garySebastian]

it is using the fact that α = α to transfer a : α to α.

Sorry I'm really struggling with this one. Isn't a already of type α, or is the point that you can use that for (α = α') to transfer a : α to a : α'? This might be part of my problem, but the variable names are going over my head. If the signature of eq.rec_on is :

eq.rec_on : Π {β : Sort u} {b : β} {C : β → Sort l} {b_1 : β}, b = b_1 → C b → C b_1

then in line two, (eq.rec_on (h2 : α = α') a : α') = a', is b |-> α or b |-> a?

I think I understand the idea that the inferred family { C : α -> Sort l } is id in this case, since the type checker seems to be okay with show a = a' instead of show (eq.rec_on (eq.refl α) a : α) = a' in line 4.

[Kevin Buzzard]

(eq.rec_on (h2 : α = α') a : α') means "make the term eq.rec_on (h2 : α = α') a and make sure it has type α' while you're at it". This sort of information ("what type is this thing supposed to have?") is helpful for Lean's elaborator because eq.rec_on has got all these inputs in { } brackets, which Lean is supposed to guess.

[Kevin Buzzard]

So now Lean looks at eq.rec_on and says "OK, the { } stuff I'll have to deal with later, so I don't know beta or b or C or b_1, but I know that the next input is supposed to have type b = b_1 and it actually has type α = α' so I'd best set b = α and b_1 = α'"

[Kevin Buzzard]

Oh, perhaps this is the trick you're missing: if a has type alpha and then I explicitly refer to a whilst assuring Lean it has type beta by writing (a : beta) then Lean will accept this, as long as it can convince itself that alpha = beta by definition.

[Kevin Buzzard]

example (α β : Type) (h : α = β) (a : α) : β := (a : β) -- fails

def fakebool := bool -- true by definition

example (a : fakebool) : bool := (a : bool) -- works

[Kevin Buzzard]

Here's the same proof in tactic mode (which I find far easier to use)

universe u

lemma eq_of_heq' {α : Sort u} {a a' : α} (h : a == a') : a = a' :=
begin
  -- intermediate lemma, called `this` in original.
  have H : ∀ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'),
             (eq.rec_on h₂ a : α') = a',
    -- proof of intermediate lemma.
    exact λ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a'),
          heq.rec_on h₁ (λ h₂ : α = α, rfl),
  -- back to one goal now.
  -- now change the goal to something definitionally equal
  show (eq.rec_on (eq.refl α) a : α) = a',
  -- now prove it using H
  exact H α a' h (eq.refl α)
end

[garySebastian]

I feel much more comfortable reading this after spending a few evenings with it. Thanks a lot for pointing me in the right direction @Kevin Buzzard and @Mario Carneiro.