# Zulip Chat Archive

## Stream: new members

### Topic: proof of neg_neg in Mathematics in Lean

#### Mike (Aug 26 2020 at 22:25):

Hi,

I'm trying to read through *Mathematics in Lean* and got stuck trying to prove

```
theorem neg_neg (a : R) : -(-a) = a :=
```

Here's what I attempted:

```
import algebra.ring
import tactic
variables {R : Type*} [ring R]
theorem neg_neg (a : R) : -(-a) = a :=
begin
have h₁ : -a + -(-a) = 0,
{apply sub_self},
have h₂ : a + -a = 0,
{apply sub_self},
rw add_comm at h₁,
rw h₁ at h₂,
apply add_right_cancel,
end
```

I thought that since h₁ and h₂ are both equations that are equal to zero, that I could (after commuting the addition in h₁ get the equation:

```
-(-a) + -a = a + -a
```

and then use `add_right_cancel`

to get `-(-a) = a`

.

I'd appreciate it if someone could let me know whether this a valid approach to proving this theorem. If it is, could you help me see what I'm doing wrong.

Thanks!

#### Mario Carneiro (Aug 26 2020 at 22:35):

Assuming that h2 says `-(-a) + -a = a + -a`

, to get from that to `-(-a) = a`

using `add_right_cancel`

is a forward reasoning step, so you should use `have`

instead of `apply`

#### Mario Carneiro (Aug 26 2020 at 22:36):

If you work backward from the goal using `apply add_right_cancel`

you will get the goal `-(-a) + ?m_1 = a + ?m_1`

, which is usable (you can finish with `exact h2`

) but a little confusing to work with

#### Mario Carneiro (Aug 26 2020 at 22:37):

because from this line alone it's not clear what you are cancelling (you are basically un-cancelling when you work backwards using this theorem)

#### Mario Carneiro (Aug 26 2020 at 22:38):

@Bryan Gin-ge Chen @Gabriel Ebner FYI the goal state here prints `--a`

. Should the pretty printer be taught that this is a bad idea?

#### Mario Carneiro (Aug 26 2020 at 22:40):

actually correction, the goal view correctly prints `- -a`

but the widget view prints `--a`

, so I guess I should ping @Edward Ayers instead

#### Mario Carneiro (Aug 26 2020 at 22:41):

Here's a corrected version of the proof using `apply`

:

```
theorem neg_neg' (a : R) : -(-a) = a :=
begin
have h₁ : -a + - -a = 0,
{apply sub_self},
have h₂ : a + -a = 0,
{apply sub_self},
rw add_comm at h₁,
rw ← h₂ at h₁,
apply add_right_cancel,
exact h₁
end
```

#### Mario Carneiro (Aug 26 2020 at 22:41):

note the somewhat weird state before the `exact`

#### Mario Carneiro (Aug 26 2020 at 22:42):

and here's a version using a forward reasoning step instead:

```
theorem neg_neg' (a : R) : -(-a) = a :=
begin
have h₁ : -a + - -a = 0,
{apply sub_self},
have h₂ : a + -a = 0,
{apply sub_self},
rw add_comm at h₁,
rw ← h₂ at h₁,
have h₁ := add_right_cancel h₁,
exact h₁
end
```

#### Mike (Aug 27 2020 at 13:38):

Thank you for explaining the difference between `apply`

using backward reasoning and `have`

using forward reasoning.

Last updated: May 14 2021 at 03:27 UTC