chore: bump toolchain to v4.16.0-rc1 (#188)

Co-authored-by: Jannis Limperg <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>

Aesop/RuleSet.lean

@@ -372,7 +372,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) :
   if let some decl := f.matchesSimpTheorem? then
     for h : i in [:rs.simpTheoremsArray.size] do
       have i_valid : i < simpTheoremsArray'.fst.size := by
-        simp_all [Membership.mem, simpTheoremsArray'.snd]
+        simp_all +zetaDelta [Membership.mem, simpTheoremsArray'.snd]
       let (name, simpTheorems) := simpTheoremsArray'.fst[i]
       if SimpTheorems.containsDecl simpTheorems decl then
         let origin := .decl decl (inv := false)
@@ -383,7 +383,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) :
         anyErased := true
   let simpTheoremsArray := simpTheoremsArray'.fst
   let simpTheoremsArrayNonempty : 0 < simpTheoremsArray.size := by
-    simp [simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty]
+    simp [simpTheoremsArray, simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty]
   let rs := { rs with
     localNormSimpRules, simpTheoremsArray, simpTheoremsArrayNonempty
   }

Aesop/Util/Basic.lean

@@ -79,6 +79,7 @@ open DiscrTree
 
 -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with
 -- `n` stars).
+
 def getConclusionDiscrTreeKeys (type : Expr) : MetaM (Array Key) :=
   withoutModifyingState do
     let (_, _, conclusion) ← forallMetaTelescope type

AesopTest/List.lean

@@ -892,7 +892,7 @@ theorem last_append (l₁ l₂ : List α) (h : l₂ ≠ []) :
   last (l₁ ++ l₂) (append_ne_nil_of_right_ne_nil l₁ h) = last l₂ h := by
   induction l₁ <;> aesop
 
-theorem last_concat {a : α} (l : List α) : last (concat l a) (concat_ne_nil a l) = a := by
+theorem last_concat {a : α} (l : List α) : last (concat l a) (X.concat_ne_nil a l) = a := by
   aesop
 
 @[simp] theorem last_singleton (a : α) : last [a] (cons_ne_nil a []) = a := rfl

AesopTest/RulePattern.lean

@@ -23,8 +23,8 @@ example (m n : Nat) : (↑m : Int) < 0 ∧ (↑n : Int) > 0 := by
   set_option aesop.check.script false in
   aesop!
   all_goals
-    guard_hyp fwd_1 : 0 ≤ (m : Int)
     guard_hyp fwd_2 : 0 ≤ (n : Int)
+    guard_hyp fwd_1 : 0 ≤ (m : Int)
     falso
 
 @[aesop safe forward (pattern := min x y)]

AesopTest/SaturatePerformance.lean

@@ -41,11 +41,11 @@ import Aesop
 error: unsolved goals
 α : Type u_1
 l0 l1 l2 : List α
-fwd : (l0 ++ l1).length ≥ 0
-fwd_1 : (l0 ++ l1 ++ l2).length ≥ 0
-fwd_2 : l2.length ≥ 0
-fwd_3 : l0.length ≥ 0
-fwd_4 : l1.length ≥ 0
+fwd : l1.length ≥ 0
+fwd_1 : (l0 ++ l1).length ≥ 0
+fwd_2 : (l0 ++ l1 ++ l2).length ≥ 0
+fwd_3 : l2.length ≥ 0
+fwd_4 : l0.length ≥ 0
 ⊢ (l0 ++ l1 ++ l2).length = l0.length + l1.length + l2.length
 -/
 #guard_msgs in

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "rev": "8ce422eb59adf557fac184f8b1678c75fa03075c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "aesop",

lakefile.toml

@@ -6,7 +6,7 @@ precompileModules = false # We would like to turn this on, but it breaks the Mat
 [[require]]
 name = "batteries"
 git = "https://github.com/leanprover-community/batteries"
-rev = "v4.15.0"
+rev = "v4.16.0-rc1"
 
 [[lean_lib]]
 name = "Aesop"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0-rc1