## Stream: new members

### Topic: Proof of self_sub for Mathematics in Lean

#### Mike (Aug 27 2020 at 15:39):

Hi,

I'm hoping someone can help me with my attempted proof of

theorem self_sub (a : R) : a - a = 0 :=


Here's what I have:

import algebra.ring
import tactic

variables {R : Type*} [ring R]

theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b :=
...

theorem sub_eq_add_neg (a b : R) : a - b = a + -b :=
by reflexivity

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

theorem self_sub (a : R) : a - a = 0 :=
begin
have h₁ : a = -(-a),
{rw neg_neg},
have h₂ : a + (-a) = 0,
exact h₂,
end


The justification of h₂ doesn't work:
/-
rewrite tactic failed, lemma lhs is a metavariable
state:
R : Type u_1,
_inst_1 : ring R,
a : R,
h₁ : a = - -a
⊢ a + -a = 0
-/
Could someone explain what caused this error and what it means please.
Thanks!

#### Yakov Pechersky (Aug 27 2020 at 15:47):

With minimal changes from what you have:

import algebra.ring
import tactic

variables {R : Type*} [ring R]

theorem eq_neg_of_add_eq_zero' {a b : R} : a + b = 0 ↔ a = -b := sorry

theorem sub_eq_add_neg' (a b : R) : a - b = a + -b :=
by reflexivity

theorem neg_neg' (a : R) : -(-a) = a := sorry

theorem self_sub (a : R) : a - a = 0 :=
begin
have h₁ : a = -(-a),
{ rw neg_neg' },
have h₂ : a + (-a) = 0,
exact h₁ },
exact h₂,
end


#### Yakov Pechersky (Aug 27 2020 at 15:48):

I named them all "prime" to avoid clashes with names in mathlib

#### Yakov Pechersky (Aug 27 2020 at 15:49):

I changed the first lemma to \iff format, so that it can be used for rewrites.

#### Yakov Pechersky (Aug 27 2020 at 15:50):

Before, having the hypothesis on the left as an explicit argument makes it not possible to use it as a rewrite how you wanted to, that was the metavariable issue.

#### Yakov Pechersky (Aug 27 2020 at 15:50):

Because how you had it originally, eq_neg_of_add_eq_zero needed an explicit argument. And that explicit argument was exactly what you were trying to prove in the goal.

#### Johan Commelin (Aug 27 2020 at 15:51):

@Mike In particular, what went wrong with your first attempt is that you tried to treat eq_neg_of_add_eq_zero as an iff statement, but it is only one direction of the iff that you are looking for. (And the wrong direction unfortunately.)

#### Yakov Pechersky (Aug 27 2020 at 15:51):

Additionally, I changed the have h2 := ... to rw ... at h2

#### Yakov Pechersky (Aug 27 2020 at 15:52):

Because you can't just apply an equality of the form a = b to a hypothesis of h2 := a to get h2 := b. That's exactly what the rewrite tactic does instead.

Last updated: May 13 2021 at 06:15 UTC