Examples to get me started with modulus

Stream: new members

[Xavier]

Hello! Very new to Lean4. (Is this even the right place to post newb questions?) Have worked my way through Natural Number Game and read a decent chunk of manuals and ... getting completely lost the moment I try to apply to my own problems.

I want to formalise a proof of "some statement is divisible by X" (e.g. n^3 + 11*n is divisible by 2). Where should I be looking for examples/documentation of builtins for working with modulus? (Searching gets confused with "module" I think.) I've found the operators % and \== and 3 | ... but I'm not sure which is preferred, where it's documented, and what tactics are available. I'm getting lost & confused.

[Daniel Weber]

Are you using Mathlib, or do you not want to depend on it?

[Daniel Weber]

Mathlib has basic results about divisibility in Mathlib.Algebra.Divisibility.Basic

[Daniel Weber]

If you're only working with natural numbers there are lemmas in Init.Data.Nat.Dvd

[Xavier]

thank you! That looks like what I was after.

[Xavier]

ok I'm making forward progress. have a few hopefully remedial questions? Inline in comments:

import Lean
import Mathlib
import Mathlib.Algebra.Divisibility.Basic

example {a b : ℕ} (h : a = 4 * b) : (a ≡ 0 [MOD 2]) := by
  rw [h]                      -- 4 * b = 0 [MOD 2]
  rw [Nat.modEq_zero_iff_dvd] -- 2 | 4 * b
  use 2 * b                   -- 4 * b = 2 * (2 * b)
  ring

-- Q1: "use 2 * b" feels somewhat convoluted to finish this off?
-- Q2: Feels weird to have to convert from MOD into | form?

example {a b : ℕ} (h : a = 4 * b) : (2 | 2 * b) := by
  use b
-- Q3: This doesn't compile: "unexpected token |"

example {a b : ℕ} : (n ^ 3 + 11 * n ≡ 0 [MOD 2]) := by
  have h : n ^ 3 + 11 * n = n * (n ^ 2 + 11) := by linarith
  rw [h]
  cases n with
  | zero => rfl
  | succ =>
    rw [mul_add]
    sorry -- TODO, still working on it

-- Q4: I suppose rfl simplies numeric expressions first?

-- Q5: Sometimes the infoview appears to crash and stop showing any info?
-- Neither Restart File or Server help.

[Daniel Weber]

The problem in the second example is that the character isn't |, but a different Unicode one ∣. You can type it with \dvd

[Daniel Weber]

For the first example you can also go through docs#ZMod :

example {a b : ℕ} (h : a = 4 * b) : (a ≡ 0 [MOD 2]) := by
  rw [h, ← ZMod.eq_iff_modEq_nat, Nat.cast_mul]
  reduce_mod_char

[Daniel Weber]

rfl doesn't simplify numeric expressions, but it unfolds definitions to try and get the values to match. For example, if you have 2 + 2 = 4, then it will unfold it as 2 + 2 = 2 + (1 + 1) = (2 + 1) + 1 = (2 + (0 + 1)) + 1 = ((2 + 0) + 1) + 1 = (2 + 1) + 1 = 3 + 1 = 4 (this is not 100% true for integers, as the kernel has special support for them to make it more efficient, but that's the idea).
Also note that the tactic rfl only tries to apply docs#rfl, which means it says "I have a proof that 2 + 2 = 4 - by reflexivity 2 + 2 = 2 + 2, and that's what we need", and then type checking verifies that 2 + 2 = 4 and 2 + 2 = 2 + 2 are definitionally equal (defeq), so it tries to unify 4 with 2 + 2

[Daniel Weber]

Regarding Q5, we need more details. Are you using VSCode? The website?

[Xavier]

Thank you for this, I'll take a look tonight.

The problem in the second example is that the character isn't |, but a different Unicode one ∣. You can type it with \dvd

ahahahaha that'll do it!

for Q5, yes using VSCode.

[Xavier]

I'm feeling close. All the trivial examples make sense to me now. And I figured out I needed to specify the actual cases I wanted (even_or_odd rather than default zero and succ)

Final thing is how to use he : Even n. Have tried a few different approaches:

example {a b n : ℕ} : (2 ∣ n ^ 3 + 11 * n) := by
  have h : n ^ 3 + 11 * n = n * (n ^ 2 + 11) := by linarith
  rw [h]
  cases Nat.even_or_odd n with
  -- he : Even n
  -- I want to represent n as (Even n) in the goal
  -- then maybe apply even_iff_exists_two_mul (2 * n) * (...) = 2 * (n * ...)
  -- then simp will complete it I think
  --
  -- but I can't find the right order of things that would make that work
  --   rw [he]                       -- tactic 'rewrite' failed, equality or
                                     --  iff proof expected
  --   apply even_iff_exists_two_mul       -- failed to unify
  --   apply even_iff_exists_two_mul.mp he -- cargo culting from an apply? suggest, doesn't work
  | inl he => apply even_iff_exists_two_mul.mp he
  -- Odd case is basically the same as above but with a bit more algebra
  | inr ho => sorry

I think the simplified version of my problem is

example {a b : ℕ} (h : Even a) : 2 ∣ a * a := by
  sorry

[Ruben Van de Velde]

import Mathlib

example {a b n : ℕ} : (2 ∣ n ^ 3 + 11 * n) := by
  have h : n ^ 3 + 11 * n = n * (n ^ 2 + 11) := by linarith
  rw [h]
  cases Nat.even_or_odd n with
  -- he : Even n
  -- I want to represent n as (Even n) in the goal
  -- then maybe apply even_iff_exists_two_mul (2 * n) * (...) = 2 * (n * ...)
  -- then simp will complete it I think
  --
  -- but I can't find the right order of things that would make that work
  --   rw [he]                       -- tactic 'rewrite' failed, equality or
                                     --  iff proof expected
  --   apply even_iff_exists_two_mul       -- failed to unify
  --   apply even_iff_exists_two_mul.mp he -- cargo culting from an apply? suggest, doesn't work
  | inl he =>
      rw [← even_iff_two_dvd] -- state the goal as `Even (n * (n ^ 2 + 11))`
      apply Even.mul_right -- an even number multiplied by any number is even, so it suffices to show that `n` is even
      exact he -- but we know that!
  -- Odd case is basically the same as above but with a bit more algebra
  | inr ho => sorry

[Xavier]

Thank you, and that makes sense. Feels like a "shortcut" though that never really assumed n was Even (i.e. n = 2k), but figured it out from the structure of the problem. I still don't think I've got the mental model right because I don't see how that approach works for the Odd case.

To show that it's even, I think I need to introduce n = 2k + 1 (Odd.exists_bit1?) so I can multiply things out. But I can't do that because the goal doesn't "know" that n is Odd yet. So I'm back to all the same problems I had with my initial Even approach.

Sorry feel like I'm needing to be spoon-fed here but I've been smashing against it for a bit...

[Xavier]

Got it! obtain was what I needed (after being tripped up by unicode again: \< not being ()

Can now express both even and odd "symmetrically"

example {n : ℤ} : (2 ∣ n ^ 3 + 11 * n) := by
  have h : n ^ 3 + 11 * n = n * (n * n + 11) := by linarith
  rw [h]
  cases Int.even_or_odd n with
  | inl he =>
      obtain ⟨k, hk⟩ := he
      rw [hk]
      have p:   (k + k) * ((k + k) * (k + k) + 11)
              = 2 * (k * ((k + k) ^ 2 + 11)) := by linarith
      rw [p]
      exact dvd_mul_right 2 _
  | inr ho =>
      obtain ⟨k, hk⟩ := ho
      rw [hk]
      have p:   (2 * k + 1) * ((2 * k + 1) * (2 * k + 1) + 11)
              = 2 * (4 * k ^ 3 + 6 * k ^ 2 + 14 * k + 6) := by linarith
      rw [p]
      exact dvd_mul_right 2 _

Now god help me as I try to show 3 ∣.....

[Xavier]

Haven't yet figured out how to destructure 3 | into 3k + {0,1,2}, but was able to do it inductively...

lemma mod_3 {n : ℕ} : (3 ∣ n ^ 3 + 11 * n) := by
  induction n with
  | zero => exact dvd_zero 3
  | succ k ih =>
    have q:   (k + 1) ^ 3 + 11 * (k + 1)
            = k ^ 3 + 11 * k + 3 * k^2 + 3 * k + 12 := by linarith
    rw [q]
    rw [← Nat.dvd_add_iff_right]
    exact Nat.dvd_of_mod_eq_zero rfl
    rw [← Nat.dvd_add_iff_right]
    exact Nat.dvd_mul_right 3 k
    rw [← Nat.dvd_add_iff_right]
    exact Nat.dvd_mul_right 3 (k ^ 2)
    exact ih

[Xavier]

For completeness, was able to combine the two proofs to show 6 | which in the end was really straight forward once I remembered I actually had to establish that 2 and 3 are coprime!

(Still want to figure out the 3k + {0,1,2} approach for 3 | but will come back to it)

https://github.com/xaviershay/lean-proofs/blob/main/LeanProofs/Basic.lean

Thank you everyone for your assistance!

[Derek Rhodes]

Hi @Xavier , The Mechanics of Proof has a section on divisibility worth checking out if you haven't seen it:
https://hrmacbeth.github.io/math2001/03_Parity_and_Divisibility.html#divisibility
As for unfolding the definition, it can be done like this:

example : 3 ∣ 6 := by
  dsimp [(· ∣ ·)]

  ⊢ ∃ c, 6 = 3 * c

That particular dsimp invocation is not fun to type, luckily vscode supports snippets, I've found this one to be helpful:

    "unfold divisor": {
        "prefix": "unfold div",
        "body": ["dsimp [(· ∣ ·)] at $1"],
        "description": "unfold a divisor"
    },

[Xavier]

I'd missed that chapter, thanks!