From 791bea027f9cce608232f902554c6ccb0cc039fc Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 16 Dec 2024 14:16:46 +1100 Subject: [PATCH] feat: lemmas about Std.Range (#6396) This PR adds lemmas reducing for loops over `Std.Range` to for loops over `List.range'`. Equivalent theorems previously existed in Batteries, but the underlying definitions have changed so these are written from scratch. --- src/Init/Data/Int/Basic.lean | 2 +- src/Init/Data/List/Notation.lean | 2 +- src/Init/Data/Nat.lean | 2 +- src/Init/Data/Nat/Bitwise/Basic.lean | 2 +- src/Init/Data/Nat/Div.lean | 418 +------------------------ src/Init/Data/Nat/Div/Basic.lean | 437 +++++++++++++++++++++++++++ src/Init/Data/Nat/Div/Lemmas.lean | 52 ++++ src/Init/Data/Nat/Dvd.lean | 2 +- src/Init/Data/Nat/Lemmas.lean | 6 + src/Init/Data/Range.lean | 83 +---- src/Init/Data/Range/Basic.lean | 86 ++++++ src/Init/Data/Range/Lemmas.lean | 103 +++++++ tests/lean/run/nat_mod_defeq.lean | 2 - 13 files changed, 697 insertions(+), 500 deletions(-) create mode 100644 src/Init/Data/Nat/Div/Basic.lean create mode 100644 src/Init/Data/Nat/Div/Lemmas.lean create mode 100644 src/Init/Data/Range/Basic.lean create mode 100644 src/Init/Data/Range/Lemmas.lean diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index dbf661c4be..01f9406f44 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -7,7 +7,7 @@ The integers, with addition, multiplication, and subtraction. -/ prelude import Init.Data.Cast -import Init.Data.Nat.Div +import Init.Data.Nat.Div.Basic set_option linter.missingDocs true -- keep it documented open Nat diff --git a/src/Init/Data/List/Notation.lean b/src/Init/Data/List/Notation.lean index fa46a1eaa3..989dcc710e 100644 --- a/src/Init/Data/List/Notation.lean +++ b/src/Init/Data/List/Notation.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ prelude -import Init.Data.Nat.Div +import Init.Data.Nat.Div.Basic /-! # Notation for `List` literals. diff --git a/src/Init/Data/Nat.lean b/src/Init/Data/Nat.lean index 6ce784e109..a37fee411d 100644 --- a/src/Init/Data/Nat.lean +++ b/src/Init/Data/Nat.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Init.Data.Nat.Basic -import Init.Data.Nat.Div +import Init.Data.Nat.Div.Basic import Init.Data.Nat.Dvd import Init.Data.Nat.Gcd import Init.Data.Nat.MinMax diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean index edc8d67656..dde8c26247 100644 --- a/src/Init/Data/Nat/Bitwise/Basic.lean +++ b/src/Init/Data/Nat/Bitwise/Basic.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Init.Data.Nat.Basic -import Init.Data.Nat.Div +import Init.Data.Nat.Div.Basic import Init.Coe namespace Nat diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean index d3d30d07d2..a7b22d338d 100644 --- a/src/Init/Data/Nat/Div.lean +++ b/src/Init/Data/Nat/Div.lean @@ -1,418 +1,8 @@ /- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Kim Morrison -/ prelude -import Init.WF -import Init.WFTactics -import Init.Data.Nat.Basic - -namespace Nat - -/-- -Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that -there is some `c` such that `b = a * c`. --/ -instance : Dvd Nat where - dvd a b := Exists (fun c => b = a * c) - -theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x := - fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos - -@[extern "lean_nat_div"] -protected def div (x y : @& Nat) : Nat := - if 0 < y ∧ y ≤ x then - Nat.div (x - y) y + 1 - else - 0 -decreasing_by apply div_rec_lemma; assumption - -instance instDiv : Div Nat := ⟨Nat.div⟩ - -theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by - show Nat.div x y = _ - rw [Nat.div] - rfl - -def div.inductionOn.{u} - {motive : Nat → Nat → Sort u} - (x y : Nat) - (ind : ∀ x y, 0 < y ∧ y ≤ x → motive (x - y) y → motive x y) - (base : ∀ x y, ¬(0 < y ∧ y ≤ x) → motive x y) - : motive x y := - if h : 0 < y ∧ y ≤ x then - ind x y h (inductionOn (x - y) y ind base) - else - base x y h -decreasing_by apply div_rec_lemma; assumption - -theorem div_le_self (n k : Nat) : n / k ≤ n := by - induction n using Nat.strongRecOn with - | ind n ih => - rw [div_eq] - -- Note: manual split to avoid Classical.em which is not yet defined - cases (inferInstance : Decidable (0 < k ∧ k ≤ n)) with - | isFalse h => simp [h] - | isTrue h => - suffices (n - k) / k + 1 ≤ n by simp [h, this] - have ⟨hK, hKN⟩ := h - have hSub : n - k < n := sub_lt (Nat.lt_of_lt_of_le hK hKN) hK - have : (n - k) / k ≤ n - k := ih (n - k) hSub - exact succ_le_of_lt (Nat.lt_of_le_of_lt this hSub) - -theorem div_lt_self {n k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) : n / k < n := by - rw [div_eq] - cases (inferInstance : Decidable (0 < k ∧ k ≤ n)) with - | isFalse h => simp [hLtN, h] - | isTrue h => - suffices (n - k) / k + 1 < n by simp [h, this] - have ⟨_, hKN⟩ := h - have : (n - k) / k ≤ n - k := div_le_self (n - k) k - have := Nat.add_le_of_le_sub hKN this - exact Nat.lt_of_lt_of_le (Nat.add_lt_add_left hLtK _) this - -@[extern "lean_nat_mod"] -protected def modCore (x y : @& Nat) : Nat := - if 0 < y ∧ y ≤ x then - Nat.modCore (x - y) y - else - x -decreasing_by apply div_rec_lemma; assumption - -@[extern "lean_nat_mod"] -protected def mod : @& Nat → @& Nat → Nat - /- - Nat.modCore is defined by well-founded recursion and thus irreducible. Nevertheless it is - desirable if trivial `Nat.mod` calculations, namely - * `Nat.mod 0 m` for all `m` - * `Nat.mod n (m+n)` for concrete literals `n` - reduce definitionally. - This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by - definition. - -/ - | 0, _ => 0 - | n@(_ + 1), m => - if m ≤ n -- NB: if n < m does not reduce as well as `m ≤ n`! - then Nat.modCore n m - else n - -instance instMod : Mod Nat := ⟨Nat.mod⟩ - -protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by - show Nat.modCore n m = Nat.mod n m - match n, m with - | 0, _ => - rw [Nat.modCore] - exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle) - | (_ + 1), _ => - rw [Nat.mod]; dsimp - refine iteInduction (fun _ => rfl) (fun h => ?false) -- cannot use `split` this early yet - rw [Nat.modCore] - exact if_neg fun ⟨_hlt, hle⟩ => h hle - -theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by - rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore] - -def mod.inductionOn.{u} - {motive : Nat → Nat → Sort u} - (x y : Nat) - (ind : ∀ x y, 0 < y ∧ y ≤ x → motive (x - y) y → motive x y) - (base : ∀ x y, ¬(0 < y ∧ y ≤ x) → motive x y) - : motive x y := - div.inductionOn x y ind base - -@[simp] theorem mod_zero (a : Nat) : a % 0 = a := - have : (if 0 < 0 ∧ 0 ≤ a then (a - 0) % 0 else a) = a := - have h : ¬ (0 < 0 ∧ 0 ≤ a) := fun ⟨h₁, _⟩ => absurd h₁ (Nat.lt_irrefl _) - if_neg h - (mod_eq a 0).symm ▸ this - -theorem mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a := - have : (if 0 < b ∧ b ≤ a then (a - b) % b else a) = a := - have h' : ¬(0 < b ∧ b ≤ a) := fun ⟨_, h₁⟩ => absurd h₁ (Nat.not_le_of_gt h) - if_neg h' - (mod_eq a b).symm ▸ this - -@[simp] theorem one_mod_eq_zero_iff {n : Nat} : 1 % n = 0 ↔ n = 1 := by - match n with - | 0 => simp - | 1 => simp - | n + 2 => - rw [mod_eq_of_lt (by exact Nat.lt_of_sub_eq_succ rfl)] - simp only [add_one_ne_zero, false_iff, ne_eq] - exact ne_of_beq_eq_false rfl - -@[simp] theorem Nat.zero_eq_one_mod_iff {n : Nat} : 0 = 1 % n ↔ n = 1 := by - rw [eq_comm] - simp - -theorem mod_eq_sub_mod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b := - match eq_zero_or_pos b with - | Or.inl h₁ => h₁.symm ▸ (Nat.sub_zero a).symm ▸ rfl - | Or.inr h₁ => (mod_eq a b).symm ▸ if_pos ⟨h₁, h⟩ - -theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y := by - induction x, y using mod.inductionOn with - | base x y h₁ => - intro h₂ - have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Decidable.not_and_iff_or_not.mp h₁ - match h₁ with - | Or.inl h₁ => exact absurd h₂ h₁ - | Or.inr h₁ => - have hgt : y > x := gt_of_not_le h₁ - have heq : x % y = x := mod_eq_of_lt hgt - rw [← heq] at hgt - exact hgt - | ind x y h h₂ => - intro h₃ - have ⟨_, h₁⟩ := h - rw [mod_eq_sub_mod h₁] - exact h₂ h₃ - -@[simp] protected theorem sub_mod_add_mod_cancel (a b : Nat) [NeZero a] : a - b % a + b % a = a := by - rw [Nat.sub_add_cancel] - cases a with - | zero => simp_all - | succ a => - exact Nat.le_of_lt (mod_lt b (zero_lt_succ a)) - -theorem mod_le (x y : Nat) : x % y ≤ x := by - match Nat.lt_or_ge x y with - | Or.inl h₁ => rw [mod_eq_of_lt h₁]; apply Nat.le_refl - | Or.inr h₁ => match eq_zero_or_pos y with - | Or.inl h₂ => rw [h₂, Nat.mod_zero x]; apply Nat.le_refl - | Or.inr h₂ => exact Nat.le_trans (Nat.le_of_lt (mod_lt _ h₂)) h₁ - -@[simp] theorem zero_mod (b : Nat) : 0 % b = 0 := by - rw [mod_eq] - have : ¬ (0 < b ∧ b = 0) := by - intro ⟨h₁, h₂⟩ - simp_all - simp [this] - -@[simp] theorem mod_self (n : Nat) : n % n = 0 := by - rw [mod_eq_sub_mod (Nat.le_refl _), Nat.sub_self, zero_mod] - -theorem mod_one (x : Nat) : x % 1 = 0 := by - have h : x % 1 < 1 := mod_lt x (by decide) - have : (y : Nat) → y < 1 → y = 0 := by - intro y - cases y with - | zero => intro _; rfl - | succ y => intro h; apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y) - exact this _ h - -theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by - rw [div_eq, mod_eq] - have h : Decidable (0 < n ∧ n ≤ m) := inferInstance - cases h with - | isFalse h => simp [h] - | isTrue h => - simp [h] - have ih := div_add_mod (m - n) n - rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2] -decreasing_by apply div_rec_lemma; assumption - -theorem div_eq_sub_div (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1 := by - rw [div_eq a, if_pos]; constructor <;> assumption - -theorem mod_add_div (m k : Nat) : m % k + k * (m / k) = m := by - induction m, k using mod.inductionOn with rw [div_eq, mod_eq] - | base x y h => simp [h] - | ind x y h IH => simp [h]; rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2] - -theorem mod_def (m k : Nat) : m % k = m - k * (m / k) := by - rw [Nat.sub_eq_of_eq_add] - apply (Nat.mod_add_div _ _).symm - -@[simp] protected theorem div_one (n : Nat) : n / 1 = n := by - have := mod_add_div n 1 - rwa [mod_one, Nat.zero_add, Nat.one_mul] at this - -@[simp] protected theorem div_zero (n : Nat) : n / 0 = 0 := by - rw [div_eq]; simp [Nat.lt_irrefl] - -@[simp] protected theorem zero_div (b : Nat) : 0 / b = 0 := - (div_eq 0 b).trans <| if_neg <| And.rec Nat.not_le_of_gt - -theorem le_div_iff_mul_le (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y := by - induction y, k using mod.inductionOn generalizing x with - (rw [div_eq]; simp [h]; cases x with | zero => simp [zero_le] | succ x => ?_) - | base y k h => - simp only [add_one, succ_mul, false_iff, Nat.not_le, Nat.succ_ne_zero] - refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_left ..) - exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩ - | ind y k h IH => - rw [Nat.add_le_add_iff_right, IH k0, succ_mul, - ← Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_iff_right h.2, Nat.add_sub_cancel] - -protected theorem div_div_eq_div_mul (m n k : Nat) : m / n / k = m / (n * k) := by - cases eq_zero_or_pos k with - | inl k0 => rw [k0, Nat.mul_zero, Nat.div_zero, Nat.div_zero] | inr kpos => ?_ - cases eq_zero_or_pos n with - | inl n0 => rw [n0, Nat.zero_mul, Nat.div_zero, Nat.zero_div] | inr npos => ?_ - - apply Nat.le_antisymm - - apply (le_div_iff_mul_le (Nat.mul_pos npos kpos)).2 - rw [Nat.mul_comm n k, ← Nat.mul_assoc] - apply (le_div_iff_mul_le npos).1 - apply (le_div_iff_mul_le kpos).1 - (apply Nat.le_refl) - - apply (le_div_iff_mul_le kpos).2 - apply (le_div_iff_mul_le npos).2 - rw [Nat.mul_assoc, Nat.mul_comm n k] - apply (le_div_iff_mul_le (Nat.mul_pos kpos npos)).1 - apply Nat.le_refl - -theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m - | m, 0 => by simp - | _, _+1 => (le_div_iff_mul_le (Nat.succ_pos _)).1 (Nat.le_refl _) - -theorem div_lt_iff_lt_mul (Hk : 0 < k) : x / k < y ↔ x < y * k := by - rw [← Nat.not_le, ← Nat.not_le]; exact not_congr (le_div_iff_mul_le Hk) - -@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = (x / z) + 1 := by - rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel] - -@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = (x / z) + 1 := by - rw [Nat.add_comm, add_div_right x H] - -theorem add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z := by - induction z with - | zero => rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero] - | succ z ih => rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]; rfl - -theorem add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z = x / z + y := by - rw [Nat.mul_comm, add_mul_div_left _ _ H] - -@[simp] theorem add_mod_right (x z : Nat) : (x + z) % z = x % z := by - rw [mod_eq_sub_mod (Nat.le_add_left ..), Nat.add_sub_cancel] - -@[simp] theorem add_mod_left (x z : Nat) : (x + z) % x = z % x := by - rw [Nat.add_comm, add_mod_right] - -@[simp] theorem add_mul_mod_self_left (x y z : Nat) : (x + y * z) % y = x % y := by - match z with - | 0 => rw [Nat.mul_zero, Nat.add_zero] - | succ z => rw [mul_succ, ← Nat.add_assoc, add_mod_right, add_mul_mod_self_left (z := z)] - -@[simp] theorem add_mul_mod_self_right (x y z : Nat) : (x + y * z) % z = x % z := by - rw [Nat.mul_comm, add_mul_mod_self_left] - -@[simp] theorem mul_mod_right (m n : Nat) : (m * n) % m = 0 := by - rw [← Nat.zero_add (m * n), add_mul_mod_self_left, zero_mod] - -@[simp] theorem mul_mod_left (m n : Nat) : (m * n) % n = 0 := by - rw [Nat.mul_comm, mul_mod_right] - -protected theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < (k + 1) * n) : m / n = k := -have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun hn => by - rw [hn, Nat.mul_zero] at hi lo; exact absurd lo (Nat.not_le_of_gt hi) -Nat.le_antisymm - (le_of_lt_succ ((Nat.div_lt_iff_lt_mul npos).2 hi)) - ((Nat.le_div_iff_mul_le npos).2 lo) - -theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p := by - match eq_zero_or_pos n with - | .inl h₀ => rw [h₀, Nat.div_zero, Nat.div_zero, Nat.zero_sub] - | .inr h₀ => induction p with - | zero => rw [Nat.mul_zero, Nat.sub_zero, Nat.sub_zero] - | succ p IH => - have h₂ : n * p ≤ x := Nat.le_trans (Nat.mul_le_mul_left _ (le_succ _)) h₁ - have h₃ : x - n * p ≥ n := by - apply Nat.le_of_add_le_add_right - rw [Nat.sub_add_cancel h₂, Nat.add_comm] - rw [mul_succ] at h₁ - exact h₁ - rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃] - simp [Nat.pred_succ, mul_succ, Nat.sub_sub] - -theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - (x + 1)) / n = p - ((x / n) + 1) := by - have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by - rw [n0, Nat.zero_mul] at h₁; exact not_lt_zero _ h₁ - apply Nat.div_eq_of_lt_le - focus - rw [Nat.mul_sub_right_distrib, Nat.mul_comm] - exact Nat.sub_le_sub_left ((div_lt_iff_lt_mul npos).1 (lt_succ_self _)) _ - focus - show succ (pred (n * p - x)) ≤ (succ (pred (p - x / n))) * n - rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁), - fun h => succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)] -- TODO: why is the function needed? - focus - rw [Nat.mul_sub_right_distrib, Nat.mul_comm] - exact Nat.sub_le_sub_left (div_mul_le_self ..) _ - focus - rwa [div_lt_iff_lt_mul npos, Nat.mul_comm] - -theorem mul_mod_mul_left (z x y : Nat) : (z * x) % (z * y) = z * (x % y) := - if y0 : y = 0 then by - rw [y0, Nat.mul_zero, mod_zero, mod_zero] - else if z0 : z = 0 then by - rw [z0, Nat.zero_mul, Nat.zero_mul, Nat.zero_mul, mod_zero] - else by - induction x using Nat.strongRecOn with - | _ n IH => - have y0 : y > 0 := Nat.pos_of_ne_zero y0 - have z0 : z > 0 := Nat.pos_of_ne_zero z0 - cases Nat.lt_or_ge n y with - | inl yn => rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)] - | inr yn => - rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn), - ← Nat.mul_sub_left_distrib] - exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0) - -theorem div_eq_of_lt (h₀ : a < b) : a / b = 0 := by - rw [div_eq a, if_neg] - intro h₁ - apply Nat.not_le_of_gt h₀ h₁.right - -protected theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by - let t := add_mul_div_right 0 m H - rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t - -protected theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m := by - rw [Nat.mul_comm, Nat.mul_div_cancel _ H] - -protected theorem div_le_of_le_mul {m n : Nat} : ∀ {k}, m ≤ k * n → m / k ≤ n - | 0, _ => by simp [Nat.div_zero, n.zero_le] - | succ k, h => by - suffices succ k * (m / succ k) ≤ succ k * n from - Nat.le_of_mul_le_mul_left this (zero_lt_succ _) - have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _ - have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div] - have h3 : m ≤ succ k * n := h - rw [← h2] at h3 - exact Nat.le_trans h1 h3 - -@[simp] theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n := by - induction n <;> simp_all [mul_succ] - -@[simp] theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by - rw [Nat.mul_comm, mul_div_right _ H] - -protected theorem div_self (H : 0 < n) : n / n = 1 := by - let t := add_div_right 0 H - rwa [Nat.zero_add, Nat.zero_div] at t - -protected theorem div_eq_of_eq_mul_left (H1 : 0 < n) (H2 : m = k * n) : m / n = k := -by rw [H2, Nat.mul_div_cancel _ H1] - -protected theorem div_eq_of_eq_mul_right (H1 : 0 < n) (H2 : m = n * k) : m / n = k := -by rw [H2, Nat.mul_div_cancel_left _ H1] - -protected theorem mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) : - m * n / (m * k) = n / k := by rw [← Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H] - -protected theorem mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) : - n * m / (k * m) = n / k := by rw [Nat.mul_comm, Nat.mul_comm k, Nat.mul_div_mul_left _ _ H] - -theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by - match n, Nat.eq_zero_or_pos n with - | _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le - | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _ - - -end Nat +import Init.Data.Nat.Div.Basic +import Init.Data.Nat.Div.Lemmas diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean new file mode 100644 index 0000000000..5ef861af4d --- /dev/null +++ b/src/Init/Data/Nat/Div/Basic.lean @@ -0,0 +1,437 @@ +/- +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.WF +import Init.WFTactics +import Init.Data.Nat.Basic + +namespace Nat + +/-- +Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that +there is some `c` such that `b = a * c`. +-/ +instance : Dvd Nat where + dvd a b := Exists (fun c => b = a * c) + +theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x := + fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos + +@[extern "lean_nat_div"] +protected def div (x y : @& Nat) : Nat := + if 0 < y ∧ y ≤ x then + Nat.div (x - y) y + 1 + else + 0 +decreasing_by apply div_rec_lemma; assumption + +instance instDiv : Div Nat := ⟨Nat.div⟩ + +theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by + show Nat.div x y = _ + rw [Nat.div] + rfl + +def div.inductionOn.{u} + {motive : Nat → Nat → Sort u} + (x y : Nat) + (ind : ∀ x y, 0 < y ∧ y ≤ x → motive (x - y) y → motive x y) + (base : ∀ x y, ¬(0 < y ∧ y ≤ x) → motive x y) + : motive x y := + if h : 0 < y ∧ y ≤ x then + ind x y h (inductionOn (x - y) y ind base) + else + base x y h +decreasing_by apply div_rec_lemma; assumption + +theorem div_le_self (n k : Nat) : n / k ≤ n := by + induction n using Nat.strongRecOn with + | ind n ih => + rw [div_eq] + -- Note: manual split to avoid Classical.em which is not yet defined + cases (inferInstance : Decidable (0 < k ∧ k ≤ n)) with + | isFalse h => simp [h] + | isTrue h => + suffices (n - k) / k + 1 ≤ n by simp [h, this] + have ⟨hK, hKN⟩ := h + have hSub : n - k < n := sub_lt (Nat.lt_of_lt_of_le hK hKN) hK + have : (n - k) / k ≤ n - k := ih (n - k) hSub + exact succ_le_of_lt (Nat.lt_of_le_of_lt this hSub) + +theorem div_lt_self {n k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) : n / k < n := by + rw [div_eq] + cases (inferInstance : Decidable (0 < k ∧ k ≤ n)) with + | isFalse h => simp [hLtN, h] + | isTrue h => + suffices (n - k) / k + 1 < n by simp [h, this] + have ⟨_, hKN⟩ := h + have : (n - k) / k ≤ n - k := div_le_self (n - k) k + have := Nat.add_le_of_le_sub hKN this + exact Nat.lt_of_lt_of_le (Nat.add_lt_add_left hLtK _) this + +@[extern "lean_nat_mod"] +protected def modCore (x y : @& Nat) : Nat := + if 0 < y ∧ y ≤ x then + Nat.modCore (x - y) y + else + x +decreasing_by apply div_rec_lemma; assumption + +@[extern "lean_nat_mod"] +protected def mod : @& Nat → @& Nat → Nat + /- + Nat.modCore is defined by well-founded recursion and thus irreducible. Nevertheless it is + desirable if trivial `Nat.mod` calculations, namely + * `Nat.mod 0 m` for all `m` + * `Nat.mod n (m+n)` for concrete literals `n` + reduce definitionally. + This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by + definition. + -/ + | 0, _ => 0 + | n@(_ + 1), m => + if m ≤ n -- NB: if n < m does not reduce as well as `m ≤ n`! + then Nat.modCore n m + else n + +instance instMod : Mod Nat := ⟨Nat.mod⟩ + +protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by + show Nat.modCore n m = Nat.mod n m + match n, m with + | 0, _ => + rw [Nat.modCore] + exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle) + | (_ + 1), _ => + rw [Nat.mod]; dsimp + refine iteInduction (fun _ => rfl) (fun h => ?false) -- cannot use `split` this early yet + rw [Nat.modCore] + exact if_neg fun ⟨_hlt, hle⟩ => h hle + +theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by + rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore] + +def mod.inductionOn.{u} + {motive : Nat → Nat → Sort u} + (x y : Nat) + (ind : ∀ x y, 0 < y ∧ y ≤ x → motive (x - y) y → motive x y) + (base : ∀ x y, ¬(0 < y ∧ y ≤ x) → motive x y) + : motive x y := + div.inductionOn x y ind base + +@[simp] theorem mod_zero (a : Nat) : a % 0 = a := + have : (if 0 < 0 ∧ 0 ≤ a then (a - 0) % 0 else a) = a := + have h : ¬ (0 < 0 ∧ 0 ≤ a) := fun ⟨h₁, _⟩ => absurd h₁ (Nat.lt_irrefl _) + if_neg h + (mod_eq a 0).symm ▸ this + +theorem mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a := + have : (if 0 < b ∧ b ≤ a then (a - b) % b else a) = a := + have h' : ¬(0 < b ∧ b ≤ a) := fun ⟨_, h₁⟩ => absurd h₁ (Nat.not_le_of_gt h) + if_neg h' + (mod_eq a b).symm ▸ this + +@[simp] theorem one_mod_eq_zero_iff {n : Nat} : 1 % n = 0 ↔ n = 1 := by + match n with + | 0 => simp + | 1 => simp + | n + 2 => + rw [mod_eq_of_lt (by exact Nat.lt_of_sub_eq_succ rfl)] + simp only [add_one_ne_zero, false_iff, ne_eq] + exact ne_of_beq_eq_false rfl + +@[simp] theorem Nat.zero_eq_one_mod_iff {n : Nat} : 0 = 1 % n ↔ n = 1 := by + rw [eq_comm] + simp + +theorem mod_eq_sub_mod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b := + match eq_zero_or_pos b with + | Or.inl h₁ => h₁.symm ▸ (Nat.sub_zero a).symm ▸ rfl + | Or.inr h₁ => (mod_eq a b).symm ▸ if_pos ⟨h₁, h⟩ + +theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y := by + induction x, y using mod.inductionOn with + | base x y h₁ => + intro h₂ + have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Decidable.not_and_iff_or_not.mp h₁ + match h₁ with + | Or.inl h₁ => exact absurd h₂ h₁ + | Or.inr h₁ => + have hgt : y > x := gt_of_not_le h₁ + have heq : x % y = x := mod_eq_of_lt hgt + rw [← heq] at hgt + exact hgt + | ind x y h h₂ => + intro h₃ + have ⟨_, h₁⟩ := h + rw [mod_eq_sub_mod h₁] + exact h₂ h₃ + +@[simp] protected theorem sub_mod_add_mod_cancel (a b : Nat) [NeZero a] : a - b % a + b % a = a := by + rw [Nat.sub_add_cancel] + cases a with + | zero => simp_all + | succ a => + exact Nat.le_of_lt (mod_lt b (zero_lt_succ a)) + +theorem mod_le (x y : Nat) : x % y ≤ x := by + match Nat.lt_or_ge x y with + | Or.inl h₁ => rw [mod_eq_of_lt h₁]; apply Nat.le_refl + | Or.inr h₁ => match eq_zero_or_pos y with + | Or.inl h₂ => rw [h₂, Nat.mod_zero x]; apply Nat.le_refl + | Or.inr h₂ => exact Nat.le_trans (Nat.le_of_lt (mod_lt _ h₂)) h₁ + +@[simp] theorem zero_mod (b : Nat) : 0 % b = 0 := by + rw [mod_eq] + have : ¬ (0 < b ∧ b = 0) := by + intro ⟨h₁, h₂⟩ + simp_all + simp [this] + +@[simp] theorem mod_self (n : Nat) : n % n = 0 := by + rw [mod_eq_sub_mod (Nat.le_refl _), Nat.sub_self, zero_mod] + +theorem mod_one (x : Nat) : x % 1 = 0 := by + have h : x % 1 < 1 := mod_lt x (by decide) + have : (y : Nat) → y < 1 → y = 0 := by + intro y + cases y with + | zero => intro _; rfl + | succ y => intro h; apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y) + exact this _ h + +theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by + rw [div_eq, mod_eq] + have h : Decidable (0 < n ∧ n ≤ m) := inferInstance + cases h with + | isFalse h => simp [h] + | isTrue h => + simp [h] + have ih := div_add_mod (m - n) n + rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2] +decreasing_by apply div_rec_lemma; assumption + +theorem div_eq_sub_div (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1 := by + rw [div_eq a, if_pos]; constructor <;> assumption + +theorem mod_add_div (m k : Nat) : m % k + k * (m / k) = m := by + induction m, k using mod.inductionOn with rw [div_eq, mod_eq] + | base x y h => simp [h] + | ind x y h IH => simp [h]; rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2] + +theorem mod_def (m k : Nat) : m % k = m - k * (m / k) := by + rw [Nat.sub_eq_of_eq_add] + apply (Nat.mod_add_div _ _).symm + +theorem mod_eq_sub_mul_div {x k : Nat} : x % k = x - k * (x / k) := mod_def _ _ + +theorem mod_eq_sub_div_mul {x k : Nat} : x % k = x - (x / k) * k := by + rw [mod_eq_sub_mul_div, Nat.mul_comm] + +@[simp] protected theorem div_one (n : Nat) : n / 1 = n := by + have := mod_add_div n 1 + rwa [mod_one, Nat.zero_add, Nat.one_mul] at this + +@[simp] protected theorem div_zero (n : Nat) : n / 0 = 0 := by + rw [div_eq]; simp [Nat.lt_irrefl] + +@[simp] protected theorem zero_div (b : Nat) : 0 / b = 0 := + (div_eq 0 b).trans <| if_neg <| And.rec Nat.not_le_of_gt + +theorem le_div_iff_mul_le (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y := by + induction y, k using mod.inductionOn generalizing x with + (rw [div_eq]; simp [h]; cases x with | zero => simp [zero_le] | succ x => ?_) + | base y k h => + simp only [add_one, succ_mul, false_iff, Nat.not_le, Nat.succ_ne_zero] + refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_left ..) + exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩ + | ind y k h IH => + rw [Nat.add_le_add_iff_right, IH k0, succ_mul, + ← Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_iff_right h.2, Nat.add_sub_cancel] + +protected theorem div_div_eq_div_mul (m n k : Nat) : m / n / k = m / (n * k) := by + cases eq_zero_or_pos k with + | inl k0 => rw [k0, Nat.mul_zero, Nat.div_zero, Nat.div_zero] | inr kpos => ?_ + cases eq_zero_or_pos n with + | inl n0 => rw [n0, Nat.zero_mul, Nat.div_zero, Nat.zero_div] | inr npos => ?_ + + apply Nat.le_antisymm + + apply (le_div_iff_mul_le (Nat.mul_pos npos kpos)).2 + rw [Nat.mul_comm n k, ← Nat.mul_assoc] + apply (le_div_iff_mul_le npos).1 + apply (le_div_iff_mul_le kpos).1 + (apply Nat.le_refl) + + apply (le_div_iff_mul_le kpos).2 + apply (le_div_iff_mul_le npos).2 + rw [Nat.mul_assoc, Nat.mul_comm n k] + apply (le_div_iff_mul_le (Nat.mul_pos kpos npos)).1 + apply Nat.le_refl + +theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m + | m, 0 => by simp + | _, _+1 => (le_div_iff_mul_le (Nat.succ_pos _)).1 (Nat.le_refl _) + +theorem div_lt_iff_lt_mul (Hk : 0 < k) : x / k < y ↔ x < y * k := by + rw [← Nat.not_le, ← Nat.not_le]; exact not_congr (le_div_iff_mul_le Hk) + +theorem pos_of_div_pos {a b : Nat} (h : 0 < a / b) : 0 < a := by + cases b with + | zero => simp at h + | succ b => + match a, h with + | 0, h => simp at h + | a + 1, _ => exact zero_lt_succ a + +@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = (x / z) + 1 := by + rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel] + +@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = (x / z) + 1 := by + rw [Nat.add_comm, add_div_right x H] + +theorem add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z := by + induction z with + | zero => rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero] + | succ z ih => rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]; rfl + +theorem add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z = x / z + y := by + rw [Nat.mul_comm, add_mul_div_left _ _ H] + +@[simp] theorem add_mod_right (x z : Nat) : (x + z) % z = x % z := by + rw [mod_eq_sub_mod (Nat.le_add_left ..), Nat.add_sub_cancel] + +@[simp] theorem add_mod_left (x z : Nat) : (x + z) % x = z % x := by + rw [Nat.add_comm, add_mod_right] + +@[simp] theorem add_mul_mod_self_left (x y z : Nat) : (x + y * z) % y = x % y := by + match z with + | 0 => rw [Nat.mul_zero, Nat.add_zero] + | succ z => rw [mul_succ, ← Nat.add_assoc, add_mod_right, add_mul_mod_self_left (z := z)] + +@[simp] theorem mul_add_mod_self_left (a b c : Nat) : (a * b + c) % a = c % a := by + rw [Nat.add_comm, Nat.add_mul_mod_self_left] + +@[simp] theorem add_mul_mod_self_right (x y z : Nat) : (x + y * z) % z = x % z := by + rw [Nat.mul_comm, add_mul_mod_self_left] + +@[simp] theorem mul_add_mod_self_right (a b c : Nat) : (a * b + c) % b = c % b := by + rw [Nat.add_comm, Nat.add_mul_mod_self_right] + +@[simp] theorem mul_mod_right (m n : Nat) : (m * n) % m = 0 := by + rw [← Nat.zero_add (m * n), add_mul_mod_self_left, zero_mod] + +@[simp] theorem mul_mod_left (m n : Nat) : (m * n) % n = 0 := by + rw [Nat.mul_comm, mul_mod_right] + +protected theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < (k + 1) * n) : m / n = k := +have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun hn => by + rw [hn, Nat.mul_zero] at hi lo; exact absurd lo (Nat.not_le_of_gt hi) +Nat.le_antisymm + (le_of_lt_succ ((Nat.div_lt_iff_lt_mul npos).2 hi)) + ((Nat.le_div_iff_mul_le npos).2 lo) + +theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p := by + match eq_zero_or_pos n with + | .inl h₀ => rw [h₀, Nat.div_zero, Nat.div_zero, Nat.zero_sub] + | .inr h₀ => induction p with + | zero => rw [Nat.mul_zero, Nat.sub_zero, Nat.sub_zero] + | succ p IH => + have h₂ : n * p ≤ x := Nat.le_trans (Nat.mul_le_mul_left _ (le_succ _)) h₁ + have h₃ : x - n * p ≥ n := by + apply Nat.le_of_add_le_add_right + rw [Nat.sub_add_cancel h₂, Nat.add_comm] + rw [mul_succ] at h₁ + exact h₁ + rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃] + simp [Nat.pred_succ, mul_succ, Nat.sub_sub] + +theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - (x + 1)) / n = p - ((x / n) + 1) := by + have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by + rw [n0, Nat.zero_mul] at h₁; exact not_lt_zero _ h₁ + apply Nat.div_eq_of_lt_le + focus + rw [Nat.mul_sub_right_distrib, Nat.mul_comm] + exact Nat.sub_le_sub_left ((div_lt_iff_lt_mul npos).1 (lt_succ_self _)) _ + focus + show succ (pred (n * p - x)) ≤ (succ (pred (p - x / n))) * n + rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁), + fun h => succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)] -- TODO: why is the function needed? + focus + rw [Nat.mul_sub_right_distrib, Nat.mul_comm] + exact Nat.sub_le_sub_left (div_mul_le_self ..) _ + focus + rwa [div_lt_iff_lt_mul npos, Nat.mul_comm] + +theorem mul_mod_mul_left (z x y : Nat) : (z * x) % (z * y) = z * (x % y) := + if y0 : y = 0 then by + rw [y0, Nat.mul_zero, mod_zero, mod_zero] + else if z0 : z = 0 then by + rw [z0, Nat.zero_mul, Nat.zero_mul, Nat.zero_mul, mod_zero] + else by + induction x using Nat.strongRecOn with + | _ n IH => + have y0 : y > 0 := Nat.pos_of_ne_zero y0 + have z0 : z > 0 := Nat.pos_of_ne_zero z0 + cases Nat.lt_or_ge n y with + | inl yn => rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)] + | inr yn => + rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn), + ← Nat.mul_sub_left_distrib] + exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0) + +theorem div_eq_of_lt (h₀ : a < b) : a / b = 0 := by + rw [div_eq a, if_neg] + intro h₁ + apply Nat.not_le_of_gt h₀ h₁.right + +protected theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by + let t := add_mul_div_right 0 m H + rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t + +protected theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m := by + rw [Nat.mul_comm, Nat.mul_div_cancel _ H] + +protected theorem div_le_of_le_mul {m n : Nat} : ∀ {k}, m ≤ k * n → m / k ≤ n + | 0, _ => by simp [Nat.div_zero, n.zero_le] + | succ k, h => by + suffices succ k * (m / succ k) ≤ succ k * n from + Nat.le_of_mul_le_mul_left this (zero_lt_succ _) + have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _ + have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div] + have h3 : m ≤ succ k * n := h + rw [← h2] at h3 + exact Nat.le_trans h1 h3 + +@[simp] theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n := by + induction n <;> simp_all [mul_succ] + +@[simp] theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by + rw [Nat.mul_comm, mul_div_right _ H] + +protected theorem div_self (H : 0 < n) : n / n = 1 := by + let t := add_div_right 0 H + rwa [Nat.zero_add, Nat.zero_div] at t + +protected theorem div_eq_of_eq_mul_left (H1 : 0 < n) (H2 : m = k * n) : m / n = k := +by rw [H2, Nat.mul_div_cancel _ H1] + +protected theorem div_eq_of_eq_mul_right (H1 : 0 < n) (H2 : m = n * k) : m / n = k := +by rw [H2, Nat.mul_div_cancel_left _ H1] + +protected theorem mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) : + m * n / (m * k) = n / k := by rw [← Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H] + +protected theorem mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) : + n * m / (k * m) = n / k := by rw [Nat.mul_comm, Nat.mul_comm k, Nat.mul_div_mul_left _ _ H] + +theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by + match n, Nat.eq_zero_or_pos n with + | _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le + | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _ + + +end Nat diff --git a/src/Init/Data/Nat/Div/Lemmas.lean b/src/Init/Data/Nat/Div/Lemmas.lean new file mode 100644 index 0000000000..538a925689 --- /dev/null +++ b/src/Init/Data/Nat/Div/Lemmas.lean @@ -0,0 +1,52 @@ +/- +Copyright (c) 2024 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +prelude +import Init.Omega +import Init.Data.Nat.Lemmas + +/-! +# Further lemmas about `Nat.div` and `Nat.mod`, with the convenience of having `omega` available. +-/ + +namespace Nat + +theorem lt_div_iff_mul_lt (h : 0 < k) : x < y / k ↔ x * k < y - (k - 1) := by + have t := le_div_iff_mul_le h (x := x + 1) (y := y) + rw [succ_le, add_one_mul] at t + have s : k = k - 1 + 1 := by omega + conv at t => rhs; lhs; rhs; rw [s] + rw [← Nat.add_assoc, succ_le, add_lt_iff_lt_sub_right] at t + exact t + +theorem div_le_iff_le_mul (h : 0 < k) : x / k ≤ y ↔ x ≤ y * k + k - 1 := by + rw [le_iff_lt_add_one, Nat.div_lt_iff_lt_mul h, Nat.add_one_mul] + omega + +-- TODO: reprove `div_eq_of_lt_le` in terms of this: +theorem div_eq_iff (h : 0 < k) : x / k = y ↔ x ≤ y * k + k - 1 ∧ y * k ≤ x := by + rw [Nat.eq_iff_le_and_ge, le_div_iff_mul_le h, Nat.div_le_iff_le_mul h] + +theorem lt_of_div_eq_zero (h : 0 < k) (h' : x / k = 0) : x < k := by + rw [div_eq_iff h] at h' + omega + +theorem div_eq_zero_iff_lt (h : 0 < k) : x / k = 0 ↔ x < k := + ⟨lt_of_div_eq_zero h, fun h' => Nat.div_eq_of_lt h'⟩ + +theorem div_mul_self_eq_mod_sub_self {x k : Nat} : (x / k) * k = x - (x % k) := by + have := mod_eq_sub_div_mul (x := x) (k := k) + have := div_mul_le_self x k + omega + +theorem mul_div_self_eq_mod_sub_self {x k : Nat} : k * (x / k) = x - (x % k) := by + rw [Nat.mul_comm, div_mul_self_eq_mod_sub_self] + +theorem lt_div_mul_self (h : 0 < k) (w : k ≤ x) : x - k < x / k * k := by + rw [div_mul_self_eq_mod_sub_self] + have : x % k < k := mod_lt x h + omega + +end Nat diff --git a/src/Init/Data/Nat/Dvd.lean b/src/Init/Data/Nat/Dvd.lean index 5571de440f..3a58c1b544 100644 --- a/src/Init/Data/Nat/Dvd.lean +++ b/src/Init/Data/Nat/Dvd.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro -/ prelude -import Init.Data.Nat.Div +import Init.Data.Nat.Div.Basic import Init.Meta namespace Nat diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 7509ebe06a..2fd5a8d700 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -176,6 +176,9 @@ protected theorem add_pos_right (m) (h : 0 < n) : 0 < m + n := protected theorem add_self_ne_one : ∀ n, n + n ≠ 1 | n+1, h => by rw [Nat.succ_add, Nat.succ.injEq] at h; contradiction +theorem le_iff_lt_add_one : x ≤ y ↔ x < y + 1 := by + omega + /-! ## sub -/ protected theorem sub_one (n) : n - 1 = pred n := rfl @@ -225,6 +228,9 @@ protected theorem sub_le_iff_le_add' {a b c : Nat} : a - b ≤ c ↔ a ≤ b + c protected theorem le_sub_iff_add_le {n : Nat} (h : k ≤ m) : n ≤ m - k ↔ n + k ≤ m := ⟨Nat.add_le_of_le_sub h, Nat.le_sub_of_add_le⟩ +theorem add_lt_iff_lt_sub_right {a b c : Nat} : a + b < c ↔ a < c - b := by + omega + protected theorem add_le_of_le_sub' {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k := Nat.add_comm .. ▸ Nat.add_le_of_le_sub h diff --git a/src/Init/Data/Range.lean b/src/Init/Data/Range.lean index 2dee612656..1915f4be9b 100644 --- a/src/Init/Data/Range.lean +++ b/src/Init/Data/Range.lean @@ -1,83 +1,8 @@ /- -Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Kim Morrison -/ prelude -import Init.Meta -import Init.Omega - -namespace Std --- We put `Range` in `Init` because we want the notation `[i:j]` without importing `Std` --- We don't put `Range` in the top-level namespace to avoid collisions with user defined types -structure Range where - start : Nat := 0 - stop : Nat - step : Nat := 1 - step_pos : 0 < step - -instance : Membership Nat Range where - mem r i := r.start ≤ i ∧ i < r.stop ∧ (i - r.start) % r.step = 0 - -namespace Range -universe u v - -@[inline] protected def forIn' [Monad m] (range : Range) (init : β) - (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) : m β := - let rec @[specialize] loop (b : β) (i : Nat) - (hs : (i - range.start) % range.step = 0) (hl : range.start ≤ i := by omega) : m β := do - if h : i < range.stop then - match (← f i ⟨hl, by omega, hs⟩ b) with - | .done b => pure b - | .yield b => - have := range.step_pos - loop b (i + range.step) (by rwa [Nat.add_comm, Nat.add_sub_assoc hl, Nat.add_mod_left]) - else - pure b - have := range.step_pos - loop init range.start (by simp) - -instance : ForIn' m Range Nat inferInstance where - forIn' := Range.forIn' - --- No separate `ForIn` instance is required because it can be derived from `ForIn'`. - -@[inline] protected def forM [Monad m] (range : Range) (f : Nat → m PUnit) : m PUnit := - let rec @[specialize] loop (i : Nat): m PUnit := do - if i < range.stop then - f i - have := range.step_pos - loop (i + range.step) - else - pure ⟨⟩ - have := range.step_pos - loop range.start - -instance : ForM m Range Nat where - forM := Range.forM - -syntax:max "[" withoutPosition(":" term) "]" : term -syntax:max "[" withoutPosition(term ":" term) "]" : term -syntax:max "[" withoutPosition(":" term ":" term) "]" : term -syntax:max "[" withoutPosition(term ":" term ":" term) "]" : term - -macro_rules - | `([ : $stop]) => `({ stop := $stop, step_pos := Nat.zero_lt_one : Range }) - | `([ $start : $stop ]) => `({ start := $start, stop := $stop, step_pos := Nat.zero_lt_one : Range }) - | `([ $start : $stop : $step ]) => `({ start := $start, stop := $stop, step := $step, step_pos := by decide : Range }) - | `([ : $stop : $step ]) => `({ stop := $stop, step := $step, step_pos := by decide : Range }) - -end Range -end Std - -theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop := h.2.1 - -theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i := h.1 - -theorem Membership.mem.step {i : Nat} {r : Std.Range} (h : i ∈ r) : (i - r.start) % r.step = 0 := h.2.2 - -theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) : - i < n := h₂ ▸ h₁.2.1 - -macro_rules - | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Membership.get_elem_helper; assumption; rfl) +import Init.Data.Range.Basic +import Init.Data.Range.Lemmas diff --git a/src/Init/Data/Range/Basic.lean b/src/Init/Data/Range/Basic.lean new file mode 100644 index 0000000000..b2f7ecbe24 --- /dev/null +++ b/src/Init/Data/Range/Basic.lean @@ -0,0 +1,86 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Meta +import Init.Omega + +namespace Std +-- We put `Range` in `Init` because we want the notation `[i:j]` without importing `Std` +-- We don't put `Range` in the top-level namespace to avoid collisions with user defined types +structure Range where + start : Nat := 0 + stop : Nat + step : Nat := 1 + step_pos : 0 < step + +instance : Membership Nat Range where + mem r i := r.start ≤ i ∧ i < r.stop ∧ (i - r.start) % r.step = 0 + +namespace Range +universe u v + +/-- The number of elements in the range. -/ +def size (r : Range) : Nat := (r.stop - r.start + r.step - 1) / r.step + +@[inline] protected def forIn' [Monad m] (range : Range) (init : β) + (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) : m β := + let rec @[specialize] loop (b : β) (i : Nat) + (hs : (i - range.start) % range.step = 0) (hl : range.start ≤ i := by omega) : m β := do + if h : i < range.stop then + match (← f i ⟨hl, by omega, hs⟩ b) with + | .done b => pure b + | .yield b => + have := range.step_pos + loop b (i + range.step) (by rwa [Nat.add_comm, Nat.add_sub_assoc hl, Nat.add_mod_left]) + else + pure b + have := range.step_pos + loop init range.start (by simp) + +instance : ForIn' m Range Nat inferInstance where + forIn' := Range.forIn' + +-- No separate `ForIn` instance is required because it can be derived from `ForIn'`. + +@[inline] protected def forM [Monad m] (range : Range) (f : Nat → m PUnit) : m PUnit := + let rec @[specialize] loop (i : Nat): m PUnit := do + if i < range.stop then + f i + have := range.step_pos + loop (i + range.step) + else + pure ⟨⟩ + have := range.step_pos + loop range.start + +instance : ForM m Range Nat where + forM := Range.forM + +syntax:max "[" withoutPosition(":" term) "]" : term +syntax:max "[" withoutPosition(term ":" term) "]" : term +syntax:max "[" withoutPosition(":" term ":" term) "]" : term +syntax:max "[" withoutPosition(term ":" term ":" term) "]" : term + +macro_rules + | `([ : $stop]) => `({ stop := $stop, step_pos := Nat.zero_lt_one : Range }) + | `([ $start : $stop ]) => `({ start := $start, stop := $stop, step_pos := Nat.zero_lt_one : Range }) + | `([ $start : $stop : $step ]) => `({ start := $start, stop := $stop, step := $step, step_pos := by decide : Range }) + | `([ : $stop : $step ]) => `({ stop := $stop, step := $step, step_pos := by decide : Range }) + +end Range +end Std + +theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop := h.2.1 + +theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i := h.1 + +theorem Membership.mem.step {i : Nat} {r : Std.Range} (h : i ∈ r) : (i - r.start) % r.step = 0 := h.2.2 + +theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) : + i < n := h₂ ▸ h₁.2.1 + +macro_rules + | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Membership.get_elem_helper; assumption; rfl) diff --git a/src/Init/Data/Range/Lemmas.lean b/src/Init/Data/Range/Lemmas.lean new file mode 100644 index 0000000000..bc9c07c23c --- /dev/null +++ b/src/Init/Data/Range/Lemmas.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +prelude +import Init.Data.Range.Basic +import Init.Data.List.Range +import Init.Data.List.Monadic +import Init.Data.Nat.Div.Lemmas + +/-! +# Lemmas about `Std.Range` + +We provide lemmas rewriting for loops over `Std.Range` in terms of `List.range'`. +-/ + +namespace Std.Range + +/-- Generalization of `mem_of_mem_range'` used in `forIn'_loop_eq_forIn'_range'` below. -/ +private theorem mem_of_mem_range'_aux {r : Range} {a : Nat} (w₁ : (i - r.start) % r.step = 0) + (w₂ : r.start ≤ i) + (h : a ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) : a ∈ r := by + obtain ⟨j, h', rfl⟩ := List.mem_range'.1 h + refine ⟨by omega, ?_⟩ + rw [Nat.lt_div_iff_mul_lt r.step_pos, Nat.mul_comm] at h' + constructor + · omega + · rwa [Nat.add_comm, Nat.add_sub_assoc w₂, Nat.mul_add_mod_self_left] + +theorem mem_of_mem_range' {r : Range} (h : x ∈ List.range' r.start r.size r.step) : x ∈ r := by + unfold size at h + apply mem_of_mem_range'_aux (by simp) (by simp) h + +private theorem size_eq (r : Std.Range) (h : i < r.stop) : + (r.stop - i + r.step - 1) / r.step = + (r.stop - (i + r.step) + r.step - 1) / r.step + 1 := by + have w := r.step_pos + if i + r.step < r.stop then -- Not sure this case split is strictly necessary. + rw [Nat.div_eq_iff w, Nat.add_one_mul] + have : (r.stop - (i + r.step) + r.step - 1) / r.step * r.step ≤ + (r.stop - (i + r.step) + r.step - 1) := Nat.div_mul_le_self _ _ + have : r.stop - (i + r.step) + r.step - 1 - r.step < + (r.stop - (i + r.step) + r.step - 1) / r.step * r.step := + Nat.lt_div_mul_self w (by omega) + omega + else + have : (r.stop - i + r.step - 1) / r.step = 1 := by + rw [Nat.div_eq_iff w, Nat.one_mul] + omega + have : (r.stop - (i + r.step) + r.step - 1) / r.step = 0 := by + rw [Nat.div_eq_iff] <;> omega + omega + +private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Std.Range) + (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) (i) (w₁) (w₂) : + forIn'.loop r f init i w₁ w₂ = + forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init + fun a h => f a (mem_of_mem_range'_aux w₁ w₂ h) := by + have w := r.step_pos + rw [forIn'.loop] + split <;> rename_i h + · simp only [size_eq r h, List.range'_succ, List.forIn'_cons] + congr 1 + funext step + split + · simp + · rw [forIn'_loop_eq_forIn'_range'] + · have : (r.stop - i + r.step - 1) / r.step = 0 := by + rw [Nat.div_eq_iff] <;> omega + simp [this] + +theorem forIn'_eq_forIn'_range' [Monad m] (r : Std.Range) + (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) : + forIn' r init f = + forIn' (List.range' r.start r.size r.step) init (fun a h => f a (mem_of_mem_range' h)) := by + conv => lhs; simp only [forIn', Range.forIn'] + simp only [size] + rw [forIn'_loop_eq_forIn'_range'] + +theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range) + (init : β) (f : Nat → β → m (ForInStep β)) : + forIn r init f = forIn (List.range' r.start r.size r.step) init f := by + simp only [forIn, forIn'_eq_forIn'_range'] + +private theorem forM_loop_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) : + forM.loop r f i = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f := by + have w := r.step_pos + rw [forM.loop] + split <;> rename_i h + · simp [size_eq r h, List.range'_succ, List.forM_cons] + congr 1 + funext + rw [forM_loop_eq_forM_range'] + · have : (r.stop - i + r.step - 1) / r.step = 0 := by + rw [Nat.div_eq_iff] <;> omega + simp [this] + +theorem forM_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) : + forM r f = forM (List.range' r.start r.size r.step) f := by + simp only [forM, Range.forM, forM_loop_eq_forM_range', size] + +end Std.Range diff --git a/tests/lean/run/nat_mod_defeq.lean b/tests/lean/run/nat_mod_defeq.lean index c36d59e87d..f49f11e432 100644 --- a/tests/lean/run/nat_mod_defeq.lean +++ b/tests/lean/run/nat_mod_defeq.lean @@ -1,5 +1,3 @@ -import Init.Data.Nat.Div - /-! This tests that `0 : Fin (n + 1)` unfolds to `0 : Nat`, which is a property kept for backwards compatibility with mathlib in Lean 3.