Zulip Chat Archive

Stream: new members

Topic: proof of two_mul from Mathematics in Lean


view this post on Zulip Mike (Aug 28 2020 at 12:18):

Hi,

Once again, I'm unable to get a proof to work in lean. I'm trying to prove
theorem two_mul (a : R) : 2 * a = a + a :=
from Mathematics in Lean
Here's what I'm trying to make work:

import algebra.ring
import tactic

namespace my_ring

variables {R : Type*} [ring R]

lemma one_and_one_eq_two : 1 + 1 = (2 : R) :=
by refl

theorem two_mul (a : R) : 2 * a = a + a :=
begin
    have h₁ : (1 + 1)* a = 1*a + 1*a,
    {rw add_mul},
    have h₂ : 2*a = 1*a + 1*a,
    {rw one_and_one_eq_two at h₁},
    have h₃ : 2*a = a + a,
    {
        rw one_mul at h₂,
        rw one_mul at h₂
    },
    exact h₃,
end

end my_ring

The proof fails at {rw one_and_one_eq_two at h₁}, with the message
/-
solve1 tactic failed, focused goal has not been solved
state:
R : Type u_1,
_inst_1 : ring R,
a : R,
h₁ : 2 * a = 1 * a + 1 * a
⊢ 2 * a = 1 * a + 1 * a
-/

Would appreciate someone showing me what the heck I'm doing wrong. Thanks!

view this post on Zulip Adam Topaz (Aug 28 2020 at 12:37):

The issue is that you've modified h\_1 in that line, but didn't tell lean to use the modified h\_1 as your proof of h\_2. So a simple fix is to add assumption after rw one_and_one_eq_two at h₁ (or even exact h\_1).

view this post on Zulip Johan Commelin (Aug 28 2020 at 12:49):

@Adam Topaz Pro tip: \1 = \_1

view this post on Zulip Adam Topaz (Aug 28 2020 at 12:50):

WHOA!

view this post on Zulip Adam Topaz (Aug 28 2020 at 12:50):

I think you just saved me millions of keystrokes

view this post on Zulip Mike (Aug 28 2020 at 12:52):

Thank you! That fixes the proof of h₂. Now I just need to prove h₃.

I'm getting this error for that:
/-
rewrite tactic failed, did not find instance of the pattern in the target expression
1 * ?m_3
state:
R : Type u_1,
_inst_1 : ring R,
a : R,
h₁ : (1 + 1) * a = 1 * a + 1 * a,
h₂ : 2 * a = a + a
⊢ 2 * a = a + a
-/
Which seems odd, because there are two 1*a 's in h₂.

view this post on Zulip Adam Topaz (Aug 28 2020 at 13:02):

This is expected. rw will change all instances of the first thing it matches with.
Here's your proof cut down a little bit (note that last have isn't needed).

import algebra.ring
import tactic

namespace my_ring

variables {R : Type*} [ring R]

lemma one_and_one_eq_two : 1 + 1 = (2 : R) :=
by refl

theorem two_mul (a : R) : 2 * a = a + a :=
begin
    have h₁ : (1 + 1)* a = 1*a + 1*a,
    {rw add_mul},
    have h₂ : 2*a = 1*a + 1*a,
    {rwa one_and_one_eq_two at h₁},
    rwa one_mul at h₂,
end

end my_ring

view this post on Zulip Kenny Lau (Aug 28 2020 at 19:58):

in mathlib we use 2-space indent as well as spaces after the opening curly bracket and before the closing one (i.e.
{ lorem ipsum })

view this post on Zulip Kenny Lau (Aug 28 2020 at 19:59):

import algebra.ring
import tactic

namespace my_ring

variables {R : Type*} [ring R]

lemma one_and_one_eq_two : 1 + 1 = (2 : R) :=
rfl

theorem two_mul (a : R) : 2 * a = a + a :=
begin
  have h₁ : (1 + 1) * a = 1 * a + 1 * a,
  { rw add_mul},
  have h₂ : 2 * a = 1 * a + 1 * a,
  { rwa one_and_one_eq_two at h₁ },
  rwa one_mul at h₂,
end

end my_ring

view this post on Zulip Kenny Lau (Aug 28 2020 at 20:00):

we also use spaces around infixes (i.e. 1 * a not 1*a)


Last updated: May 16 2021 at 21:11 UTC