proof of neg_neg in Mathematics in Lean

Stream: new members

[Mike]

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]

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]

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]

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]

@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]

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]

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]

note the somewhat weird state before the exact

[Mario Carneiro]

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]

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