Integers

Stream: new members

[Ashvni Narayanan]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Scott Morrison]

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]

Can you golf that last line to ?

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

[Kevin Buzzard]

#3132

[Ashvni Narayanan]

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]

Kevin Buzzard said:

#3132

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

[Kevin Buzzard]

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]

So I need to convert the example into a lemma?

[Scott Morrison]

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

[Scott Morrison]

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]

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