## Stream: new members

### Topic: Cases on even/oddness of a nat?

#### 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.

#### 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

#### 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


#### Sandy Maguire (Jan 07 2021 at 20:24):

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

#### Alex J. Best (Jan 07 2021 at 20:25):

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

#### 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

#### Eric Wieser (Jan 07 2021 at 20:26):

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

#### Alex J. Best (Jan 07 2021 at 20:28):

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!

#### Sandy Maguire (Jan 07 2021 at 20:29):

how could i have found even_or_odd for myself?

#### 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

#naming :smile:

#### Eric Wieser (Jan 07 2021 at 20:31):

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

thanks all!

#### Sandy Maguire (Jan 07 2021 at 20:46):

how can i refine

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


into n = 0?

#### Sandy Maguire (Jan 07 2021 at 20:52):

got it -- rw h at hn and then linarith

#### 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,
},

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,
{
linarith,
},

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

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


#### Sandy Maguire (Jan 07 2021 at 21:15):

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

#### 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

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

#### Kevin Buzzard (Jan 07 2021 at 21:37):

oh got it:

import data.nat.parity
import tactic

open nat


#### 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


#### Kevin Buzzard (Jan 07 2021 at 21:46):

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

#### 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...

#### 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
-- 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


#### Kevin Buzzard (Jan 07 2021 at 21:58):

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

#### Sandy Maguire (Jan 07 2021 at 21:59):

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

#### 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

#### 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.

#### 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!

#### Kevin Buzzard (Jan 07 2021 at 22:03):

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

#### 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: Dec 20 2023 at 11:08 UTC