Beginner question: Mathematics in Lean, Release 0.1 p11

Stream: new members

[Peter Dolland]

My solution to

import Mathlib.Algebra.Ring.Basic
theorem add_neg_cancel_right (a b : R) : a + b + -b = a := by
    rw [← add_assoc, add_right_neg, add_zero]

was not accepted:
tactic 'rewrite' failed, did not find instance of the pattern in the target expression\n ?a + (?b + ?c)\nR✝ : Type u_1\ninst✝² : Ring R✝\nR' : Type u_2\ninst✝¹ : CommRing R'\na✝ b✝ c d : R'\nR : Type u_3\ninst✝ : Ring R\na b : R\n⊢ a + b + -b = a
I do not understand what is wrong.

[Riccardo Brasca]

Can you please use #backticks?

[Notification Bot]

This topic was moved here from #mathlib4 > Beginner question: Mathematics in Lean, Release 0.1 p11 by Riccardo Brasca.

[Riccardo Brasca]

And also it's better to provide a #mwe

[Riccardo Brasca]

(here the error is clear, ← add_assoc transforms a + (b + c) into a + b + c (that by definition means (a + b) + c). Lean is complaining that there is no a + (b + c) in your expression)

[Peter Dolland]

Riccardo Brasca schrieb:

(here the error is clear, ← add_assoc transforms a + (b + c) into a + b + c (that by definition means (a + b) + c). Lean is complaining that there is no a + (b + c) in your expression)

How can I see, that ← add_assoc transforms a + (b + c) into a + b + c and does not vice versa? How I could find a proposition I could use for vice versa? In my mind equality is a symmetric relation.

[Kevin Buzzard]

Equality _is_ a symmetric relation, but here we are manipulating terms in a type theory, and "change X to Y" is definitely different to "change Y to X". The numbers 2 + 2 and 4 are equal, but the terms 2 + 2 and 4 are distinct.

add_assoc is a proof of (a + b) + c = a + (b + c), so rw [add_assoc] will change the LHS into the RHS and rw [← add_assoc] will turn the RHS into the LHS.

Did you play the natural number game?

[Peter Dolland]

Kevin Buzzard schrieb:

Equality _is_ a symmetric relation, but here we are manipulating terms in a type theory, and "change X to Y" is definitely different to "change Y to X". The numbers 2 + 2 and 4 are equal, but the terms 2 + 2 and 4 are distinct.

add_assoc is a proof of (a + b) + c = a + (b + c), so rw [add_assoc] will change the LHS into the RHS and rw [← add_assoc] will turn the RHS into the LHS.

Did you play the natural number game?

Okay, thank you. I did not understand the ←. What the natural number game?

[Riccardo Brasca]

It is this game. It shows you the very basics of Lean, and a lot of people started there.

[Patrick Massot]

Playing the natural number game is absolutely not a prerequisite of MIL. All this is explained in MIL.

[Patrick Massot]

You need to read again the paragraph that said

Try proving these identities, in each case replacing sorry by a tactic proof. With the rw tactic, you can use a left arrow (\l) to reverse an identity. For example, rw [← mul_assoc a b c] replaces a * (b * c) by a * b * c in the current goal. Note that the left-pointing arrow refers to going from right to left in the identity provided by mul_assoc, it has nothing to do with the left or right side of the goal.

[Peter Dolland]

Patrick Massot schrieb:

You need to read again the paragraph that said
```quote
Try proving these identities, in each case replacing sorry by a tactic proof. With the rw tactic, you can use a left arrow (\l) to reverse an identity. For example, rw [← mul_assoc a b c] replaces a * (b * c) by a * b * c in the current goal. Note that the left-pointing arrow refers to going from right to left in the identity provided by mul_assoc, it has nothing to do with the left or right side of the goal.
```

Okay, here it was explained, what means to "reverse an identity"(?) with the help of an example. My question is, if there is a location, where this is explained in a more systematic way?

[Luigi Massacci]

By default, rw rewrites the equalities you provide left to right. (it tries to match the left-hand side of what you gave to something in the goal, and then replaces the right hand side). If you want to rewrite right to left, that is “reversing an identity”, and the arrow does just that . There just isn’t much to explain

[Peter Dolland]

With "systematic way" I mean the options I have to use rw. E.g. I want to apply the reverse group rule one_mul to the first a in a * a⁻¹. How to teach Lean?