# Zulip Chat Archive

## Stream: new members

### Topic: When exactly does Lean accept `rfl` as a proof?

#### Chris M (Aug 02 2020 at 12:48):

I've not yet been able to see the pattern that predicts whether Lean will accept `rfl`

as a proof. I would like to understand which reductions Lean does and doesn't do before concluding that two sides of an equation are the same.

What exactly is the rule that Lean applies to check whether `rfl`

is a correct proof? Basically, `rfl`

is a proof of `a=a`

, and I think that Lean accepts `rfl`

as a proof for a given equality, if those objects are "definitionally the same", but I'm not exactly sure what that means concretely.

#### Chris M (Aug 02 2020 at 13:11):

e.g., in the following example, Lean accepts `rfl`

as a proof for the case that `n=0`

, which would require a substitution to be correct. However, for the case that `n=4`

for example, we could in principle also deduce that the two sides are the same, simply by first reducing the terms on both sides of the equation, but Lean doesn't do this type of reduction.

```
def add (n m :ℕ) : ℕ := nat.rec_on n m (λx xplusm, nat.succ xplusm)
example (n m : ℕ) : add n (nat.succ m) = add (nat.succ n) m :=
nat.rec_on n rfl sorry
example (n m : ℕ) : add n (nat.succ m) = add (nat.succ n) m :=
rfl
```

i.e. in the first example, `rfl`

is accepted but in the second it isn't. (I'm not saying it should be accepted in the second. If the line isn't drawn somewhere, this would basically amount to quite general automated prover. I'm just stating that I don't know where the line is.)

#### Reid Barton (Aug 02 2020 at 13:35):

See section 2 of https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf

#### Kevin Buzzard (Aug 02 2020 at 14:39):

Or section 3.7 of the Lean reference manual https://leanprover.github.io/reference/expressions.html#computation

#### Kevin Buzzard (Aug 02 2020 at 14:41):

`add n (succ m)`

is defeq to `succ (add n m)`

, but to prove it's equal to `add (succ n) m`

you need to prove it by induction, i.e. you need to apply the recursor, so it's not definitional.

#### Kevin Buzzard (Aug 02 2020 at 14:43):

You're right that when you start putting numbers in, more things become definitionally equal. For example `0 + n = n`

needs to be proved by induction, but for any fixed numeral `n`

e.g. `n=4`

, it's definitional.

Last updated: May 14 2021 at 04:22 UTC