# Zulip Chat Archive

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

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!

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

#### Bryan Gin-ge Chen (Jan 07 2021 at 20:31):

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

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

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

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

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