How does eq.refl work?

Stream: new members

[Golol]

I'm trying to understand how the following proof really works:

theorem my_theorem : ∀ (f : α → α) (a : α), (λ x, f x) a = f a :=
    assume (f : α → α) (a : α),
        eq.refl ((λ x, f x) a)

eq.refl basically returns a proof of the proposition

(λ x, f x) a = (λ x, f x) a

I suppose then the theorem gets proven by applying beta-reduction? Are the terms ((λ x, f x) a) and (f a) already considered equivalent anyways, and lean just looks for an equivalent way to write them so you get (λ x, f x) a = f a?
Doing this also works when two beta reductions are necessary, and even "in reverse"

theorem my_other_theorem : ∀ (f : α → α) (a : α), (λ x, f x) ((λ x, f x) a) = f (f a) :=
    assume (f : α → α) (a : α),
        eq.refl ( (λ x, f x) ((λ x, f x) a) )

theorem my_third_theorem : ∀ (f : α → α) (a : α), (λ x, f x) ((λ x, f x) a) = f (f a) :=
    assume (f : α → α) (a : α),
        eq.refl ( f (f a) )

This makes it feel like eq.refl is more of a tactic, but Id like to know what's really going on.

[Kevin Buzzard]

https://leanprover.github.io/reference/expressions.html#computation

[Kevin Buzzard]

Lean has a concept of definitional equality, and its formal definition is in the link. beta reduction is part of the story.

[Kevin Buzzard]

example (α : Type) : ∀ (f : α → α) (a : α), (λ x, f x) a = f a := λ f a, rfl

[Kevin Buzzard]

I once mentioned the fact that refl was a powerful tactic to Floris van Doorn, and he said he'd never thought of it that way. I think that any tactic that can prove 2 + 2 = 4 has something going for it.

[Chris Hughes]

If terms are definitionally equal then they can be used interchangeably in any proof. eq.refl isn't the only thing that uses definitional equality, for example this proof works because the type of h is defeq to the goal.

example (x : ℕ) (h : (λ y : ℕ, 0 < y) x) : 0 < x := h

[Kevin Buzzard]

Definitional equality is a highly non-mathematical concept. For example, in Lean, if n is a natural number then n+0=n is definitionally true, and 0+n=n is not. In Coq it might be the other way around.

[Kevin Buzzard]

In the natural number game I encourage mathematicians to use add_zero and zero_add to prove these two theorems, and do not really ever indicate the fact that one, but not the other, can be proved with rfl. For me, this is a coincidence.

[Kevin Buzzard]

(by the way, if you write #check rfl and then right click on it and go to definition, you'll see that it's just an abbreviation for eq.refl)

[Golol]

Okay, thank you!