Zulip Chat Archive

Stream: new members

Topic: How to show 2 \ne 1?


view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 26 2020 at 17:59):

norm_num?

view this post on Zulip Johan Commelin (May 26 2020 at 17:59):

exact dec_trivial?

view this post on Zulip Daniel Fabian (May 26 2020 at 18:00):

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

view this post on Zulip Kevin Buzzard (May 26 2020 at 18:01):

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

view this post on Zulip Alex J. Best (May 26 2020 at 18:01):

norm_num should close both of those goals.

view this post on Zulip Kevin Buzzard (May 26 2020 at 18:01):

right

view this post on Zulip 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

view this post on Zulip Daniel Fabian (May 26 2020 at 18:03):

ah, I didn't know about modeq.

view this post on Zulip 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

view this post on Zulip Daniel Fabian (May 26 2020 at 18:05):

cool, thanks.


Last updated: May 14 2021 at 12:18 UTC