Proof of self_sub for Mathematics in Lean

Stream: new members

[Mike]

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,
    {rw ←eq_neg_of_add_eq_zero at h₁},
    have h₂ := sub_eq_add_neg h₂,
    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]

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,
    { rw ←eq_neg_of_add_eq_zero' at h₁,
      exact h₁ },
    rw ←sub_eq_add_neg' at h₂,
    exact h₂,
end

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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]

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

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

[Yakov Pechersky]

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.