chore: bump Std (#8505)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Dec 15, 2023 · d1e4753 · d1e4753
1 parent 31b5843
commit d1e4753
Show file tree

Hide file tree

Showing 8 changed files with 11 additions and 41 deletions.
diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
@@ -176,20 +176,9 @@ theorem lt_self_iff_false (x : α) : x < x ↔ False :=
   ⟨lt_irrefl x, False.elim⟩
 #align lt_self_iff_false lt_self_iff_false
 
-theorem le_of_le_of_eq (hab : a ≤ b) (hbc : b = c) : a ≤ c :=
-  hab.trans hbc.le
 #align le_of_le_of_eq le_of_le_of_eq
-
-theorem le_of_eq_of_le (hab : a = b) (hbc : b ≤ c) : a ≤ c :=
-  hab.le.trans hbc
 #align le_of_eq_of_le le_of_eq_of_le
-
-theorem lt_of_lt_of_eq (hab : a < b) (hbc : b = c) : a < c :=
-  hab.trans_le hbc.le
 #align lt_of_lt_of_eq lt_of_lt_of_eq
-
-theorem lt_of_eq_of_lt (hab : a = b) (hbc : b < c) : a < c :=
-  hab.le.trans_lt hbc
 #align lt_of_eq_of_lt lt_of_eq_of_lt
 
 theorem le_of_le_of_eq' : b ≤ c → a = b → a ≤ c :=
@@ -353,18 +342,7 @@ theorem ge_of_eq [Preorder α] {a b : α} (h : a = b) : a ≥ b :=
   h.ge
 #align ge_of_eq ge_of_eq
 
--- see Note [nolint_ge]
--- Porting note: linter not found @[nolint ge_or_gt]
-@[simp]
-theorem ge_iff_le [LE α] {a b : α} : a ≥ b ↔ b ≤ a :=
-  Iff.rfl
 #align ge_iff_le ge_iff_le
-
--- see Note [nolint_ge]
--- Porting note: linter not found @[nolint ge_or_gt]
-@[simp]
-theorem gt_iff_lt [LT α] {a b : α} : a > b ↔ b < a :=
-  Iff.rfl
 #align gt_iff_lt gt_iff_lt
 
 theorem not_le_of_lt [Preorder α] {a b : α} (h : a < b) : ¬b ≤ a :=

diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean
@@ -123,8 +123,8 @@ section Hint
 register_hint split
 register_hint intro
 register_hint aesop
-register_hint decide
 register_hint simp_all?
 register_hint exact?
+register_hint decide
 
 end Hint
diff --git a/Mathlib/Tactic/LibrarySearch.lean b/Mathlib/Tactic/LibrarySearch.lean
@@ -67,7 +67,7 @@ def processLemma (name : Name) (constInfo : ConstantInfo) :
 /-- Insert a lemma into the discrimination tree. -/
 -- Recall that `apply?` caches the discrimination tree on disk.
 -- If you are modifying this file, you will probably want to delete
--- `build/lib/MathlibExtras/LibrarySearch.extra`
+-- `.lake/build/lib/MathlibExtras/LibrarySearch.extra`
 -- so that the cache is rebuilt.
 def addLemma (name : Name) (constInfo : ConstantInfo)
     (lemmas : DiscrTree (Name × DeclMod)) : MetaM (DiscrTree (Name × DeclMod)) := do

diff --git a/Mathlib/Tactic/Rewrites.lean b/Mathlib/Tactic/Rewrites.lean
@@ -56,6 +56,10 @@ def backwardWeight := 1
 /-- Configuration for `DiscrTree`. -/
 def discrTreeConfig : WhnfCoreConfig := {}
 
+/-- We will discard -/
+def keysSpecific (keys : Array DiscrTree.Key) : Bool :=
+  !(keys == #[.star] || keys == #[.const `Eq 3, .star, .star, .star])
+
 /-- Prepare the discrimination tree entries for a lemma. -/
 def processLemma (name : Name) (constInfo : ConstantInfo) :
     MetaM (Array (Array DiscrTree.Key × (Name × Bool × Nat))) := do
@@ -75,7 +79,7 @@ def processLemma (name : Name) (constInfo : ConstantInfo) :
       let lhsKey ← DiscrTree.mkPath lhs discrTreeConfig
       let rhsKey ← DiscrTree.mkPath rhs discrTreeConfig
       return #[(lhsKey, (name, false, forwardWeight * lhsKey.size)),
-        (rhsKey, (name, true, backwardWeight * rhsKey.size))]
+        (rhsKey, (name, true, backwardWeight * rhsKey.size))].filter fun t => keysSpecific t.1
     | _ => return #[]
 
 /-- Select `=` and `↔` local hypotheses. -/
@@ -96,18 +100,6 @@ def localHypotheses (except : List FVarId := []) : MetaM (Array (Expr × Bool ×
     | _ => pure ()
   return result
 
-/-- Insert a lemma into the discrimination tree. -/
--- Recall that `rw?` caches the discrimination tree on disk.
--- If you are modifying this file, you will probably want to delete
--- `build/lib/MathlibExtras/Rewrites.extra`
--- so that the cache is rebuilt.
-def addLemma (name : Name) (constInfo : ConstantInfo)
-    (lemmas : DiscrTree (Name × Bool × Nat)) : MetaM (DiscrTree (Name × Bool × Nat)) := do
-  let mut lemmas := lemmas
-  for (key, value) in ← processLemma name constInfo do
-    lemmas := lemmas.insertIfSpecific key value discrTreeConfig
-  return lemmas
-
 /-- Construct the discrimination tree of all lemmas. -/
 def buildDiscrTree : IO (DiscrTreeCache (Name × Bool × Nat)) :=
   DiscrTreeCache.mk "rw?: init cache" processLemma

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "d3049643f6dded69eb7ce8124796cb1ec8df8840",
+   "rev": "1d1197d7f3b480a4a4a1ec34b39a962852432bd2",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/test/LibrarySearch/basic.lean b/test/LibrarySearch/basic.lean
@@ -16,7 +16,7 @@ set_option autoImplicit true
 -- Recall that `apply?` caches the discrimination tree on disk.
 -- If you are modifying the way that `apply?` indexes lemmas,
 -- while testing you will probably want to delete
--- `build/lib/MathlibExtras/LibrarySearch.extra`
+-- `.lake/build/lib/MathlibExtras/LibrarySearch.extra`
 -- so that the cache is rebuilt.
 
 -- We need to set this here, as the lakefile does not enable this during testing.

diff --git a/test/hint.lean b/test/hint.lean
@@ -32,7 +32,7 @@ example {a b : ℚ} (h : a < b) : ¬ b < a := by hint
 
 /--
 info: Try these:
-• exact rfl
+• decide
 -/
 #guard_msgs in
 example : 37^2 - 35^2 = 72 * 2 := by hint

diff --git a/test/rewrites.lean b/test/rewrites.lean
@@ -13,7 +13,7 @@ set_option autoImplicit true
 -- Recall that `rw?` caches the discrimination tree on disk.
 -- If you are modifying the way that `rewrites` indexes lemmas,
 -- while testing you will probably want to delete
--- `build/lib/MathlibExtras/Rewrites.extra`
+-- `.lake/build/lib/MathlibExtras/Rewrites.extra`
 -- so that the cache is rebuilt.
 
 set_option autoImplicit true