Zulip Chat Archive

Stream: new members

Topic: Newbie question


view this post on Zulip Jakob Scholbach (Jan 26 2021 at 20:12):

I am really new to lean, and working through §2 here https://leanprover-community.github.io/mathematics_in_lean/basics.html
I am stuck with this one:

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b :=
sorry

Of course I would like to say: starting from hypothesis h, add -a on the left and use this lemma sub_self mentioned above in the chapter. What is the syntax to achieve this? Thanks!

view this post on Zulip Johan Commelin (Jan 26 2021 at 20:13):

Hey @Jakob Scholbach nice to see you here!

view this post on Zulip Johan Commelin (Jan 26 2021 at 20:13):

Small tip: you can use #backticks to format your code on Zulip

view this post on Zulip Johan Commelin (Jan 26 2021 at 20:16):

You can go two ways. You can work on the hypothesis h. Or you can work "backward" on the goal.
There is a lemma add_left_cancel that could help with backwards reasoning.

view this post on Zulip Johan Commelin (Jan 26 2021 at 20:18):

For a forward step, you could do something like

example {R : Type} [comm_ring R] {a b : R} (h : a + b = 0) : -a = b :=
begin
  have h2 : -a + (a + b) = -a + 0,
  { rw h },
end

view this post on Zulip Johan Commelin (Jan 26 2021 at 20:18):

There are ways of doing this in 1 step. But that's maybe not very enlightening right now.

view this post on Zulip Jakob Scholbach (Jan 26 2021 at 20:21):

Ok, thanks!

view this post on Zulip Alex J. Best (Jan 26 2021 at 20:21):

For working backwards from the goal, you can do something like,

import algebra.ring

namespace my_ring

variables {R : Type*} [ring R]

-- BEGIN
theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b :=
begin
rw  add_zero (-a),
rw  h,
rw neg_add_cancel_left,
end
end my_ring

view this post on Zulip Patrick Massot (Jan 26 2021 at 20:26):

Beware the exercise asks to do it only with the lemmas discussed before. So we need to know the list of allowed lemmas (that I don't remember).

view this post on Zulip Alex J. Best (Jan 26 2021 at 20:39):

good point, I updated what I wrote to only use lemmas in the tutorial, it got way shorter too :grinning:


Last updated: May 07 2021 at 00:30 UTC