Reasoning modulo 4 by cases

Stream: new members

[Aniruddh Agarwal]

If I want to prove something about x % 4, how can I split the current goal into 4 goals with the first one having the additional hypothesis x % 4 = 0 % 4, the second x % 4 = 1 % 4, and so on?

[Patrick Massot]

I tried something at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/even.20or.20odd/near/195632609 but my threat wasn't taken seriously (and indeed I didn't follow up).

[Patrick Massot]

But there is no obstruction beyond available time and energy.

[Mario Carneiro]

doesn't fin_cases work here?

[Patrick Massot]

The thing I linked to is a wrapper around fin_cases

[Mario Carneiro]

okay, but the proof script using fin_cases directly shouldn't be nearly that bad

[Aniruddh Agarwal]

I'm unable to use ring for some reason:

import data.int.basic
import data.nat.parity
import tactic.interval_cases

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

theorem th (y : ℤ) (h : ∃ x : ℤ, y = x*x) : (∃ k, y = 4 * k) ∨ (∃ k, y = 4 * k + 1) :=
begin
  cases h with x hx,
  modulo_cases x : (4 : ℤ); rw hx,
  { left,
    use k * (4 * k),
    sorry },
  { right,
    use 4 * k * k + 2 * k,
    sorry, },
  { left,
    use 4 * k * k + 4 * k + 1,
    sorry },
  { right,
    use 4 * k * k + 6 * k + 2,
    ring }
end

The error I'm getting is

type mismatch at application
  tactic.istep 56 4 56 4 ring
term
  ring
has type
  Type ? → Type ? : Type (?+1)
but is expected to have type
  tactic ?m_1 : Type ?
don't know how to synthesize placeholder
context:
y : ℤ,
h : ∃ (x : ℤ), y = x * x
⊢ Type ?

[Jalex Stark]

you still have all the open statements from the tactic-writing part

[Mario Carneiro]

you haven't imported ring

[Jalex Stark]

ah. Type ? → Type ? : Type (?+1) is the type signature of ring typeclass

[Aniruddh Agarwal]

Can someone help me finish the proof?

import data.int.basic
import data.int.parity
import data.nat.parity
import tactic.interval_cases
import tactic

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

theorem square_eq_zero_or_one_mod_four (y : ℤ) (h : ∃ x : ℤ, y = x*x) : ∃ k, y = 4 * k ∨ y = 4 * k + 1 :=
begin
  cases h with x hx,
  modulo_cases x : (4 : ℤ); rw hx,
  { use k * (4 * k),
    left,
    ring },
  { use 4 * k * k + 2 * k,
    right,
    ring },
  { use 4 * k * k + 4 * k + 1,
    left,
    ring },
  { use 4 * k * k + 6 * k + 2,
    right,
    ring }
end

theorem pyth_triples (x : ℤ) (y : ℤ) (z : ℤ) (h : x*x + y*y = z*z) (h' : x.gcd y = 1 ∧ x.gcd z = 1 ∧ y.gcd z = 1)
  : ¬ (int.even z)
:=
begin
intro hz,
cases square_eq_zero_or_one_mod_four (z*z) (exists.intro z rfl),
cases square_eq_zero_or_one_mod_four (y*y) (exists.intro y rfl),
cases square_eq_zero_or_one_mod_four (x*x) (exists.intro x rfl),
cases h_3 with; cases h_2 with; cases h_1 with,
{ sorry }, -- contradiction gcd =/= 1
{ sorry }, -- contradiction gcd =/= 1
{ sorry }, -- contradiction gcd =/= 1
{ cases hz with,
  rw hz_h at h_1,
  sorry }, -- contradiction, 1 % 4 implies not even
{ sorry }, -- contradiction gcd =/= 1
{ cases hz with,
  rw hz_h at h_1,
  sorry }, -- contradiction, 1 % 4 implies not even
{ rw h_1 at h,
  rw h_2 at h,
  rw h_3 at h,
  sorry }, -- contradiction 1 % 4 + 1 % 4 != 0 % 4
{ rw h_1 at h,
  rw h_2 at h,
  rw h_3 at h,
  sorry }  -- contradiction 1 % 4 + 1 % 4 != 1 % 4
end

[Johan Commelin]

@Aniruddh Agarwal Often you can prove a helper lemma directly by dec_trivial... see for example here: https://github.com/leanprover-community/mathlib/blob/pythagorean_triples_jmc/src/number_theory/pythagorean_triples.lean#L123L126

[Johan Commelin]

I hope you are aware that there is an ongoing PR on pythagorean triples. So please don't duplicate effort, unless this is all for fun.

[Aniruddh Agarwal]

@Johan Commelin Thanks, I'll check that out. I'm just doing this for fun, and don't intend to PR this into mathlib.