Zulip Chat Archive

Stream: new members

Topic: How does eq.refl work?

Golol (May 11 2020 at 10:20):

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 (May 11 2020 at 10:30):


Kevin Buzzard (May 11 2020 at 10:31):

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

Kevin Buzzard (May 11 2020 at 10:32):

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

Kevin Buzzard (May 11 2020 at 10:33):

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 (May 11 2020 at 10:34):

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 (May 11 2020 at 10:57):

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 (May 11 2020 at 10:58):

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 (May 11 2020 at 11:00):

(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 (May 11 2020 at 11:44):

Okay, thank you!

Last updated: Dec 20 2023 at 11:08 UTC