Zulip Chat Archive

Stream: new members

Topic: Proof of self_sub for Mathematics in Lean


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

view this post on Zulip 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,
    { rw eq_neg_of_add_eq_zero' at h₁,
      exact h₁ },
    rw sub_eq_add_neg' at h₂,
    exact h₂,
end

view this post on Zulip Yakov Pechersky (Aug 27 2020 at 15:48):

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

view this post on Zulip Yakov Pechersky (Aug 27 2020 at 15:49):

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

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

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

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

view this post on Zulip Yakov Pechersky (Aug 27 2020 at 15:51):

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

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