## Stream: general

### Topic: even or odd

#### Patrick Massot (Apr 28 2020 at 09:23):

What is the recommended way to prove:

example (n : ℤ) : (∃ k, n = 2*k) ∨ ∃ k, n = 2*k + 1


I can prove it but it's ugly.

#### Johan Commelin (Apr 28 2020 at 09:23):

Shouldn't this be simp with parity_simps?

#### Patrick Massot (Apr 28 2020 at 09:25):

I guess it should, but it isn't.

#### Kenny Lau (Apr 28 2020 at 09:26):

import tactic

example (n : ℤ) : (∃ k, n = 2*k) ∨ (∃ k, n = 2*k + 1) :=
or.cases_on (int.mod_two_eq_zero_or_one n)
(λ h, or.inl ⟨n / 2, by conv_lhs { rw ← int.mod_add_div n 2 }; rw [h, zero_add]⟩)
(λ h, or.inr ⟨n / 2, by conv_lhs { rw ← int.mod_add_div n 2 }; rw [h, add_comm]⟩)


#### Patrick Massot (Apr 28 2020 at 09:27):

Thanks Kenny, it looks like what I have, and this is what I call ugly.

#### Patrick Massot (Apr 28 2020 at 09:27):

(I have by by_cases h : n % 2 = 0 ; [left, {right ; rw int.mod_two_ne_zero at h}] ; rw [← int.mod_add_div n 2, h] ; use n/2 ; ring )

#### Kenny Lau (Apr 28 2020 at 09:30):

import tactic

example (n : ℤ) : (∃ k, n = 2*k) ∨ (∃ k, n = 2*k + 1) :=
by rw ← int.mod_add_div n 2; cases int.mod_two_eq_zero_or_one n; rw [h, add_comm]; simp [exists.intro (n/2)]


#### Kenny Lau (Apr 28 2020 at 09:32):

I call this simp magic

#### Kenny Lau (Apr 28 2020 at 09:32):

or as Clarke calls it, sufficiently advanced simp technology

#### Yury G. Kudryashov (Apr 28 2020 at 16:21):

Look at int.bit_decomp

#### Yury G. Kudryashov (Apr 28 2020 at 16:22):

And int.bit_cases_on

#### Patrick Massot (Apr 28 2020 at 19:54):

Thanks Yury. This is really really arcane though. We need some modulo_cases tactic here.

#### Chris Hughes (Apr 28 2020 at 20:03):

I think Scott wrote a tactic where given a proof that a % b < b you could case split on all the possibilities for a % b.

#### Kevin Buzzard (Apr 28 2020 at 20:12):

Right, I used this a lot in codewars. Interval_cases?

#### Patrick Massot (Apr 28 2020 at 20:12):

Yes, we need to build it on top of interval_cases of course

#### Patrick Massot (Apr 28 2020 at 21:56):

I did it so dirty that the following code should be read by @Rob Lewis and @Gabriel Ebner as a PR threat:

import tactic.interval_cases
import data.int.basic

namespace tactic.interactive
open tactic
open interactive (parse)
open lean.parser (tk)
open interactive.types (texpr)

meta def modulo_cases (n : parse texpr) (q : parse (tk ":" *> texpr)) : tactic unit :=
do qe ← tactic.i_to_expr q,
ne ← tactic.i_to_expr n,
«have» h1 (%%ne = %%ne % %%qe + %%qe * (%%n / %%qe)) ((int.mod_add_div %%ne %%qe).symm),
«have» h2 (%%ne % %%qe < abs %%qe) (int.mod_lt %%ne (by norm_num : (%%qe : ℤ) ≠ 0)),
«have» h4 (0 ≤ (%%qe: ℤ)) (dec_trivial),
[rw abs_of_nonneg h4 at h2],
h4e ← get_local h4,
tactic.clear h4e,
«have» h3 (0 ≤ %%ne % %%qe) (int.mod_nonneg %%ne dec_trivial),
h1e ← get_local h1,
h2e ← get_local h2,
h3e ← get_local h3,
tactic.revert h1e,
tactic.revert h2e,
tactic.revert h3e,
e ← (to_expr (%%ne % %%qe)),
tactic.generalize e,
e ← (to_expr (%%ne / %%qe)),
[ intros r h1 h2 h3,
interval_cases r ; clear h1 h2 ; try {rw add_zero at h3}],
tactic.all_goals \$ do
h3e ← get_local h3,
tactic.revert h3e,
tactic.generalize e,
[rintros k rfl]

end tactic.interactive

example (n : ℤ) : (∃ k, n = 2*k) ∨ (∃ k, n = 2*k + 1) :=
begin
modulo_cases n : (2 : ℤ),
{ left,
use k },
{ right,
use k },
end


#### Patrick Massot (Apr 28 2020 at 21:57):

A (small) part of the problem is I don't know how to parse two texpr in a row without a separating token. And I don't know how to force a type ascription when parsing a texpr`. And then of course the name handling is awful.

Last updated: Aug 03 2023 at 10:10 UTC