## Stream: new members

### Topic: Integers

#### Ashvni Narayanan (Jun 21 2020 at 15:24):

I am trying to prove that val(1)+val(1) = 0 implies val(1) = 0, where val(1) is an integer. I tried to use

rw add_self_eq_zero


I get the error

invalid type ascription, term has type
?m_3 + ?m_3 = 0 ↔ ?m_3 = 0
but is expected to have type
val 1 + val 1 = 0


Technically, val(1) is in with_top \Z . Is that what is causing the error?
Any help is appreciated. Thank you!

#### Kevin Buzzard (Jun 21 2020 at 15:28):

If you hover over add_self_eq_zero , or write #check @add_self_eq_zero, you see

add_self_eq_zero : ∀ {α : Type u_1} [_inst_1 : domain α] [_inst_2 : char_zero α] {a : α}, a + a = 0 ↔ a = 0


#### Kevin Buzzard (Jun 21 2020 at 15:29):

So add_self_eq_zero will only work for domains (this is Lean's word for an integral domain without the commutativity condition) of characteristic zero, and with_top \Z is probably not even a ring.

#### Ashvni Narayanan (Jun 21 2020 at 15:31):

Kevin Buzzard said:

So add_self_eq_zero will only work for domains (this is Lean's word for an integral domain without the commutativity condition) of characteristic zero, and with_top \Z is probably not even a ring.

Ah alright. Thank you!

#### Kevin Buzzard (Jun 21 2020 at 15:31):

Hang on, I'll knock you up a proof. If you're going to be working with with_top you're going to have to learn how to use it.

#### Ashvni Narayanan (Jun 21 2020 at 15:32):

lemma val_one_is_zero : val(1 : K) = 0 :=
begin
have f : (1 : K) = (1:K)*(1:K),
simp,
have g : val(1 : K) = val((1 : K)*(1 : K)),
rw f,
simp,
have k : val((1 : K)*(1 : K)) = val(1 : K) + val(1 : K),
apply mul,
rw k at g,
rw g,
rw <- two_nsmul,
have s : 2*0 = 0,
simp,
sorry,
end


This is where I was. But that goes back to the same thing.

#### Kevin Buzzard (Jun 21 2020 at 15:43):

import tactic

-- the next 10 lines should be in mathlib.
attribute [norm_cast] with_top.coe_eq_coe

@[norm_cast] lemma with_top.coe_zero' {α : Type*}
[add_monoid α] : ((0 : α) : with_top α) = 0 := rfl

@[norm_cast] lemma with_top.coe_eq_zero' {α : Type*}
[add_monoid α] {a : α} : (a : with_top α) = 0 ↔ a = 0 :=
by rw [←with_top.coe_zero', with_top.coe_eq_coe]

/-- An element of ℤ ∪ {⊤} is either ⊤ or in ℤ -/
lemma with_top.cases (a : with_top ℤ) : a = ⊤ ∨ ∃ n : ℤ, a = n :=
begin
cases a with n,
{ -- a = ⊤ case
left,
refl, -- true by definition
},
{ -- ℤ case
right,
use n,
refl, -- true by definition
}
end

example (a : with_top ℤ) : a + a = 0 ↔ a = 0 :=
begin
split,
{ -- the hard way
intro h, -- h is a proof of a+a=0
-- split into cases
cases (with_top.cases a) with htop hn,
{ -- a = ⊤
rw htop at h,
-- h is false
cases h,
-- no cases!
},
{ -- a = n
cases hn with n hn,
rw hn at h ⊢,
-- now h says n+n=0 and our goal is n=0
-- but these are equalities in with_top ℤ
-- so we need to get them into ℤ
-- A tactic called norm_cast does this
norm_cast at h ⊢,
-- we finally have a hypothesis n + n = 0
-- and a goal n = 0
-- and everything is an integer
assumption
}
},
{ -- the easy way
intro ha,
rw ha,
simp
}
end


#### Scott Morrison (Jun 22 2020 at 02:56):

If you add two more simp lemmas you can get it down to:

import tactic

-- the next *11* lines should be in mathlib.
attribute [norm_cast] with_top.coe_eq_coe
attribute [simp] with_top.none_eq_top with_top.some_eq_coe

@[norm_cast] lemma with_top.coe_zero' {α : Type*}
[add_monoid α] : ((0 : α) : with_top α) = 0 := rfl

@[norm_cast] lemma with_top.coe_eq_zero' {α : Type*}
[add_monoid α] {a : α} : (a : with_top α) = 0 ↔ a = 0 :=
by rw [←with_top.coe_zero', with_top.coe_eq_coe]

example (a : with_top ℤ) : a + a = 0 ↔ a = 0 :=
begin
cases a,
{ simp, },
{ simp, norm_cast, simp [add_self_eq_zero], },
end


#### Scott Morrison (Jun 22 2020 at 02:56):

(Of course, there's a non-terminal simp in my example, but it's only an example. :-)

#### Scott Morrison (Jun 22 2020 at 02:58):

Perhaps those two simp lemmas break mathlib elsewhere, I didn't try. @Ashvni Narayanan, would you be interested in trying to PR the extra norm_cast lemmas Kevin proposes?

#### Johan Commelin (Jun 22 2020 at 05:04):

Can you golf that last line to ?

 -- { simp, norm_cast, simp [add_self_eq_zero], },


#3132

#### Ashvni Narayanan (Jun 22 2020 at 12:56):

Scott Morrison said:

Perhaps those two simp lemmas break mathlib elsewhere, I didn't try. Ashvni Narayanan, would you be interested in trying to PR the extra norm_cast lemmas Kevin proposes?

Sure! I don't know if I know how to, but I would like to learn.

#### Ashvni Narayanan (Jun 22 2020 at 12:58):

Kevin Buzzard said:

#3132

As far as I understand, this is about adding the attribute, right?

#### Kevin Buzzard (Jun 22 2020 at 13:07):

Right. So after that PR is accepted norm_cast should behave the way we want it to, and actually coe_zero will work for any type with a 0, as will coe_eq_zero: the lemmas are PR'ed too. But the example is not.

#### Ashvni Narayanan (Jun 22 2020 at 13:09):

So I need to convert the example into a lemma?

#### Scott Morrison (Jun 22 2020 at 23:33):

I did a little experiment making those two lemmas simp lemmas, and unfortunately quite a lot breaks.

#### Scott Morrison (Jun 22 2020 at 23:34):

I think it would nevertheless be a good change at some point --- to insist that simp normal form for expressions involving with_top uses \top instead of none, and uses the coercion rather than some`. But achieving this will require rewiring some proofs in mathlib.

#### Ashvni Narayanan (Jun 23 2020 at 12:41):

https://github.com/leanprover-community/mathlib/pull/3135#discussion_r443758403

Last updated: Dec 20 2023 at 11:08 UTC