Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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