Stream: new members
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):
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=4, it's definitional.
Last updated: May 14 2021 at 04:22 UTC