merge lean-pr-testing-6123

leanprover-community · Dec 14, 2024 · 6dd5eb5 · 6dd5eb5
1 parent 0c995c6
commit 6dd5eb5
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 13 deletions.
diff --git a/Aesop/RuleSet.lean b/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
   }

diff --git a/AesopTest/RulePattern.lean b/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 ≤ (n : Int)
-    guard_hyp fwd_2 : 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)]
@@ -44,8 +44,8 @@ axiom triangle (a b : Int) : |a + b| ≤ |a| + |b|
 
 example : |a + b| ≤ |c + d| := by
   aesop!
-  guard_hyp fwd   : |c + d| ≤ |c| + |d|
-  guard_hyp fwd_1 : |a + b| ≤ |a| + |b|
+  guard_hyp fwd_1 : |c + d| ≤ |c| + |d|
+  guard_hyp fwd   : |a + b| ≤ |a| + |b|
   falso
 
 @[aesop safe apply (pattern := (0 : Nat))]

diff --git a/AesopTest/SaturatePerformance.lean b/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

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9b9f4d0406d00baaae62d1a717b5aa854a2ae51d",
+   "rev": "13c202289cae0db69d997904de3c4d43c9222ea8",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-20
+leanprover/lean4:nightly-2024-12-14
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2024-11-20
		leanprover/lean4:nightly-2024-12-14