Odd number mod eight

Stream: Is there code for X?

[Will Midwood]

Hi all,

I've struggled with trying to prove this theorem:

  example (a: ℤ) (h: odd a): a.nat_abs % 8 ≠ 1 → (3 = a % 8 ∨ 5 = a % 8) := sorry

Any thoughts on how to proceed with proving this in Lean?

[Johan Commelin]

Take a = 7.

[Will Midwood]

Hm it seems I formulated this theorem wrong. It should be:

 example (a: ℤ) (h: odd a): ¬(a % 8 = 1 ∨ a % 8 = -1) → (a % 8 = 3 ∨ a % 8 = 5) := sorry

[Adam Topaz]

a % 8 is never -1.

[Will Midwood]

Is it not equivalent to a ≡ -1 [ZMOD 8]?

[Adam Topaz]

no, a % 8 is the remainder left when a is divided by 8, so it's an element of $\{0,1,\ldots,7\}$.

[Adam Topaz]

just change -1 to 7

[Will Midwood]

Ah right so for

 example (a: ℤ) (h: odd a): ¬(a % 8 = 1 ∨ a % 8 = 7) → (a % 8 = 3 ∨ a % 8 = 5) := sorry

[Adam Topaz]

you could start by rewriting using docs#int.div_add_mod

[Alex J. Best]

tactic#slim_check (https://leanprover-community.github.io/mathlib_docs/tactic/slim_check.html#tactic.interactive.slim_check) is helpful for checking if statements like this are true (I didn't try this example but I don't see why it shouldn't work)

[Adam Topaz]

the odd assumption is an issue for slim_check it seems

[Alex J. Best]

Maybe we need a decidable_pred instance for odd? Which should just be derivable by unfolding the definition?

[Adam Topaz]

yeah I think that's right

[Alex J. Best]

Maybe odd has been generalized to semirings or something so maybe it's not so simple, but we should have it for Z.

[Adam Topaz]

docs#odd

[Kevin Buzzard]

Here's a lazy proof, where I check all the cases in $\Z/8\Z$ and then lift:

import tactic
import data.zmod.basic

-- first work in ℤ/8ℤ
lemma odd_zmod_eight (n : zmod 8) : 2 * n + 1 = 1 ∨ 2 * n + 1 = 3 ∨ 2 * n + 1 = 5 ∨ 2 * n + 1 = 7 :=
begin
  fin_cases n; finish, -- stupid "check all the cases" proof
end
.

-- now lift to ZMOD 8 (an equivalence relation on ℤ)
lemma odd_ZMOD_eight (n : ℤ) : (2 * n + 1) ≡ 1 [ZMOD (8 : ℕ)] ∨ (2 * n + 1) ≡ 3 [ZMOD (8 : ℕ)] ∨
  (2 * n + 1) ≡ 5 [ZMOD (8 : ℕ)] ∨ (2 * n + 1) ≡  7 [ZMOD (8 : ℕ)] :=
begin
  simp only [←zmod.int_coe_eq_int_coe_iff],
  push_cast,
  apply odd_zmod_eight,
end

-- now to ℤ and %
lemma odd_mod_eight (n : ℤ) : (2 * n + 1) % 8 = 1 ∨ (2 * n + 1) % 8 = 3 ∨
  (2 * n + 1) % 8 = 5 ∨ (2 * n + 1) % 8 = 7 :=
odd_ZMOD_eight n -- definitional abuse

-- now do the problem using just logic
example (a: ℤ) (h: odd a): ¬(a % 8 = 1 ∨ a % 8 = 7) → (a % 8 = 3 ∨ a % 8 = 5) :=
begin
  rcases h with ⟨n, rfl⟩,
  have := odd_mod_eight n,
  tauto!,
end

[Kevin Buzzard]

You can tell I've done far too many of these with undergrads ;-)

[Heather Macbeth]

I have written some tactic support for this kind of thing, but it's not all in mathlib. See
https://hrmacbeth.github.io/math2001/04_Proofs_with_Structure_II.html#id29

[Kevin Buzzard]

You can also tell that Heather has done far too many of these things with undergrads, but is also good at tactic writing as opposed to my dirty hackery :-)

[Will Midwood]

I managed to complete the proof by splitting it into 4 cases,

example (a: ℕ) (h: odd a): ¬(a % 8 = 1 ∨ a % 8 = 7) → (a % 8 = 3 ∨ a % 8 = 5) :=
  begin
    intro hn,
    rw not_or_distrib at hn,
    cases hn with hn₁ hn₂,
    have hem: ∀ (a: ℕ), 8*a % 8 = 0, {
      intro a,
      apply nat.mod_eq_zero_of_dvd,
      use a,
    },
    cases h with k hk,
    by_cases hl: even k,
    cases hl with l hl,
    by_cases hm: even l,
    cases hm with m hm,
    exfalso,
    apply hn₁,
    rw [hk, hl, hm],
    ring_nf,
    rw nat.add_mod,
    rw hem,
    by norm_num,
    rw ← nat.odd_iff_not_even at hm,
    cases hm with m hm,
    right,
    rw [hk, hl, hm],
    ring_nf,
    rw nat.add_mod,
    rw hem,
    by norm_num,
    rw ← nat.odd_iff_not_even at hl,
    cases hl with l hl,
    by_cases hm: even l,
    cases hm with m hm,
    left,
    rw [hk, hl, hm],
    ring_nf,
    rw nat.add_mod,
    rw hem,
    by norm_num,
    rw ← nat.odd_iff_not_even at hm,
    cases hm with m hm,
    exfalso,
    apply hn₂,
    rw [hk, hl, hm],
    ring_nf,
    rw nat.add_mod,
    rw hem,
    by norm_num,
  end

[Will Midwood]

Lots of sections of this proof is reusing code from earlier bits of the proof repeated, but I'm not sure how to reduce the redundancies here.

[Alex J. Best]

Heather Macbeth said:

I have written some tactic support for this kind of thing, but it's not all in mathlib. See
https://hrmacbeth.github.io/math2001/04_Proofs_with_Structure_II.html#id29

Can you say a little more sometime about what you've done, sounds very interesting! I guess it's lean 4? But its a little hard to tell what they do from reading that page.

[Kevin Buzzard]

@Will Midwood one thing you might want to avoid is just leaping into a proof and writing one long begin/end block. If you find something which can be split off as a sublemma, split it off! See how I wrote four short proofs instead of one long one?

[Kevin Buzzard]

Also you should structure your proofs more, by adding {}s when you have more than one goal. Right now it's really hard to read your proof because I can't see where one argument is ending and another one beginning.

[Kevin Buzzard]

On the other hand, are you just a lean beginner? It's great that you've got this question out at all if you are!

[Will Midwood]

Thanks for the advice Kevin, I'm not sure I would quite call myself a beginner, I've been using Lean for my undergraduate dissertation since November. I'm in the last stages now and I'm going to go through my code to try make it a bit more readable as per your suggestion.

[Kevin Buzzard]

Ok then it's a bit less surprising that you got the question out (still cool though) but whoever is supervising you should be telling you to write more structured code :-)

[Kevin Buzzard]

Do you understand my proof?

[Will Midwood]

I understand the idea of it, some tactics however I'm not too familiar with such as fin_cases, push_cast or tauto!

[Kevin Buzzard]

You can just hover over the tactics you're not sure of in VS Code and you'll be able to see the docstrings.

[Heather Macbeth]

Alex J. Best said:

Can you say a little more sometime about what you've done, sounds very interesting! I guess it's lean 4? But its a little hard to tell what they do from reading that page.

@Alex J. Best That's true. To explain the nonstandard tactics: They are all finishing tactics designed to fill in single steps in calc proofs.

• numbers is a renaming of norm_num1
• extra proves a relation X + Y ~ X if Y is a "neutral" quantity for that relation, eg
  • when ~ is "greater than" and Y is something which positivity can prove positive
  • when ~ is "congruent mod n" and Y is manifestly zero mod n
• rel [h] proves a relation f X ~ f Y by "substituting" a hypothesis h : X ~ Y, if the function f is well-behaved under the relation, eg
  • when ~ is "greater than" it works if f is built out of additions, subtractions of constants, multiplications by positivity-satisfying constants, and (when Y is positivity-satisfying) exponentiations
  • when ~ is "congruent mod n" it works if f is built out of additions, subtractions, multiplications, exponentiations

The relatively surprising part is that this grammar is flexible enough (together with ring) to cover a full course of elementary mathematics.

[Heather Macbeth]

So here is "Show that if $n^2+n+1\equiv 1\mod 3$ then $n\equiv 0\mod 3$ or $n\equiv 2\mod 3$" in that language.

example (n : ℤ) (hn : n ^ 2 + n + 1 ≡ 1 [ZMOD 3]) : n ≡ 0 [ZMOD 3] ∨ n ≡ 2 [ZMOD 3] := by
  mod_cases h : n % 3
  · -- case 1: `n ≡ 0 [ZMOD 3]`
    left
    apply h
  · -- case 2: `n ≡ 1 [ZMOD 3]`
    have H : 0 ≡ 1 [ZMOD 3]
    · calc 0 ≡ 0 + 3 * 1 [ZMOD 3] := by extra
      _ = 1 ^ 2 + 1 + 1 := by numbers
      _ ≡ n ^ 2 + n + 1 [ZMOD 3] := by rel [h.symm]
      _ ≡ 1 [ZMOD 3] := hn
    numbers at H -- contradiction!
  · -- case 3: `n ≡ 2 [ZMOD 3]`
    right
    apply h

[Heather Macbeth]

I should say that everything is simply a layer of configuration-setting (no backtracking, custom dischargers, attributes with curated lemma sets) on top of @Scott Morrison's Lean 4 solve_by_elim.

[Scott Morrison]

Probably we should get some of these into mathlib4. Different names presumably, and perhaps docs that explain in detail how they are built out of the "core" tactics, so others can use them as models for other specialised tactics.

[Scott Morrison]

I'm impressed by rel being able to "work out" the function f without being told explicitly. That's cool.

[Heather Macbeth]

Yes, I've been surprised by how robust it is. I have (of course) had to answer tons of student questions about the various quirks of Lean syntax and behaviour, and only once has it been "I thought rel should work here, why doesn't it?"

[Heather Macbeth]

(Actually, caveat: fairly often there is a question "I thought rel should work here, why doesn't it?" and the answer is "your mathematics is wrong". But only once when the student's mathematics was correct.)