## 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 h₁ at h₂,
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 ← h₂ at h₁,
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},

Thank you for explaining the difference between apply using backward reasoning and have using forward reasoning.