even or odd

Stream: general

[Patrick Massot]

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]

Shouldn't this be simp with parity_simps?

[Patrick Massot]

I guess it should, but it isn't.

[Kenny Lau]

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]

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

[Patrick Massot]

(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]

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]

I call this simp magic

[Kenny Lau]

or as Clarke calls it, sufficiently advanced simp technology

[Yury G. Kudryashov]

Look at int.bit_decomp

[Yury G. Kudryashov]

And int.bit_cases_on

[Patrick Massot]

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

[Chris Hughes]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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),
   `[rw add_comm at h1],
   «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]

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.