From 1cf71e54cf268e87cf5c43c830d953f5c88e6c39 Mon Sep 17 00:00:00 2001 From: Markus Schmaus Date: Mon, 17 Jun 2024 07:35:32 +0200 Subject: [PATCH] feat: add missing theorems for `+ 1` and `- 1` normal form (#4242) `Nat.succ_eq_add_one` and `Nat.pred_eq_sub_one` are now simp lemmas. For theorems about `Nat.succ` or `Nat.pred` without corresponding theorem for `+ 1` or `- 1`, this adds the corresponding theorem. --- src/Init/Data/Nat/Basic.lean | 121 +++++++++++++++++- src/Init/Data/Nat/Bitwise/Lemmas.lean | 4 + src/Init/Data/Nat/Gcd.lean | 3 + src/Init/Data/Nat/Lemmas.lean | 14 +- src/Init/Prelude.lean | 10 +- src/Init/WFTactics.lean | 2 +- .../lean/interactive/hover.lean.expected.out | 12 +- .../interactive/hoverDot.lean.expected.out | 8 +- tests/lean/librarySearch.lean | 4 +- tests/lean/run/wfEqnsIssue.lean | 4 - 10 files changed, 155 insertions(+), 27 deletions(-) diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index a4aa2ecbc8..9a13897e11 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -200,6 +200,9 @@ protected theorem eq_zero_of_add_eq_zero_left (h : n + m = 0) : m = 0 := theorem mul_succ (n m : Nat) : n * succ m = n * m + n := rfl +theorem mul_add_one (n m : Nat) : n * (m + 1) = n * m + n := + rfl + @[simp] protected theorem zero_mul : ∀ (n : Nat), 0 * n = 0 | 0 => rfl | succ n => mul_succ 0 n ▸ (Nat.zero_mul n).symm ▸ rfl @@ -209,6 +212,8 @@ theorem succ_mul (n m : Nat) : (succ n) * m = (n * m) + m := by | zero => rfl | succ m ih => rw [mul_succ, add_succ, ih, mul_succ, add_succ, Nat.add_right_comm] +theorem add_one_mul (n m : Nat) : (n + 1) * m = (n * m) + m := succ_mul n m + protected theorem mul_comm : ∀ (n m : Nat), n * m = m * n | n, 0 => (Nat.zero_mul n).symm ▸ (Nat.mul_zero n).symm ▸ rfl | n, succ m => (mul_succ n m).symm ▸ (succ_mul m n).symm ▸ (Nat.mul_comm n m).symm ▸ rfl @@ -256,8 +261,18 @@ 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 le_of_lt_add_one {n m : Nat} : n < m + 1 → n ≤ m := le_of_succ_le_succ + +theorem lt_add_one_of_le {n m : Nat} : n ≤ m → n < m + 1 := succ_le_succ + @[simp] protected theorem sub_zero (n : Nat) : n - 0 = n := rfl +theorem not_add_one_le_zero (n : Nat) : ¬ n + 1 ≤ 0 := nofun + +theorem not_add_one_le_self : (n : Nat) → ¬ n + 1 ≤ n := Nat.not_succ_le_self + +theorem add_one_pos (n : Nat) : 0 < n + 1 := Nat.zero_lt_succ n + theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by induction m with | zero => exact rfl @@ -271,6 +286,8 @@ theorem pred_lt : ∀ {n : Nat}, n ≠ 0 → pred n < n | zero, h => absurd rfl h | succ _, _ => lt_succ_of_le (Nat.le_refl _) +theorem sub_one_lt : ∀ {n : Nat}, n ≠ 0 → n - 1 < n := pred_lt + theorem sub_le (n m : Nat) : n - m ≤ n := by induction m with | zero => exact Nat.le_refl (n - 0) @@ -340,6 +357,8 @@ theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n) @[simp] theorem lt_succ_self (n : Nat) : n < succ n := lt.base n +@[simp] protected theorem lt_add_one (n : Nat) : n < n + 1 := lt.base n + protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m := match Nat.lt_or_ge m n with | Or.inl h => Or.inl (Nat.le_of_lt h) @@ -370,6 +389,9 @@ theorem le_or_eq_of_le_succ {m n : Nat} (h : m ≤ succ n) : m ≤ n ∨ m = suc have : succ m ≤ succ n := succ_le_of_lt this Or.inl (le_of_succ_le_succ this)) +theorem le_or_eq_of_le_add_one {m n : Nat} (h : m ≤ n + 1) : m ≤ n ∨ m = n + 1 := + le_or_eq_of_le_succ h + theorem le_add_right : ∀ (n k : Nat), n ≤ n + k | n, 0 => Nat.le_refl n | n, k+1 => le_succ_of_le (le_add_right n k) @@ -377,12 +399,25 @@ theorem le_add_right : ∀ (n k : Nat), n ≤ n + k theorem le_add_left (n m : Nat): n ≤ m + n := Nat.add_comm n m ▸ le_add_right n m +theorem le_of_add_right_le {n m k : Nat} (h : n + k ≤ m) : n ≤ m := + Nat.le_trans (le_add_right n k) h + +theorem le_add_right_of_le {n m k : Nat} (h : n ≤ m) : n ≤ m + k := + Nat.le_trans h (le_add_right m k) + +theorem lt_of_add_one_le {n m : Nat} (h : n + 1 ≤ m) : n < m := h + +theorem add_one_le_of_lt {n m : Nat} (h : n < m) : n + 1 ≤ m := h + protected theorem lt_add_left (c : Nat) (h : a < b) : a < c + b := Nat.lt_of_lt_of_le h (Nat.le_add_left ..) protected theorem lt_add_right (c : Nat) (h : a < b) : a < b + c := Nat.lt_of_lt_of_le h (Nat.le_add_right ..) +theorem lt_of_add_right_lt {n m k : Nat} (h : n + k < m) : n < m := + Nat.lt_of_le_of_lt (Nat.le_add_right ..) h + theorem le.dest : ∀ {n m : Nat}, n ≤ m → Exists (fun k => n + k = m) | zero, zero, _ => ⟨0, rfl⟩ | zero, succ n, _ => ⟨succ n, Nat.add_comm 0 (succ n) ▸ rfl⟩ @@ -537,9 +572,14 @@ protected theorem le_iff_lt_or_eq {n m : Nat} : n ≤ m ↔ n < m ∨ n = m := protected theorem lt_succ_iff : m < succ n ↔ m ≤ n := ⟨le_of_lt_succ, lt_succ_of_le⟩ +protected theorem lt_add_one_iff : m < n + 1 ↔ m ≤ n := ⟨le_of_lt_succ, lt_succ_of_le⟩ + protected theorem lt_succ_iff_lt_or_eq : m < succ n ↔ m < n ∨ m = n := Nat.lt_succ_iff.trans Nat.le_iff_lt_or_eq +protected theorem lt_add_one_iff_lt_or_eq : m < n + 1 ↔ m < n ∨ m = n := + Nat.lt_add_one_iff.trans Nat.le_iff_lt_or_eq + protected theorem eq_of_lt_succ_of_not_lt (hmn : m < n + 1) (h : ¬ m < n) : m = n := (Nat.lt_succ_iff_lt_or_eq.1 hmn).resolve_left h @@ -571,12 +611,18 @@ attribute [simp] zero_lt_succ theorem succ_ne_self (n) : succ n ≠ n := Nat.ne_of_gt (lt_succ_self n) +theorem add_one_ne_self (n) : n + 1 ≠ n := Nat.ne_of_gt (lt_succ_self n) + theorem succ_le : succ n ≤ m ↔ n < m := .rfl +theorem add_one_le_iff : n + 1 ≤ m ↔ n < m := .rfl + theorem lt_succ : m < succ n ↔ m ≤ n := ⟨le_of_lt_succ, lt_succ_of_le⟩ theorem lt_succ_of_lt (h : a < b) : a < succ b := le_succ_of_le h +theorem lt_add_one_of_lt (h : a < b) : a < b + 1 := le_succ_of_le h + theorem succ_pred_eq_of_ne_zero : ∀ {n}, n ≠ 0 → succ (pred n) = n | _+1, _ => rfl @@ -596,6 +642,9 @@ theorem pred_inj : ∀ {a b}, 0 < a → 0 < b → pred a = pred b → a = b theorem pred_ne_self : ∀ {a}, a ≠ 0 → pred a ≠ a | _+1, _ => (succ_ne_self _).symm +theorem sub_one_ne_self : ∀ {a}, a ≠ 0 → a - 1 ≠ a + | _+1, _ => (succ_ne_self _).symm + theorem pred_lt_self : ∀ {a}, 0 < a → pred a < a | _+1, _ => lt_succ_self _ @@ -628,9 +677,17 @@ theorem le_sub_one_of_lt : a < b → a ≤ b - 1 := Nat.le_pred_of_lt theorem lt_of_le_pred (h : 0 < m) : n ≤ pred m → n < m := (le_pred_iff_lt h).1 +theorem lt_of_le_sub_one (h : 0 < m) : n ≤ m - 1 → n < m := (le_pred_iff_lt h).1 + +protected theorem le_sub_one_iff_lt (h : 0 < m) : n ≤ m - 1 ↔ n < m := + ⟨Nat.lt_of_le_sub_one h, Nat.le_sub_one_of_lt⟩ + theorem exists_eq_succ_of_ne_zero : ∀ {n}, n ≠ 0 → Exists fun k => n = succ k | _+1, _ => ⟨_, rfl⟩ +theorem exists_eq_add_one_of_ne_zero : ∀ {n}, n ≠ 0 → Exists fun k => n = k + 1 + | _+1, _ => ⟨_, rfl⟩ + /-! # Basic theorems for comparing numerals -/ theorem ctor_eq_zero : Nat.zero = 0 := @@ -686,6 +743,9 @@ theorem eq_of_mul_eq_mul_right {n m k : Nat} (hm : 0 < m) (h : n * m = k * m) : protected theorem pow_succ (n m : Nat) : n^(succ m) = n^m * n := rfl +protected theorem pow_add_one (n m : Nat) : n^(m + 1) = n^m * n := + rfl + protected theorem pow_zero (n : Nat) : n^0 = 1 := rfl theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i @@ -737,9 +797,15 @@ theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by exact absurd h (Nat.not_lt_zero _) apply Nat.noConfusion -theorem pred_lt' {n m : Nat} (h : m < n) : pred n < n := +theorem pred_lt_of_lt {n m : Nat} (h : m < n) : pred n < n := pred_lt (not_eq_zero_of_lt h) +set_option linter.missingDocs false in +@[deprecated (since := "2024-06-01")] abbrev pred_lt' := @pred_lt_of_lt + +theorem sub_one_lt_of_lt {n m : Nat} (h : m < n) : n - 1 < n := + sub_one_lt (not_eq_zero_of_lt h) + /-! # pred theorems -/ @[simp] protected theorem pred_zero : pred 0 = 0 := rfl @@ -750,12 +816,21 @@ theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by | zero => contradiction | succ => rfl +theorem sub_one_add_one {a : Nat} (h : a ≠ 0) : a - 1 + 1 = a := by + induction a with + | zero => contradiction + | succ => rfl + theorem succ_pred_eq_of_pos : ∀ {n}, 0 < n → succ (pred n) = n | _+1, _ => rfl theorem sub_one_add_one_eq_of_pos : ∀ {n}, 0 < n → (n - 1) + 1 = n | _+1, _ => rfl +theorem eq_zero_or_eq_sub_one_add_one : ∀ {n}, n = 0 ∨ n = n - 1 + 1 + | 0 => Or.inl rfl + | _+1 => Or.inr rfl + @[simp] theorem pred_eq_sub_one : pred n = n - 1 := rfl /-! # sub theorems -/ @@ -806,6 +881,9 @@ theorem add_sub_of_le {a b : Nat} (h : a ≤ b) : a + (b - a) = b := by have : a ≤ b := Nat.le_of_succ_le h rw [sub_succ, Nat.succ_add, ← Nat.add_succ, Nat.succ_pred hne, ih this] +theorem sub_one_cancel : ∀ {a b : Nat}, 0 < a → 0 < b → a - 1 = b - 1 → a = b + | _+1, _+1, _, _ => congrArg _ + @[simp] protected theorem sub_add_cancel {n m : Nat} (h : m ≤ n) : n - m + m = n := by rw [Nat.add_comm, Nat.add_sub_of_le h] @@ -857,6 +935,17 @@ protected theorem sub_lt_sub_left : ∀ {k m n : Nat}, k < m → k < n → m - n | zero => rfl | succ n ih => simp only [ih, Nat.sub_succ]; decide +protected theorem sub_lt_sub_right : ∀ {a b c : Nat}, c ≤ a → a < b → a - c < b - c + | 0, _, _, hle, h => by + rw [Nat.eq_zero_of_le_zero hle, Nat.sub_zero, Nat.sub_zero] + exact h + | _, _, 0, _, h => by + rw [Nat.sub_zero, Nat.sub_zero] + exact h + | _+1, _+1, _+1, hle, h => by + rw [Nat.add_sub_add_right, Nat.add_sub_add_right] + exact Nat.sub_lt_sub_right (le_of_succ_le_succ hle) (lt_of_succ_lt_succ h) + protected theorem sub_self_add (n m : Nat) : n - (n + m) = 0 := by show (n + 0) - (n + m) = 0 rw [Nat.add_sub_add_left, Nat.zero_sub] @@ -935,6 +1024,9 @@ protected theorem sub_le_sub_right {n m : Nat} (h : n ≤ m) : ∀ k, n - k ≤ | 0 => h | z+1 => pred_le_pred (Nat.sub_le_sub_right h z) +protected theorem sub_le_add_right_sub (a i j : Nat) : a - i ≤ a + j - i := + Nat.sub_le_sub_right (Nat.le_add_right ..) .. + 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) @@ -947,6 +1039,9 @@ protected theorem lt_of_sub_pos (h : 0 < n - m) : m < n := 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 lt_of_sub_eq_sub_one (h : m - n = l + 1) : 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 @@ -974,21 +1069,35 @@ protected theorem sub_eq_iff_eq_add {c : Nat} (h : b ≤ a) : a - b = c ↔ a = 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 +/-! ## Mul sub distrib -/ + +theorem pred_mul (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 -/ +set_option linter.missingDocs false in +@[deprecated (since := "2024-06-01")] abbrev mul_pred_left := @pred_mul -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_one_mul (n m : Nat) : (n - 1) * m = n * m - m := by + cases n with + | zero => simp + | succ n => + rw [Nat.add_sub_cancel, add_one_mul, Nat.add_sub_cancel] +theorem mul_pred (n m : Nat) : n * pred m = n * m - n := by + rw [Nat.mul_comm, pred_mul, Nat.mul_comm] + +set_option linter.missingDocs false in +@[deprecated (since := "2024-06-01")] abbrev mul_pred_right := @mul_pred + +theorem mul_sub_one (n m : Nat) : n * (m - 1) = n * m - n := by + rw [Nat.mul_comm, Nat.sub_one_mul , 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 - | succ m ih => rw [Nat.sub_succ, Nat.mul_pred_left, ih, succ_mul, Nat.sub_sub]; done + | succ m ih => rw [Nat.sub_succ, Nat.pred_mul, ih, succ_mul, Nat.sub_sub]; done protected theorem mul_sub_left_distrib (n m k : Nat) : n * (m - k) = n * m - n * k := by rw [Nat.mul_comm, Nat.mul_sub_right_distrib, Nat.mul_comm m n, Nat.mul_comm n k] diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index d039ded7c3..51eba5e04a 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -90,6 +90,10 @@ noncomputable def div2Induction {motive : Nat → Sort u} unfold testBit simp [shiftRight_succ_inside] +@[simp] theorem testBit_add_one (x i : Nat) : testBit x (i + 1) = testBit (x/2) i := by + unfold testBit + simp [shiftRight_succ_inside] + theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by induction i generalizing x with | zero => diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean index 78961e04e0..9402b474a1 100644 --- a/src/Init/Data/Nat/Gcd.lean +++ b/src/Init/Data/Nat/Gcd.lean @@ -43,6 +43,9 @@ def gcd (m n : @& Nat) : Nat := theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := by rw [gcd]; rfl +theorem gcd_add_one (x y : Nat) : gcd (x + 1) y = gcd (y % (x + 1)) (x + 1) := by + rw [gcd]; rfl + @[simp] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by rw [gcd_succ, mod_one] rfl diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 07c071affe..d3eece2f9b 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -101,6 +101,10 @@ protected theorem one_sub : ∀ n, 1 - n = if n = 0 then 1 else 0 theorem succ_sub_sub_succ (n m k) : succ n - m - succ k = n - m - k := by rw [Nat.sub_sub, Nat.sub_sub, add_succ, succ_sub_succ] +theorem add_sub_sub_add_right (n m k l : Nat) : + (n + l) - m - (k + l) = n - m - k := by + rw [Nat.sub_sub, Nat.sub_sub, ←Nat.add_assoc, Nat.add_sub_add_right] + protected theorem sub_right_comm (m n k : Nat) : m - n - k = m - k - n := by rw [Nat.sub_sub, Nat.sub_sub, Nat.add_comm] @@ -176,10 +180,12 @@ protected theorem sub_add_lt_sub (h₁ : m + k ≤ n) (h₂ : 0 < k) : n - (m + rw [← Nat.sub_sub]; exact Nat.sub_lt_of_pos_le h₂ (Nat.le_sub_of_add_le' h₁) theorem sub_one_lt_of_le (h₀ : 0 < a) (h₁ : a ≤ b) : a - 1 < b := - Nat.lt_of_lt_of_le (Nat.pred_lt' h₀) h₁ + Nat.lt_of_lt_of_le (Nat.pred_lt_of_lt h₀) h₁ theorem sub_lt_succ (a b) : a - b < succ a := lt_succ_of_le (sub_le a b) +theorem sub_lt_add_one (a b) : a - b < a + 1 := lt_add_one_of_le (sub_le a b) + theorem sub_one_sub_lt (h : i < n) : n - 1 - i < n := by rw [Nat.sub_right_comm]; exact Nat.sub_one_lt_of_le (Nat.sub_pos_of_lt h) (Nat.sub_le ..) @@ -479,6 +485,9 @@ protected theorem mul_lt_mul_of_lt_of_lt {a b c d : Nat} (hac : a < c) (hbd : b theorem succ_mul_succ (a b) : succ a * succ b = a * b + a + b + 1 := by rw [succ_mul, mul_succ]; rfl +theorem add_one_mul_add_one (a b : Nat) : (a + 1) * (b + 1) = a * b + a + b + 1 := by + rw [add_one_mul, mul_add_one]; rfl + theorem mul_le_add_right (m k n : Nat) : k * m ≤ m + n ↔ (k-1) * m ≤ n := by match k with | 0 => @@ -562,6 +571,9 @@ theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by theorem pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n := by rw [Nat.pow_succ, Nat.mul_comm] +theorem pow_add_one' {m n : Nat} : m ^ (n + 1) = m * m ^ n := by + rw [Nat.pow_add_one, Nat.mul_comm] + @[simp] theorem pow_eq {m n : Nat} : m.pow n = m ^ n := rfl theorem one_shiftLeft (n : Nat) : 1 <<< n = 2 ^ n := by rw [shiftLeft_eq, Nat.one_mul] diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 41777235ab..faab0d139e 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1071,11 +1071,15 @@ This type is special-cased by both the kernel and the compiler: library (usually [GMP](https://gmplib.org/)). -/ inductive Nat where - /-- `Nat.zero`, normally written `0 : Nat`, is the smallest natural number. - This is one of the two constructors of `Nat`. -/ + /-- `Nat.zero`, is the smallest natural number. This is one of the two + constructors of `Nat`. Using `Nat.zero` should usually be avoided in favor of + `0 : Nat` or simply `0`, in order to remain compatible with the simp normal + form defined by `Nat.zero_eq`. -/ | zero : Nat /-- The successor function on natural numbers, `succ n = n + 1`. - This is one of the two constructors of `Nat`. -/ + This is one of the two constructors of `Nat`. Using `succ n` should usually + be avoided in favor of `n + 1`, in order to remain compatible with the simp + normal form defined by `Nat.succ_eq_add_one`. -/ | succ (n : Nat) : Nat instance : Inhabited Nat where diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean index 60897eb744..3c970d083c 100644 --- a/src/Init/WFTactics.lean +++ b/src/Init/WFTactics.lean @@ -32,7 +32,7 @@ before `omega` is available. -/ syntax "decreasing_trivial_pre_omega" : tactic macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a -macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i +macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt_of_lt; assumption) -- i-1 < i if j < i macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt; assumption) -- i-1 < i if i ≠ 0 diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index a54ce09e3c..012e4b45c0 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -20,7 +20,7 @@ {"start": {"line": 12, "character": 4}, "end": {"line": 12, "character": 12}}, "contents": {"value": - "```lean\nNat.zero : Nat\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", + "```lean\nNat.zero : Nat\n```\n***\n`Nat.zero`, is the smallest natural number. This is one of the two\nconstructors of `Nat`. Using `Nat.zero` should usually be avoided in favor of\n`0 : Nat` or simply `0`, in order to remain compatible with the simp normal\nform defined by `Nat.zero_eq`. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 21, "character": 2}} @@ -521,7 +521,7 @@ {"start": {"line": 257, "character": 4}, "end": {"line": 257, "character": 9}}, "contents": {"value": - "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", + "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, is the smallest natural number. This is one of the two\nconstructors of `Nat`. Using `Nat.zero` should usually be avoided in favor of\n`0 : Nat` or simply `0`, in order to remain compatible with the simp normal\nform defined by `Nat.zero_eq`. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 257, "character": 15}} @@ -530,7 +530,7 @@ "end": {"line": 257, "character": 18}}, "contents": {"value": - "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", + "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, is the smallest natural number. This is one of the two\nconstructors of `Nat`. Using `Nat.zero` should usually be avoided in favor of\n`0 : Nat` or simply `0`, in order to remain compatible with the simp normal\nform defined by `Nat.zero_eq`. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 260, "character": 6}} @@ -538,7 +538,7 @@ {"start": {"line": 260, "character": 4}, "end": {"line": 260, "character": 9}}, "contents": {"value": - "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 260, "character": 17}} @@ -547,7 +547,7 @@ "end": {"line": 260, "character": 20}}, "contents": {"value": - "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 263, "character": 27}} @@ -565,7 +565,7 @@ "end": {"line": 263, "character": 36}}, "contents": {"value": - "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", + "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, is the smallest natural number. This is one of the two\nconstructors of `Nat`. Using `Nat.zero` should usually be avoided in favor of\n`0 : Nat` or simply `0`, in order to remain compatible with the simp normal\nform defined by `Nat.zero_eq`. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 269, "character": 2}} diff --git a/tests/lean/interactive/hoverDot.lean.expected.out b/tests/lean/interactive/hoverDot.lean.expected.out index 844b67da3b..2146a7314e 100644 --- a/tests/lean/interactive/hoverDot.lean.expected.out +++ b/tests/lean/interactive/hoverDot.lean.expected.out @@ -20,7 +20,7 @@ {"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 18}}, "contents": {"value": - "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 16, "character": 11}} @@ -34,7 +34,7 @@ {"start": {"line": 16, "character": 14}, "end": {"line": 16, "character": 18}}, "contents": {"value": - "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 19, "character": 13}} @@ -48,7 +48,7 @@ {"start": {"line": 19, "character": 16}, "end": {"line": 19, "character": 20}}, "contents": {"value": - "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 22, "character": 14}} @@ -62,5 +62,5 @@ {"start": {"line": 22, "character": 17}, "end": {"line": 22, "character": 21}}, "contents": {"value": - "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", "kind": "markdown"}} diff --git a/tests/lean/librarySearch.lean b/tests/lean/librarySearch.lean index 474828fb15..c762e037f4 100644 --- a/tests/lean/librarySearch.lean +++ b/tests/lean/librarySearch.lean @@ -17,7 +17,7 @@ noncomputable section -/-- info: Try this: exact Nat.lt.base x -/ +/-- info: Try this: exact Nat.lt_add_one x -/ #guard_msgs in example (x : Nat) : x ≠ x.succ := Nat.ne_of_lt (by apply?) @@ -39,7 +39,7 @@ example (n m k : Nat) : n ≤ m → n + k ≤ m + k := by apply? #guard_msgs in example (_ha : a > 0) (w : b ∣ c) : a * b ∣ a * c := by apply? -/-- info: Try this: Nat.lt.base x -/ +/-- info: Try this: Nat.lt_add_one x -/ #guard_msgs in example : x < x + 1 := exact?% diff --git a/tests/lean/run/wfEqnsIssue.lean b/tests/lean/run/wfEqnsIssue.lean index 14ede871e8..63b2429493 100644 --- a/tests/lean/run/wfEqnsIssue.lean +++ b/tests/lean/run/wfEqnsIssue.lean @@ -55,10 +55,6 @@ def Ctx.extend (x : α) : HList Γ → HList (α :: Γ) := def Ctx.drop : HList (α :: Γ) → HList Γ | HList.cons a as => as --- custom wf tactic -theorem Nat.le_add_right_of_le (n m : Nat) : n ≤ m → n ≤ m + k := - fun h => add_le_add h (Nat.zero_le _) - macro_rules | `(tactic| decreasing_tactic) => `(tactic|