# 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):

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

#### 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