Zulip Chat Archive

Stream: general

Topic: even or odd


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 28 2020 at 09:23):

Shouldn't this be simp with parity_simps?

view this post on Zulip Patrick Massot (Apr 28 2020 at 09:25):

I guess it should, but it isn't.

view this post on Zulip 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])

view this post on Zulip Patrick Massot (Apr 28 2020 at 09:27):

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

view this post on Zulip 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 )

view this post on Zulip 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)]

view this post on Zulip Kenny Lau (Apr 28 2020 at 09:32):

I call this simp magic

view this post on Zulip Kenny Lau (Apr 28 2020 at 09:32):

or as Clarke calls it, sufficiently advanced simp technology

view this post on Zulip Yury G. Kudryashov (Apr 28 2020 at 16:21):

Look at int.bit_decomp

view this post on Zulip Yury G. Kudryashov (Apr 28 2020 at 16:22):

And int.bit_cases_on

view this post on Zulip Patrick Massot (Apr 28 2020 at 19:54):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 20:12):

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

view this post on Zulip Patrick Massot (Apr 28 2020 at 20:12):

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

view this post on Zulip 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),
   `[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

view this post on Zulip 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: May 11 2021 at 13:22 UTC