Nat.mul_sub_mod

Stream: Is there code for X?

[Kim Morrison]

I found

theorem Nat.mul_sub_mod {x n p : Nat} (h : x < n * p) : (n * p - (x + 1)) % n = n - (x % n + 1) := ...

surprisingly awkward to prove. (I need it in Lean, so no imports suggestions are best, but I would be happy with any suggestions of quick proofs.)

[Floris van Doorn]

This was indeed quite painful. At least each individual proof is pretty simple, and these are some useful lemmas to have anyway. Not quite mathlib-free

import Mathlib.Tactic

@[simp]
theorem Nat.mod_lt_iff {a b : Nat} : a % b < b ↔ 0 < b := by
  refine ⟨fun h => zero_lt_of_lt h, fun h => mod_lt _ h⟩

theorem Nat.add_one_mod (a b : Nat) :
    (a + 1) % b = if a % b + 1 = b then 0 else a % b + 1 := by
  rw [← mod_add_mod]
  split_ifs with h
  · rw [h]; simp
  rw [mod_eq]
  simp
  intro h1 h2
  refine h2.not_lt (lt_of_le_of_ne ?_ h) |>.elim
  simp [add_one_le_iff, h1]

theorem Nat.add_mod_eq_add_mod_cancel_right {a b c d : Nat} :
    (a + c) % d = (b + c) % d ↔ a % d = b % d := by
  have (a b) : (a + 1) % d = (b + 1) % d ↔ a % d = b % d := by
    refine ⟨fun h => ?_, fun h => by rw [add_mod a, h, ← add_mod]⟩
    simp_rw [Nat.add_one_mod] at h
    split_ifs at h with h1 h2
    · omega
    · contradiction -- can omega be taught how to do this?
    · contradiction -- can omega be taught how to do this?
    · omega
  induction c using Nat.recAux <;> simp [*, ← add_assoc]

theorem Nat.add_mod_eq_add_mod_cancel_left {a b c d : Nat} :
    (a + b) % d = (a + c) % d ↔ b % d = c % d := by
  simp_rw [add_comm a, Nat.add_mod_eq_add_mod_cancel_right]

theorem Nat.sub_mod_eq {a b c d e : Nat}
    (h1 : a % c = d % c) (h2 : b % c = e % c) (h3 : b ≤ a) (h4 : e ≤ d) (h5 : d < e + c) :
    (a - b) % c = d - e := by
  obtain ⟨k, rfl⟩ := le.dest h3
  obtain ⟨l, rfl⟩ := le.dest h4
  simp at h5 ⊢
  rwa [add_mod, h2, ← add_mod, Nat.add_mod_eq_add_mod_cancel_left, mod_eq_of_lt h5] at h1

theorem Nat.mul_sub_mod {x n p : Nat} (h : x < n * p) :
    (n * p - (x + 1)) % n = n - (x % n + 1) := by
  have h2 : 0 < n := by exact Nat.pos_of_mul_pos_right <| zero_lt_of_lt h
  apply Nat.sub_mod_eq <;> simp [add_one_le_iff, h, h2]

[Kim Morrison]

Oh, that is nicer that what I came to. Is it just simp_rw and split_ifs from Mathlib?

[Kim Morrison]

Hmm, slightly more, okay.

[Kim Morrison]

I am pretty confused why all the simp_rws don't work at rw!

[Kim Morrison]

Your two queries about omega are surely bugs in omega.

[Kim Morrison]

My brutal proof is at https://github.com/leanprover/lean4/pull/3727/files#diff-0dbeee478bb270c49a85d373a39875ebc427323eea248ffa741743cad1648813R813. I will try to reconcile them later. :-)

[Floris van Doorn]

I had to run right after sending, I didn't have time to investigate how much of Mathlib I used.

[Floris van Doorn]

Scott Morrison said:

I am pretty confused why all the simp_rws don't work at rw!

Both simp_rw work as rw if you write the first rewrite rule twice.

[Richard Copley]

Brutal, but import free (just for fun):

theorem Nat.mul_sub_mod {x n p : Nat} (h : x < n * p) : (n * p - (x + 1)) % n = n - (x % n + 1) := by
  cases Nat.eq_zero_or_pos n with
  | inl hn => subst hn ; rw [Nat.zero_mul, Nat.zero_sub, Nat.zero_sub, Nat.zero_mod]
  | inr hn =>
    have hp : 0 < p := Nat.pos_of_ne_zero fun hp => Nat.not_lt_zero x (Nat.mul_zero _ ▸ hp ▸ h)
    have ⟨c, hc⟩ := Nat.exists_eq_add_of_le h
    suffices c % n + x % n = n - 1 by
      rw [hc, Nat.add_sub_cancel_left, Nat.add_comm, Nat.sub_add_eq, ← this, Nat.add_sub_cancel]
    have hc' : (c % n + x % n) % n = n - 1 := by
      suffices n * (p - 1) + (n - 1) = c + x by
        rw [← Nat.mod_eq_of_lt (Nat.sub_lt_self Nat.zero_lt_one hn), ← Nat.add_mod,
          ← Nat.mul_add_mod n (p - 1) (n - 1), this]
      rwa [← Nat.add_sub_assoc hn, ← Nat.mul_succ, Nat.sub_one p, Nat.succ_pred_eq_of_pos hp,
        Nat.sub_eq_iff_eq_add (Nat.mul_pos hn hp), Nat.add_comm c, Nat.add_right_comm]
    cases Nat.lt_or_ge (c % n + x % n) n with
    | inl hlt => rwa [Nat.mod_eq_of_lt hlt] at hc'
    | inr hge =>
      have ⟨k, hk⟩ : ∃ k, c % n + x % n = n + k := Nat.exists_eq_add_of_le hge
      have hk' : k < n - 1 := by
        apply Nat.lt_of_add_lt_add_left (n := n)
        rw [← Nat.add_sub_assoc hn, ← hk, Nat.add_sub_assoc hn]
        exact Nat.add_lt_add_of_lt_of_le (Nat.mod_lt c hn) (Nat.le_sub_one_of_lt (Nat.mod_lt x hn))
      rw [hk, Nat.add_mod_left, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le hk' (Nat.sub_le n _))] at hc'
      exact (Nat.ne_of_lt hk' hc').elim

[Junyan Xu]

This could go next to docs#Nat.mul_sub_div

import Mathlib.Data.Nat.Defs
import Mathlib.Tactic.Contrapose

theorem Nat.mod_eq_sub_div_mul {x y : Nat} : x % y = x - x / y * y := by
  rw [eq_comm, Nat.sub_eq_iff_eq_add (div_mul_le_self _ _), Nat.mul_comm, mod_add_div]

theorem Nat.mul_sub_mod {x n p : Nat} (h : x < n * p) : (n * p - (x + 1)) % n = n - (x % n + 1) := by
  rw [mod_eq_sub_div_mul, mul_sub_div _ _ _ h, Nat.sub_sub, Nat.add_comm, ← Nat.sub_sub,
    Nat.mul_comm _ n, ← Nat.mul_sub_left_distrib, Nat.sub_sub_self, mul_succ, Nat.add_comm]
  · conv in (_ + 1) => rw [← mod_add_div x n, Nat.add_right_comm]
    apply Nat.add_sub_add_right
  rw [Nat.succ_le_iff, Nat.div_lt_iff_lt_mul]
  · rwa [Nat.mul_comm]
  · contrapose! h; rw [Nat.le_zero.mp h, Nat.zero_mul]; apply Nat.zero_le

[Kim Morrison]

@Junyan Xu, unfortunately I really need a mathlib free version, as this is for a BitVec application.

[Kim Morrison]

@Floris van Doorn, I've fixed the omega bug in lean#3736.

[Kim Morrison]

@Junyan Xu, however yours is easy to-demathlib! Thanks!