Zulip Chat Archive

Stream: new members

Topic: Cases on even/oddness of a nat?


view this post on Zulip Sandy Maguire (Jan 07 2021 at 20:22):

I'm trying to formalize the proof given here https://cs.uwaterloo.ca/~cbruni/videos/Math135SeptDec2015/Lesson01ppplusoneprime.pdf, which wants me to inspect whether a nat is even or odd. Besides writing the type of the theorem, I'm not sure how to make progress here.

view this post on Zulip Sandy Maguire (Jan 07 2021 at 20:22):

I've gotten as far as theorem prime_and_prime_succ : ∀ p, prime p → prime (p + 1) → p = 2 := sorry

view this post on Zulip Alex J. Best (Jan 07 2021 at 20:24):

You can start the proof with

begin
intro  p,
cases nat.even_or_odd p,
end

view this post on Zulip Sandy Maguire (Jan 07 2021 at 20:24):

just what i was looking for, thanks. i can probably get it from there

view this post on Zulip Alex J. Best (Jan 07 2021 at 20:25):

Ooops, I think you have to import data.nat.parity too

view this post on Zulip Eric Wieser (Jan 07 2021 at 20:26):

More generally you can use by_cases h : some_prop if you have an arbitrary condition you want to case on

view this post on Zulip Eric Wieser (Jan 07 2021 at 20:26):

But the lemma above will be more convenient for even/odd

view this post on Zulip Alex J. Best (Jan 07 2021 at 20:28):

And I misread your goal,

theorem prime_and_prime_succ :  p, prime p  prime (p + 1)  p = 2 :=
begin
  intros p hp hp_succ,
  cases nat.even_or_odd p,
 end

would be way better!

view this post on Zulip Sandy Maguire (Jan 07 2021 at 20:29):

how could i have found even_or_odd for myself?

view this post on Zulip Alex J. Best (Jan 07 2021 at 20:31):

I just guessed the name, that requires a little experience with the naming convention though.
You can try searching on https://leanprover-community.github.io/mathlib_docs/ by typing in the top right, I put "even odd" in and it came up as the fourth result or something

view this post on Zulip Bryan Gin-ge Chen (Jan 07 2021 at 20:31):

#naming :smile:

view this post on Zulip Eric Wieser (Jan 07 2021 at 20:31):

Or if desperate, example (n : \N) : is_even n \or is_odd n := by library_search

view this post on Zulip Sandy Maguire (Jan 07 2021 at 20:32):

thanks all!

view this post on Zulip Sandy Maguire (Jan 07 2021 at 20:46):

how can i refine

hn: p = 2 * n
h: n = p

into n = 0?

view this post on Zulip Sandy Maguire (Jan 07 2021 at 20:52):

got it -- rw h at hn and then linarith

view this post on Zulip Sandy Maguire (Jan 07 2021 at 21:13):

took me two hours, but i managed to prove it. anyone mind critiquing my solution for style/ergonomics/anything?

theorem prime_and_prime_succ :  p, prime p  prime (p + 1)  p = 2 :=
begin
  intros p hprime hprimesucc,
  cases even_or_odd p,
  {
    cases h with n hn,
    let hprime2 := hprime,
    cases hprime,
    specialize hprime_right n,
    have n_div_p : n  p,
    {
      exact dvd.intro_left 2 (eq.symm hn)
    },

    cases hprime_right n_div_p,
    {
      linarith,
    },

    have p_zero : p = 0,
    {
      rw h at hn,
      linarith,
    },

    by_contradiction h',
    apply not_prime_zero,
    rw p_zero at hprime2,
    exact hprime2,
  },

  let h2 := h,
  cases h with n hn,
  cases hprimesucc,

  have n_div_succ_p : 2  succ p,
  {
    refine even_iff_two_dvd.mp _,
    refine even_succ.mpr _,
    exact odd_iff_not_even.mp h2,
  },

  specialize hprimesucc_right 2,
  cases hprimesucc_right n_div_succ_p,
  {
    by_contradiction h',
    linarith,
  },

  have n_zero : n = 0,
  {
    linarith,
  },

  rw n_zero at hn,
  by_contradiction,
  refine not_prime_one _,
  have p_one : p = 1,
  {
    linarith,
  },
  rw p_one,
  exact hprime,
end

view this post on Zulip Sandy Maguire (Jan 07 2021 at 21:15):

in particular i hate let hprime2 := hprime, cases hprime to work around cases destroying my term

view this post on Zulip Eric Wieser (Jan 07 2021 at 21:23):

An easy ergonomics thing to start: you can move your forall before the colon as {p} (hprime : prime p) (hprimesucc : prime (p + 1)) : p = 2, which removes the need for intros

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 21:36):

Sandy Maguire said:

took me two hours, but i managed to prove it. anyone mind critiquing my solution for style/ergonomics/anything?

Can you post fully working code? (with all imports and open and etc)

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 21:37):

oh got it:

import data.nat.parity
import tactic

open nat

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 21:42):

I would prove this first:

lemma eq_two_of_prime_and_even (n : ) (hn : even n) (hn' : prime n) : n = 2 :=
begin
  symmetry,
  rw  prime_dvd_prime_iff_eq prime_two hn',
  exact even_iff_two_dvd.mp hn
end

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 21:46):

let h2 := h -- you can use have here instead of let, because h is a proof.

view this post on Zulip Bryan Gin-ge Chen (Jan 07 2021 at 21:55):

Here's my first try:

import data.nat.parity
import data.nat.prime

open nat

theorem prime_and_prime_succ (p : ) (hp : prime p) (hp' : prime (p + 1)) : p = 2 :=
begin
  cases hp.eq_two_or_odd with H H,
  { exact H, },
  { exfalso,
    cases hp'.eq_two_or_odd with H' H',
    { rw succ_inj' at H',
      exact hp.ne_one H', },
    { have : even (p + 1) := begin
        rw  odd_iff at H,
        cases H with k hk,
        rw  succ_inj' at hk,
        use [k + 1, hk],
      end,
      rw  not_even_iff at H',
      exact H' this, } }
end

Undoubtedly this can be golfed further...

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 21:57):

But the proof looks fine, you step forwards showing the stuff in the proof. Here's a shorter proof:

import data.nat.parity
import tactic

open nat

-- an even prime must be 2
lemma eq_two_of_prime_and_even {n : } (hn : even n) (hn' : prime n) : n = 2 :=
begin
  symmetry,
  -- goal now 2 = n
  rw  prime_dvd_prime_iff_eq prime_two hn',
  -- goal now 2 ∣ n which is easy
  exact even_iff_two_dvd.mp hn
end

theorem prime_and_prime_succ (p : ) (hprime : prime p) (hprimesucc : prime (p + 1)) :
  p = 2 :=
begin
  -- p is even or odd
  cases even_or_odd p with hp hp,
  { -- if it's even we're done by the previous lemma
    exact eq_two_of_prime_and_even hp hprime },
  { -- odd case can't happen so let's prove a contradiction
    exfalso,
    -- suffices to prove 1 is prime
    apply not_prime_one,
    -- so it suffices to prove p = 1
    convert hprime,
    -- so it suffices to prove p+1 = 2
    apply nat.add_right_cancel,
    -- but p+1 is prime so it suffices to prove it's even
    convert (eq_two_of_prime_and_even _ hprimesucc).symm,
    -- so it suffices to prove p is isn't even
    rw even_succ,
    -- which we can do because it's odd
    exact odd_iff_not_even.mp hp }
end

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 21:58):

Of course I'm cheating by not formalising the proof you showed, but a shorter proof.

view this post on Zulip Sandy Maguire (Jan 07 2021 at 21:59):

i'll grok my way through these tomorrow. they're SIGNIFICANTLY shorter!

view this post on Zulip Sandy Maguire (Jan 07 2021 at 22:00):

i'd heard great things about this community but never imagined it'd be THIS helpful <3

view this post on Zulip Bryan Gin-ge Chen (Jan 07 2021 at 22:00):

Kevin's is nicer because he extracts a lemma that'd be reasonable to PR to mathlib.

view this post on Zulip Sandy Maguire (Jan 07 2021 at 22:03):

@Kevin Buzzard i just watched your talk on the future of mathematics, and it was wildly inspiring. thanks for giving it!

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 22:03):

Great! Now go formalise a bunch more stuff :-)

view this post on Zulip Ruben Van de Velde (Jan 08 2021 at 09:44):

Alternative approach to Kevin's lemma:

import tactic
import data.nat.parity
import data.nat.prime

open nat

lemma eq_two_of_prime_and_even (n : ) (hn : even n) (hn' : prime n) : n = 2 :=
begin
  contrapose! hn,
  rw [odd_iff_not_even, odd_iff],
  exact hn'.eq_two_or_odd.resolve_left hn,
end

Last updated: May 16 2021 at 05:21 UTC