When exactly does Lean accept `rfl` as a proof?

Stream: new members

[Chris M]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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.