From eebdfdf87ae09188d857b4928df89e40a3034047 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 14 Feb 2024 16:18:41 -0800 Subject: [PATCH] chore: upstream of Std.Data.Nat.Init (#3331) --- src/Init/Data/Nat.lean | 2 + src/Init/Data/Nat/Basic.lean | 216 +++++++++++++++++++++--------- src/Init/Data/Nat/Div.lean | 133 ++++++++++++++++++ src/Init/Data/Nat/Dvd.lean | 96 +++++++++++++ src/Init/Data/Nat/Gcd.lean | 33 ++++- src/Init/Data/Nat/Linear.lean | 4 +- src/Init/Data/Nat/MinMax.lean | 51 +++++++ src/Init/Data/Nat/Power2.lean | 2 + src/Init/Prelude.lean | 5 + src/Init/PropLemmas.lean | 6 - tests/lean/run/1380.lean | 1 - tests/lean/run/simproc_panic.lean | 7 - 12 files changed, 475 insertions(+), 81 deletions(-) create mode 100644 src/Init/Data/Nat/Dvd.lean create mode 100644 src/Init/Data/Nat/MinMax.lean diff --git a/src/Init/Data/Nat.lean b/src/Init/Data/Nat.lean index 5d71ac093b..daf9ea0707 100644 --- a/src/Init/Data/Nat.lean +++ b/src/Init/Data/Nat.lean @@ -6,7 +6,9 @@ Authors: Leonardo de Moura prelude import Init.Data.Nat.Basic import Init.Data.Nat.Div +import Init.Data.Nat.Dvd import Init.Data.Nat.Gcd +import Init.Data.Nat.MinMax import Init.Data.Nat.Bitwise import Init.Data.Nat.Control import Init.Data.Nat.Log2 diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 78856c3bf6..9f4d592f36 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -154,6 +154,13 @@ protected theorem add_right_cancel {n m k : Nat} (h : n + m = k + m) : n = k := rw [Nat.add_comm n m, Nat.add_comm k m] at h apply Nat.add_left_cancel h +theorem eq_zero_of_add_eq_zero : ∀ {n m}, n + m = 0 → n = 0 ∧ m = 0 + | 0, 0, _ => ⟨rfl, rfl⟩ + | _+1, 0, h => Nat.noConfusion h + +protected theorem eq_zero_of_add_eq_zero_left (h : n + m = 0) : m = 0 := + (Nat.eq_zero_of_add_eq_zero h).2 + /-! # Nat.mul theorems -/ @[simp] protected theorem mul_zero (n : Nat) : n * 0 = 0 := @@ -206,16 +213,13 @@ protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by attribute [simp] Nat.le_refl -theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m := - succ_le_succ +theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m := succ_le_succ -theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := - succ_le_succ +theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ -@[simp] protected theorem sub_zero (n : Nat) : n - 0 = n := - rfl +@[simp] protected theorem sub_zero (n : Nat) : n - 0 = n := rfl -theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by +@[simp] theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by induction m with | zero => exact rfl | succ m ih => apply congrArg pred ih @@ -241,8 +245,7 @@ theorem sub_lt : ∀ {n m : Nat}, 0 < n → 0 < m → n - m < n show n - m < succ n from lt_succ_of_le (sub_le n m) -theorem sub_succ (n m : Nat) : n - succ m = pred (n - m) := - rfl +theorem sub_succ (n m : Nat) : n - succ m = pred (n - m) := rfl theorem succ_sub_succ (n m : Nat) : succ n - succ m = n - m := succ_sub_succ_eq_sub n m @@ -277,20 +280,24 @@ instance : Trans (. ≤ . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop) protected theorem le_of_eq {n m : Nat} (p : n = m) : n ≤ m := p ▸ Nat.le_refl n -theorem le_of_succ_le {n m : Nat} (h : succ n ≤ m) : n ≤ m := - Nat.le_trans (le_succ n) h - -protected theorem le_of_lt {n m : Nat} (h : n < m) : n ≤ m := - le_of_succ_le h - theorem lt.step {n m : Nat} : n < m → n < succ m := le_step +theorem le_of_succ_le {n m : Nat} (h : succ n ≤ m) : n ≤ m := Nat.le_trans (le_succ n) h +theorem lt_of_succ_lt {n m : Nat} : succ n < m → n < m := le_of_succ_le +protected theorem le_of_lt {n m : Nat} : n < m → n ≤ m := le_of_succ_le + +theorem lt_of_succ_lt_succ {n m : Nat} : succ n < succ m → n < m := le_of_succ_le_succ + +theorem lt_of_succ_le {n m : Nat} (h : succ n ≤ m) : n < m := h +theorem succ_le_of_lt {n m : Nat} (h : n < m) : succ n ≤ m := h + theorem eq_zero_or_pos : ∀ (n : Nat), n = 0 ∨ n > 0 | 0 => Or.inl rfl | _+1 => Or.inr (succ_pos _) -theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n) +protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_pos n).resolve_left +theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n) theorem lt_succ_self (n : Nat) : n < succ n := lt.base n protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m := @@ -298,20 +305,7 @@ protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m := | Or.inl h => Or.inl (Nat.le_of_lt h) | Or.inr h => Or.inr h -theorem eq_zero_of_le_zero {n : Nat} (h : n ≤ 0) : n = 0 := - Nat.le_antisymm h (zero_le _) - -theorem lt_of_succ_lt {n m : Nat} : succ n < m → n < m := - le_of_succ_le - -theorem lt_of_succ_lt_succ {n m : Nat} : succ n < succ m → n < m := - le_of_succ_le_succ - -theorem lt_of_succ_le {n m : Nat} (h : succ n ≤ m) : n < m := - h - -theorem succ_le_of_lt {n m : Nat} (h : n < m) : succ n ≤ m := - h +theorem eq_zero_of_le_zero {n : Nat} (h : n ≤ 0) : n = 0 := Nat.le_antisymm h (zero_le _) theorem zero_lt_of_lt : {a b : Nat} → a < b → 0 < b | 0, _, h => h @@ -326,8 +320,7 @@ theorem zero_lt_of_ne_zero {a : Nat} (h : a ≠ 0) : 0 < a := by attribute [simp] Nat.lt_irrefl -theorem ne_of_lt {a b : Nat} (h : a < b) : a ≠ b := - fun he => absurd (he ▸ h) (Nat.lt_irrefl a) +theorem ne_of_lt {a b : Nat} (h : a < b) : a ≠ b := fun he => absurd (he ▸ h) (Nat.lt_irrefl a) theorem le_or_eq_of_le_succ {m n : Nat} (h : m ≤ succ n) : m ≤ n ∨ m = succ n := Decidable.byCases @@ -363,16 +356,51 @@ protected theorem not_le_of_gt {n m : Nat} (h : n > m) : ¬ n ≤ m := fun h₁ | Or.inr h₂ => have Heq : n = m := Nat.le_antisymm h₁ h₂ absurd (@Eq.subst _ _ _ _ Heq h) (Nat.lt_irrefl m) +protected theorem not_le_of_lt : ∀{a b : Nat}, a < b → ¬(b ≤ a) := Nat.not_le_of_gt +protected theorem not_lt_of_ge : ∀{a b : Nat}, b ≥ a → ¬(b < a) := flip Nat.not_le_of_gt +protected theorem not_lt_of_le : ∀{a b : Nat}, a ≤ b → ¬(b < a) := flip Nat.not_le_of_gt +protected theorem lt_le_asymm : ∀{a b : Nat}, a < b → ¬(b ≤ a) := Nat.not_le_of_gt +protected theorem le_lt_asymm : ∀{a b : Nat}, a ≤ b → ¬(b < a) := flip Nat.not_le_of_gt -theorem gt_of_not_le {n m : Nat} (h : ¬ n ≤ m) : n > m := - match Nat.lt_or_ge m n with - | Or.inl h₁ => h₁ - | Or.inr h₁ => absurd h₁ h +theorem gt_of_not_le {n m : Nat} (h : ¬ n ≤ m) : n > m := (Nat.lt_or_ge m n).resolve_right h +protected theorem lt_of_not_ge : ∀{a b : Nat}, ¬(b ≥ a) → b < a := Nat.gt_of_not_le +protected theorem lt_of_not_le : ∀{a b : Nat}, ¬(a ≤ b) → b < a := Nat.gt_of_not_le -theorem ge_of_not_lt {n m : Nat} (h : ¬ n < m) : n ≥ m := - match Nat.lt_or_ge n m with - | Or.inl h₁ => absurd h₁ h - | Or.inr h₁ => h₁ +theorem ge_of_not_lt {n m : Nat} (h : ¬ n < m) : n ≥ m := (Nat.lt_or_ge n m).resolve_left h +protected theorem le_of_not_gt : ∀{a b : Nat}, ¬(b > a) → b ≤ a := Nat.ge_of_not_lt +protected theorem le_of_not_lt : ∀{a b : Nat}, ¬(a < b) → b ≤ a := Nat.ge_of_not_lt + +theorem ne_of_gt {a b : Nat} (h : b < a) : a ≠ b := (ne_of_lt h).symm +protected theorem ne_of_lt' : ∀{a b : Nat}, a < b → b ≠ a := ne_of_gt + +@[simp] protected theorem not_le {a b : Nat} : ¬ a ≤ b ↔ b < a := + Iff.intro Nat.gt_of_not_le Nat.not_le_of_gt +@[simp] protected theorem not_lt {a b : Nat} : ¬ a < b ↔ b ≤ a := + Iff.intro Nat.ge_of_not_lt (flip Nat.not_le_of_gt) + +protected theorem le_of_not_le {a b : Nat} (h : ¬ b ≤ a) : a ≤ b := Nat.le_of_lt (Nat.not_le.1 h) +protected theorem le_of_not_ge : ∀{a b : Nat}, ¬(a ≥ b) → a ≤ b:= @Nat.le_of_not_le + +protected theorem lt_trichotomy (a b : Nat) : a < b ∨ a = b ∨ b < a := + match Nat.lt_or_ge a b with + | .inl h => .inl h + | .inr h => + match Nat.eq_or_lt_of_le h with + | .inl h => .inr (.inl h.symm) + | .inr h => .inr (.inr h) + +protected theorem lt_or_gt_of_ne {a b : Nat} (ne : a ≠ b) : a < b ∨ a > b := + match Nat.lt_trichotomy a b with + | .inl h => .inl h + | .inr (.inl e) => False.elim (ne e) + | .inr (.inr h) => .inr h + +protected theorem lt_or_lt_of_ne : ∀{a b : Nat}, a ≠ b → a < b ∨ b < a := Nat.lt_or_gt_of_ne + +protected theorem le_antisymm_iff {a b : Nat} : a = b ↔ a ≤ b ∧ b ≤ a := + Iff.intro (fun p => And.intro (Nat.le_of_eq p) (Nat.le_of_eq p.symm)) + (fun ⟨hle, hge⟩ => Nat.le_antisymm hle hge) +protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤ a := @Nat.le_antisymm_iff instance : Antisymm ( . ≤ . : Nat → Nat → Prop) where antisymm h₁ h₂ := Nat.le_antisymm h₁ h₂ @@ -401,6 +429,8 @@ protected theorem add_lt_add_right {n m : Nat} (h : n < m) (k : Nat) : n + k < m protected theorem zero_lt_one : 0 < (1:Nat) := zero_lt_succ 0 +protected theorem pos_iff_ne_zero : 0 < n ↔ n ≠ 0 := ⟨ne_of_gt, Nat.pos_of_ne_zero⟩ + theorem add_le_add {a b c d : Nat} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d := Nat.le_trans (Nat.add_le_add_right h₁ c) (Nat.add_le_add_left h₂ b) @@ -418,6 +448,9 @@ protected theorem le_of_add_le_add_right {a b c : Nat} : a + b ≤ c + b → a rw [Nat.add_comm _ b, Nat.add_comm _ b] apply Nat.le_of_add_le_add_left +protected theorem add_le_add_iff_right {n : Nat} : m + n ≤ k + n ↔ m ≤ k := + ⟨Nat.le_of_add_le_add_right, fun h => Nat.add_le_add_right h _⟩ + /-! # Basic theorems for comparing numerals -/ theorem ctor_eq_zero : Nat.zero = 0 := @@ -527,7 +560,20 @@ theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by theorem pred_lt' {n m : Nat} (h : m < n) : pred n < n := pred_lt (not_eq_zero_of_lt h) -/-! # sub/pred theorems -/ +/-! # pred theorems -/ + +@[simp] protected theorem pred_zero : pred 0 = 0 := rfl +@[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl + +theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by + induction a with + | zero => contradiction + | succ => rfl + +theorem succ_pred_eq_of_pos : ∀ {n}, 0 < n → succ (pred n) = n + | _+1, _ => rfl + +/-! # sub theorems -/ theorem add_sub_self_left (a b : Nat) : (a + b) - a = b := by induction a with @@ -561,11 +607,6 @@ theorem sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - i := by apply Nat.zero_lt_sub_of_lt assumption -theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by - induction a with - | zero => contradiction - | succ => rfl - theorem sub_ne_zero_of_lt : {a b : Nat} → a < b → b - a ≠ 0 | 0, 0, h => absurd h (Nat.lt_irrefl 0) | 0, succ b, _ => by simp @@ -591,7 +632,7 @@ protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m := protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m := by rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right] -protected theorem add_sub_cancel (n m : Nat) : n + m - m = n := +@[simp] protected theorem add_sub_cancel (n m : Nat) : n + m - m = n := suffices n + m - (0 + m) = n by rw [Nat.zero_add] at this; assumption by rw [Nat.add_sub_add_right, Nat.sub_zero] @@ -680,12 +721,6 @@ theorem lt_sub_of_add_lt {a b c : Nat} (h : a + b < c) : a < c - b := have : a.succ + b ≤ c := by simp [Nat.succ_add]; exact h le_sub_of_add_le this -@[simp] protected theorem pred_zero : pred 0 = 0 := - rfl - -@[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n := - rfl - theorem sub.elim {motive : Nat → Prop} (x y : Nat) (h₁ : y ≤ x → (k : Nat) → x = y + k → motive k) @@ -695,19 +730,76 @@ theorem sub.elim {motive : Nat → Prop} | inl hlt => rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hlt)]; exact h₂ hlt | inr hle => exact h₁ hle (x - y) (Nat.add_sub_of_le hle).symm -theorem mul_pred_left (n m : Nat) : pred n * m = n * m - m := by - cases n with - | zero => simp - | succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel] +theorem succ_sub {m n : Nat} (h : n ≤ m) : succ m - n = succ (m - n) := by + let ⟨k, hk⟩ := Nat.le.dest h + rw [← hk, Nat.add_sub_cancel_left, ← add_succ, Nat.add_sub_cancel_left] -theorem mul_pred_right (n m : Nat) : n * pred m = n * m - n := by - rw [Nat.mul_comm, mul_pred_left, Nat.mul_comm] +protected theorem sub_pos_of_lt (h : m < n) : 0 < n - m := + Nat.pos_iff_ne_zero.2 (Nat.sub_ne_zero_of_lt h) protected theorem sub_sub (n m k : Nat) : n - m - k = n - (m + k) := by induction k with | zero => simp | succ k ih => rw [Nat.add_succ, Nat.sub_succ, Nat.sub_succ, ih] +protected theorem sub_le_sub_left (h : n ≤ m) (k : Nat) : k - m ≤ k - n := + match m, le.dest h with + | _, ⟨a, rfl⟩ => by rw [← Nat.sub_sub]; apply sub_le + +protected theorem sub_le_sub_right {n m : Nat} (h : n ≤ m) : ∀ k, n - k ≤ m - k + | 0 => h + | z+1 => pred_le_pred (Nat.sub_le_sub_right h z) + +protected theorem lt_of_sub_ne_zero (h : n - m ≠ 0) : m < n := + Nat.not_le.1 (mt Nat.sub_eq_zero_of_le h) + +protected theorem sub_ne_zero_iff_lt : n - m ≠ 0 ↔ m < n := + ⟨Nat.lt_of_sub_ne_zero, Nat.sub_ne_zero_of_lt⟩ + +protected theorem lt_of_sub_pos (h : 0 < n - m) : m < n := + Nat.lt_of_sub_ne_zero (Nat.pos_iff_ne_zero.1 h) + +protected theorem lt_of_sub_eq_succ (h : m - n = succ l) : n < m := + Nat.lt_of_sub_pos (h ▸ Nat.zero_lt_succ _) + +protected theorem sub_lt_left_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < n + m) : k - n < m := by + have := Nat.sub_le_sub_right (succ_le_of_lt h) n + rwa [Nat.add_sub_cancel_left, Nat.succ_sub H] at this + +protected theorem sub_lt_right_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < m + n) : k - n < m := + Nat.sub_lt_left_of_lt_add H (Nat.add_comm .. ▸ h) + +protected theorem le_of_sub_eq_zero : ∀ {n m}, n - m = 0 → n ≤ m + | 0, _, _ => Nat.zero_le .. + | _+1, _+1, h => Nat.succ_le_succ <| Nat.le_of_sub_eq_zero (Nat.succ_sub_succ .. ▸ h) + +protected theorem le_of_sub_le_sub_right : ∀ {n m k : Nat}, k ≤ m → n - k ≤ m - k → n ≤ m + | 0, _, _, _, _ => Nat.zero_le .. + | _+1, _, 0, _, h₁ => h₁ + | _+1, _+1, _+1, h₀, h₁ => by + simp only [Nat.succ_sub_succ] at h₁ + exact succ_le_succ <| Nat.le_of_sub_le_sub_right (le_of_succ_le_succ h₀) h₁ + +protected theorem sub_le_sub_iff_right {n : Nat} (h : k ≤ m) : n - k ≤ m - k ↔ n ≤ m := + ⟨Nat.le_of_sub_le_sub_right h, fun h => Nat.sub_le_sub_right h _⟩ + +protected theorem sub_eq_iff_eq_add {c : Nat} (h : b ≤ a) : a - b = c ↔ a = c + b := + ⟨fun | rfl => by rw [Nat.sub_add_cancel h], fun heq => by rw [heq, Nat.add_sub_cancel]⟩ + +protected theorem sub_eq_iff_eq_add' {c : Nat} (h : b ≤ a) : a - b = c ↔ a = b + c := by + rw [Nat.add_comm, Nat.sub_eq_iff_eq_add h] + +theorem mul_pred_left (n m : Nat) : pred n * m = n * m - m := by + cases n with + | zero => simp + | succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel] + +/-! ## Mul sub distrib -/ + +theorem mul_pred_right (n m : Nat) : n * pred m = n * m - n := by + rw [Nat.mul_comm, mul_pred_left, Nat.mul_comm] + + protected theorem mul_sub_right_distrib (n m k : Nat) : (n - m) * k = n * k - m * k := by induction m with | zero => simp @@ -719,14 +811,12 @@ protected theorem mul_sub_left_distrib (n m k : Nat) : n * (m - k) = n * m - n * /-! # Helper normalization theorems -/ theorem not_le_eq (a b : Nat) : (¬ (a ≤ b)) = (b + 1 ≤ a) := - propext <| Iff.intro (fun h => Nat.gt_of_not_le h) (fun h => Nat.not_le_of_gt h) - + Eq.propIntro Nat.gt_of_not_le Nat.not_le_of_gt theorem not_ge_eq (a b : Nat) : (¬ (a ≥ b)) = (a + 1 ≤ b) := not_le_eq b a theorem not_lt_eq (a b : Nat) : (¬ (a < b)) = (b ≤ a) := - propext <| Iff.intro (fun h => have h := Nat.succ_le_of_lt (Nat.gt_of_not_le h); Nat.le_of_succ_le_succ h) (fun h => Nat.not_le_of_gt (Nat.succ_le_succ h)) - + Eq.propIntro Nat.le_of_not_lt Nat.not_lt_of_le theorem not_gt_eq (a b : Nat) : (¬ (a > b)) = (a ≤ b) := not_lt_eq b a diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean index 31fe788f17..94ba1f7209 100644 --- a/src/Init/Data/Nat/Div.lean +++ b/src/Init/Data/Nat/Div.lean @@ -7,6 +7,7 @@ prelude import Init.WF import Init.WFTactics import Init.Data.Nat.Basic + namespace Nat theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x := @@ -174,4 +175,136 @@ theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by 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] + +@[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 [not_succ_le_zero x, succ_mul, Nat.add_comm] + refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_right ..) + exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩ + | ind y k h IH => + rw [← add_one, 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] + +theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m + | m, 0 => by simp + | m, n+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 = succ (x / z) := 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 = succ (x / z) := 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 < succ k * 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 [add_one, Nat.pred_succ, mul_succ, Nat.sub_sub] + +theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := 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.strongInductionOn 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 + end Nat diff --git a/src/Init/Data/Nat/Dvd.lean b/src/Init/Data/Nat/Dvd.lean new file mode 100644 index 0000000000..b6507a06fd --- /dev/null +++ b/src/Init/Data/Nat/Dvd.lean @@ -0,0 +1,96 @@ +prelude +import Init.Data.Nat.Div + +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) + +protected theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩ + +protected theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩ + +protected theorem dvd_mul_left (a b : Nat) : a ∣ b * a := ⟨b, Nat.mul_comm b a⟩ +protected theorem dvd_mul_right (a b : Nat) : a ∣ a * b := ⟨b, rfl⟩ + +protected theorem dvd_trans {a b c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c := + match h₁, h₂ with + | ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ => + ⟨d * e, show c = a * (d * e) by simp[h₃,h₄, Nat.mul_assoc]⟩ + +protected theorem eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) : a = 0 := + let ⟨c, H'⟩ := h; H'.trans c.zero_mul + +@[simp] protected theorem zero_dvd {n : Nat} : 0 ∣ n ↔ n = 0 := + ⟨Nat.eq_zero_of_zero_dvd, fun h => h.symm ▸ Nat.dvd_zero 0⟩ + +protected theorem dvd_add {a b c : Nat} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c := + let ⟨d, hd⟩ := h₁; let ⟨e, he⟩ := h₂; ⟨d + e, by simp [Nat.left_distrib, hd, he]⟩ + +protected theorem dvd_add_iff_right {k m n : Nat} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n := + ⟨Nat.dvd_add h, + match m, h with + | _, ⟨d, rfl⟩ => fun ⟨e, he⟩ => + ⟨e - d, by rw [Nat.mul_sub_left_distrib, ← he, Nat.add_sub_cancel_left]⟩⟩ + +protected theorem dvd_add_iff_left {k m n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n := by + rw [Nat.add_comm]; exact Nat.dvd_add_iff_right h + +theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m := + have := Nat.dvd_add_iff_left <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n) + by rwa [mod_add_div] at this + +theorem le_of_dvd {m n : Nat} (h : 0 < n) : m ∣ n → m ≤ n + | ⟨k, e⟩ => by + revert h + rw [e] + match k with + | 0 => intro hn; simp at hn + | pk+1 => + intro + have := Nat.mul_le_mul_left m (succ_pos pk) + rwa [Nat.mul_one] at this + +protected theorem dvd_antisymm : ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n + | _, 0, _, h₂ => Nat.eq_zero_of_zero_dvd h₂ + | 0, _, h₁, _ => (Nat.eq_zero_of_zero_dvd h₁).symm + | _+1, _+1, h₁, h₂ => Nat.le_antisymm (le_of_dvd (succ_pos _) h₁) (le_of_dvd (succ_pos _) h₂) + +theorem pos_of_dvd_of_pos {m n : Nat} (H1 : m ∣ n) (H2 : 0 < n) : 0 < m := + Nat.pos_of_ne_zero fun m0 => Nat.ne_of_gt H2 <| Nat.eq_zero_of_zero_dvd (m0 ▸ H1) + +@[simp] protected theorem one_dvd (n : Nat) : 1 ∣ n := ⟨n, n.one_mul.symm⟩ + +theorem eq_one_of_dvd_one {n : Nat} (H : n ∣ 1) : n = 1 := Nat.dvd_antisymm H n.one_dvd + +theorem mod_eq_zero_of_dvd {m n : Nat} (H : m ∣ n) : n % m = 0 := by + let ⟨z, H⟩ := H; rw [H, mul_mod_right] + +theorem dvd_of_mod_eq_zero {m n : Nat} (H : n % m = 0) : m ∣ n := by + exists n / m + have := (mod_add_div n m).symm + rwa [H, Nat.zero_add] at this + +theorem dvd_iff_mod_eq_zero (m n : Nat) : m ∣ n ↔ n % m = 0 := + ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩ + +instance decidable_dvd : @DecidableRel Nat (·∣·) := + fun _ _ => decidable_of_decidable_of_iff (dvd_iff_mod_eq_zero _ _).symm + +theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a ∣ b) : 0 < b % a := by + rw [dvd_iff_mod_eq_zero] at h + exact Nat.pos_of_ne_zero h + + +protected theorem mul_div_cancel' {n m : Nat} (H : n ∣ m) : n * (m / n) = m := by + have := mod_add_div m n + rwa [mod_eq_zero_of_dvd H, Nat.zero_add] at this + +protected theorem div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m := by + rw [Nat.mul_comm, Nat.mul_div_cancel' H] + +end Nat diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean index 68943ad995..cb66f767fb 100644 --- a/src/Init/Data/Nat/Gcd.lean +++ b/src/Init/Data/Nat/Gcd.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import Init.Data.Nat.Div +import Init.Data.Nat.Dvd namespace Nat @@ -38,4 +38,35 @@ theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := @[simp] theorem gcd_self (n : Nat) : gcd n n = n := by cases n <;> simp [gcd_succ] +theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m := + match m with + | 0 => by have := (mod_zero n).symm; rwa [gcd_zero_right] + | _ + 1 => by simp [gcd_succ] + +@[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat) + (H0 : ∀n, P 0 n) (H1 : ∀ m n, 0 < m → P (n % m) m → P m n) : P m n := + Nat.strongInductionOn (motive := fun m => ∀ n, P m n) m + (fun + | 0, _ => H0 + | _+1, IH => fun _ => H1 _ _ (succ_pos _) (IH _ (mod_lt _ (succ_pos _)) _) ) + n + +theorem gcd_dvd (m n : Nat) : (gcd m n ∣ m) ∧ (gcd m n ∣ n) := by + induction m, n using gcd.induction with + | H0 n => rw [gcd_zero_left]; exact ⟨Nat.dvd_zero n, Nat.dvd_refl n⟩ + | H1 m n _ IH => rw [← gcd_rec] at IH; exact ⟨IH.2, (dvd_mod_iff IH.2).1 IH.1⟩ + +theorem gcd_dvd_left (m n : Nat) : gcd m n ∣ m := (gcd_dvd m n).left + +theorem gcd_dvd_right (m n : Nat) : gcd m n ∣ n := (gcd_dvd m n).right + +theorem gcd_le_left (n) (h : 0 < m) : gcd m n ≤ m := le_of_dvd h <| gcd_dvd_left m n + +theorem gcd_le_right (n) (h : 0 < n) : gcd m n ≤ n := le_of_dvd h <| gcd_dvd_right m n + +theorem dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n := by + induction m, n using gcd.induction with intro km kn + | H0 n => rw [gcd_zero_left]; exact kn + | H1 n m _ IH => rw [gcd_rec]; exact IH ((dvd_mod_iff km).2 kn) km + end Nat diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean index 35c98eaa62..a12fcec997 100644 --- a/src/Init/Data/Nat/Linear.lean +++ b/src/Init/Data/Nat/Linear.lean @@ -642,9 +642,7 @@ theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsa | Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this] · intro ⟨h₁, h₂⟩ simp [Poly.of_isZero, h₂] - have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁) - simp [this] - done + exact Poly.of_isNonZero ctx h₁ theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid → c.denote ctx = True := by cases c; rename_i eq lhs rhs diff --git a/src/Init/Data/Nat/MinMax.lean b/src/Init/Data/Nat/MinMax.lean new file mode 100644 index 0000000000..c68fce134d --- /dev/null +++ b/src/Init/Data/Nat/MinMax.lean @@ -0,0 +1,51 @@ +prelude +import Init.ByCases + +namespace Nat + +/-! # min lemmas -/ + +protected theorem min_eq_min (a : Nat) : Nat.min a b = min a b := rfl + +protected theorem min_comm (a b : Nat) : min a b = min b a := by + match Nat.lt_trichotomy a b with + | .inl h => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt] + | .inr (.inl h) => simp [Nat.min_def, h] + | .inr (.inr h) => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt] + +protected theorem min_le_right (a b : Nat) : min a b ≤ b := by + by_cases (a <= b) <;> simp [Nat.min_def, *] +protected theorem min_le_left (a b : Nat) : min a b ≤ a := + Nat.min_comm .. ▸ Nat.min_le_right .. + +protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := if_pos h +protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b := + Nat.min_comm .. ▸ Nat.min_eq_left h + +protected theorem le_min_of_le_of_le {a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c := by + intros; cases Nat.le_total b c with + | inl h => rw [Nat.min_eq_left h]; assumption + | inr h => rw [Nat.min_eq_right h]; assumption + +protected theorem le_min {a b c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c := + ⟨fun h => ⟨Nat.le_trans h (Nat.min_le_left ..), Nat.le_trans h (Nat.min_le_right ..)⟩, + fun ⟨h₁, h₂⟩ => Nat.le_min_of_le_of_le h₁ h₂⟩ + +protected theorem lt_min {a b c : Nat} : a < min b c ↔ a < b ∧ a < c := Nat.le_min + +/-! # max lemmas -/ + +protected theorem max_eq_max (a : Nat) : Nat.max a b = max a b := rfl + +protected theorem max_comm (a b : Nat) : max a b = max b a := by + simp only [Nat.max_def] + by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂] + · exact Nat.le_antisymm h₂ h₁ + · cases not_or_intro h₁ h₂ <| Nat.le_total .. + +protected theorem le_max_left ( a b : Nat) : a ≤ max a b := by + by_cases (a <= b) <;> simp [Nat.max_def, *] +protected theorem le_max_right (a b : Nat) : b ≤ max a b := + Nat.max_comm .. ▸ Nat.le_max_left .. + +end Nat diff --git a/src/Init/Data/Nat/Power2.lean b/src/Init/Data/Nat/Power2.lean index 46b1b29599..287e4dfdbf 100644 --- a/src/Init/Data/Nat/Power2.lean +++ b/src/Init/Data/Nat/Power2.lean @@ -8,6 +8,8 @@ import Init.Data.Nat.Linear namespace Nat +protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide) + theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by have : power * 2 = power + power := by simp_arith rw [this, Nat.sub_add_eq] diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 5d5a73e2cc..0c21db5447 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -548,6 +548,11 @@ theorem Or.elim {c : Prop} (h : Or a b) (left : a → c) (right : b → c) : c : | Or.inl h => left h | Or.inr h => right h +theorem Or.resolve_left (h: Or a b) (na : Not a) : b := h.elim (absurd · na) id +theorem Or.resolve_right (h: Or a b) (nb : Not b) : a := h.elim id (absurd · nb) +theorem Or.neg_resolve_left (h : Or (Not a) b) (ha : a) : b := h.elim (absurd ha) id +theorem Or.neg_resolve_right (h : Or a (Not b)) (nb : b) : a := h.elim id (absurd nb) + /-- `Bool` is the type of boolean values, `true` and `false`. Classically, this is equivalent to `Prop` (the type of propositions), but the distinction diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index b0b4b08a18..e773b7dc26 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -59,12 +59,6 @@ theorem and_iff_right (ha : a) : a ∧ b ↔ b := Iff.intro And.right (And.intro theorem or_self_iff : a ∨ a ↔ a := or_self _ ▸ .rfl theorem not_or_intro {a b : Prop} (ha : ¬a) (hb : ¬b) : ¬(a ∨ b) := (·.elim ha hb) -theorem Or.resolve_left (h: a ∨ b) (na : ¬a) : b := h.elim (absurd · na) id -theorem Or.resolve_right (h: a ∨ b) (nb : ¬b) : a := h.elim id (absurd · nb) - -theorem Or.neg_resolve_left (h : ¬a ∨ b) (ha : a) : b := h.elim (absurd ha) id -theorem Or.neg_resolve_right (h : a ∨ ¬b) (nb : b) : a := h.elim id (absurd nb) - theorem or_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := ⟨.imp h₁.mp h₂.mp, .imp h₁.mpr h₂.mpr⟩ theorem or_congr_left (h : a ↔ b) : a ∨ c ↔ b ∨ c := or_congr h .rfl theorem or_congr_right (h : b ↔ c) : a ∨ b ↔ a ∨ c := or_congr .rfl h diff --git a/tests/lean/run/1380.lean b/tests/lean/run/1380.lean index 248837b855..2cd3161654 100644 --- a/tests/lean/run/1380.lean +++ b/tests/lean/run/1380.lean @@ -1,4 +1,3 @@ -theorem Nat.ne_of_gt {a b : Nat} (h : a < b) : b ≠ a := sorry theorem Nat.lt_succ_iff {m n : Nat} : m < succ n ↔ m ≤ n := sorry variable (n v₁ v₂) (hv₁: v₁ < n + 1) (hv₂: v₂ < n + 1) diff --git a/tests/lean/run/simproc_panic.lean b/tests/lean/run/simproc_panic.lean index 9215c6eb15..eafdef2c7f 100644 --- a/tests/lean/run/simproc_panic.lean +++ b/tests/lean/run/simproc_panic.lean @@ -1,13 +1,6 @@ -- Extracted from Mathlib.Data.UnionFind. -- This file was failing in Mathlib during development of #3124. -section Std.Data.Nat.Init.Lemmas - -protected theorem Nat.le_max_left (a b : Nat) : a ≤ max a b := sorry -protected theorem Nat.le_max_right (a b : Nat) : b ≤ max a b := sorry - -end Std.Data.Nat.Init.Lemmas - section Std.Data.Nat.Lemmas protected theorem Nat.lt_or_eq_of_le {n m : Nat} (h : n ≤ m) : n < m ∨ n = m := sorry