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

#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