# Zulip Chat Archive

## 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_add
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
rw add_self_eq_zero at h,
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_add
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], },
{ norm_cast [add_self_eq_zero], },
```

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

#### 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:

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