From 18afefda96d7169fb407210eef11bc9925754fd6 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 16 Feb 2024 16:42:38 +1100 Subject: [PATCH] chore: upstream basic statements about inequalities (#3366) --- src/Init/Core.lean | 12 ++++++++++++ tests/lean/letFun.lean.expected.out | 8 ++++---- tests/lean/simp_trace.lean.expected.out | 6 ++++-- tests/lean/simp_trace_backtrack.lean | 3 --- tests/lean/simp_trace_backtrack.lean.expected.out | 2 +- 5 files changed, 21 insertions(+), 10 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 511d3dbcba..3b921fc126 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1932,6 +1932,18 @@ axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b end Lean +@[simp] theorem ge_iff_le [LE α] {x y : α} : x ≥ y ↔ y ≤ x := Iff.rfl + +@[simp] theorem gt_iff_lt [LT α] {x y : α} : x > y ↔ y < x := Iff.rfl + +theorem le_of_eq_of_le {a b c : α} [LE α] (h₁ : a = b) (h₂ : b ≤ c) : a ≤ c := h₁ ▸ h₂ + +theorem le_of_le_of_eq {a b c : α} [LE α] (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c := h₂ ▸ h₁ + +theorem lt_of_eq_of_lt {a b c : α} [LT α] (h₁ : a = b) (h₂ : b < c) : a < c := h₁ ▸ h₂ + +theorem lt_of_lt_of_eq {a b c : α} [LT α] (h₁ : a < b) (h₂ : b = c) : a < c := h₂ ▸ h₁ + namespace Std variable {α : Sort u} diff --git a/tests/lean/letFun.lean.expected.out b/tests/lean/letFun.lean.expected.out index fecb7bba97..264149a5cf 100644 --- a/tests/lean/letFun.lean.expected.out +++ b/tests/lean/letFun.lean.expected.out @@ -5,15 +5,15 @@ f (y + x) : Nat a b : Nat h1 : a = 0 h2 : b = 0 -⊢ (let_fun x := 1; - x + x) > - b +⊢ b < + let_fun x := 1; + x + x (let_fun this := id; this) 1 : Nat a b : Nat h : a > b -⊢ a > b +⊢ b < a let_fun n := 5; { val := [], property := (⋯ : 0 ≤ n) } : { as // List.length as ≤ 5 } rfl : (let_fun n := 5; diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out index 4f92e81a9e..46a60cdf2e 100644 --- a/tests/lean/simp_trace.lean.expected.out +++ b/tests/lean/simp_trace.lean.expected.out @@ -1,11 +1,13 @@ Try this: simp only [f] [Meta.Tactic.simp.rewrite] unfold f, f (a :: b = []) ==> a :: b = [] [Meta.Tactic.simp.rewrite] @eq_self:1000, False = False ==> True -Try this: simp only [length] +Try this: simp only [length, gt_iff_lt] [Meta.Tactic.simp.rewrite] unfold length, length (a :: b :: as) ==> length (b :: as) + 1 [Meta.Tactic.simp.rewrite] unfold length, length (b :: as) ==> length as + 1 -Try this: simp only [fact] +[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, length as + 1 + 1 > length as ==> length as < length as + 1 + 1 +Try this: simp only [fact, gt_iff_lt] [Meta.Tactic.simp.rewrite] unfold fact, fact (Nat.succ x) ==> (x + 1) * fact x +[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, (x + 1) * fact x > 0 ==> 0 < (x + 1) * fact x Try this: simp only [head] [Meta.Tactic.simp.rewrite] unfold head, head (a :: as) ==> match a :: as with | [] => default diff --git a/tests/lean/simp_trace_backtrack.lean b/tests/lean/simp_trace_backtrack.lean index 2448481fb1..7285ec1979 100644 --- a/tests/lean/simp_trace_backtrack.lean +++ b/tests/lean/simp_trace_backtrack.lean @@ -7,9 +7,6 @@ universe u theorem tsub_eq_zero_of_le {α : Type u} [LE α] [Sub α] [OfNat α 0] {a b : α} : a ≤ b → a - b = 0 := by sorry -@[simp] -theorem ge_iff_le (x y : Nat) : x ≥ y ↔ y ≤ x := Iff.rfl - set_option tactic.simp.trace true -- This used to report: `Try this: simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub]` diff --git a/tests/lean/simp_trace_backtrack.lean.expected.out b/tests/lean/simp_trace_backtrack.lean.expected.out index 7df7cbe9c5..cd7d8a676a 100644 --- a/tests/lean/simp_trace_backtrack.lean.expected.out +++ b/tests/lean/simp_trace_backtrack.lean.expected.out @@ -1,3 +1,3 @@ simp_trace_backtrack.lean:7:8-7:26: warning: declaration uses 'sorry' Try this: simp only [Nat.succ_sub_succ_eq_sub] -simp_trace_backtrack.lean:17:0-17:7: warning: declaration uses 'sorry' +simp_trace_backtrack.lean:14:0-14:7: warning: declaration uses 'sorry'