Zulip Chat Archive

Stream: new members

Topic: How to show 2 \ne 1?


Daniel Fabian (May 26 2020 at 17:59):

I've come across an embarrassingly simple problem:

example : ¬(2 : )  1 :=
begin
    intro h,
    have : (2 : ) = 1 := int.eq_one_of_dvd_one (show (0 : )  2, by simp) h,
    cases this,
end

example : ¬(2 : )  1 :=
begin
    rw nat.dvd_one,
    intro,
    cases a,
end

Due to the local context in my proof, lean wanted me to show the first version (in integers as opposed to natural numbers) and the number of theorems available is substantially smaller. Is there a way to cast the statement down to naturals (even though it's technically a weaker statement, so I might have to prove that 2 and 1 are indeed \ge 0).

And secondly, how do I convince lean that something is impossible, i.e. how do I apply refl in a negative position? Looks like adding it as an assumption and then definition by cases eliminated it.

Also, library_search came up with the idea to call decidable prop on the proposition and use that instead: exact of_to_bool_ff rfl

Is introducing followed by cases the right way to discharge a non-equality proof?

Johan Commelin (May 26 2020 at 17:59):

norm_num?

Johan Commelin (May 26 2020 at 17:59):

exact dec_trivial?

Daniel Fabian (May 26 2020 at 18:00):

norm_num didn't do the trick, because it left everything in integer domain.

Kevin Buzzard (May 26 2020 at 18:01):

Do I need an import for this? Lean is complaining about has_dvd int

Alex J. Best (May 26 2020 at 18:01):

norm_num should close both of those goals.

Kevin Buzzard (May 26 2020 at 18:01):

right

Kevin Buzzard (May 26 2020 at 18:02):

import tactic data.int.modeq

example : ¬(2 : )  1 :=
begin
  norm_num,
end

example : ¬(2 : )  1 :=
begin
  norm_num
end

works fine

Daniel Fabian (May 26 2020 at 18:03):

ah, I didn't know about modeq.

Alex J. Best (May 26 2020 at 18:04):

If the question is how to reduce the first to the second (and not use norm_num, which really is the recommended way) you can do:

example : ¬(2 : )  1 :=
begin
    exact_mod_cast (_ : ¬ (2 1)),
    rw nat.dvd_one,
    intro,
    cases a,
end

Daniel Fabian (May 26 2020 at 18:05):

cool, thanks.


Last updated: Dec 20 2023 at 11:08 UTC