Zulip Chat Archive

Stream: new members

Topic: proof of neg_neg in Mathematics in Lean


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 26 2020 at 22:41):

note the somewhat weird state before the exact

view this post on Zulip 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

view this post on Zulip 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