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