chore: adaptations for nightly-2024-10-17

Aesop/Frontend/Attribute.lean

@@ -51,7 +51,7 @@ initialize registerBuiltinAttribute {
   add := λ decl stx attrKind => withRef stx do
     let rules ← runTermElabMAsCoreM do
       let config ← AttrConfig.elab stx
-      config.rules.concatMapM (·.buildAdditionalGlobalRules decl)
+      config.rules.flatMapM (·.buildAdditionalGlobalRules decl)
     for (rule, rsNames) in rules do
       for rsName in rsNames do
         addGlobalRule rsName rule attrKind (checkNotExists := true)

Aesop/Search/Expansion/Basic.lean

@@ -15,12 +15,11 @@ def runRuleTac (tac : RuleTac) (ruleName : RuleName)
     (preState : Meta.SavedState) (input : RuleTacInput) :
     MetaM (Sum Exception RuleTacOutput) := do
   let result ←
-    try
-      Sum.inr <$> preState.runMetaM' do
+    tryCatchRuntimeEx
+      (Sum.inr <$> preState.runMetaM' do
         withMaxHeartbeats input.options.maxRuleHeartbeats do
-          tac input
-    catch e =>
-      return Sum.inl e
+          tac input)
+      (λ e => return Sum.inl e)
   if ← Check.rules.isEnabled then
     if let (Sum.inr ruleOutput) := result then
       ruleOutput.applications.forM λ rapp => do

Aesop/Search/Expansion/Norm.lean

@@ -230,12 +230,11 @@ def normSimp (goal : MVarId) (goalMVars : Std.HashSet MVarId) :
     NormM (Option NormRuleResult) := do
   profilingRule .normSimp (wasSuccessful := λ _ => true) do
     checkSimp "norm simp" (mayCloseGoal := true) goal do
-      try
-        withNormTraceNode .normSimp do
+      tryCatchRuntimeEx
+        (withNormTraceNode .normSimp do
           withMaxHeartbeats (← read).options.maxSimpHeartbeats do
-            normSimpCore goal goalMVars
-      catch e =>
-        throwError "aesop: error in norm simp: {e.toMessageData}"
+            normSimpCore goal goalMVars)
+        (λ e => throwError "aesop: error in norm simp: {e.toMessageData}")
 
 def normUnfoldCore (goal : MVarId) : NormM (Option NormRuleResult) := do
   let unfoldRules := (← read).ruleSet.unfoldRules
@@ -250,12 +249,11 @@ def normUnfoldCore (goal : MVarId) : NormM (Option NormRuleResult) := do
 def normUnfold (goal : MVarId) : NormM (Option NormRuleResult) := do
   profilingRule .normUnfold (wasSuccessful := λ _ => true) do
     checkSimp "unfold simp" (mayCloseGoal := false) goal do
-      try
-        withNormTraceNode .normUnfold do
+      tryCatchRuntimeEx
+        (withNormTraceNode .normUnfold do
           withMaxHeartbeats (← read).options.maxUnfoldHeartbeats do
-            normUnfoldCore goal
-      catch e =>
-        throwError "aesop: error in norm unfold: {e.toMessageData}"
+            normUnfoldCore goal)
+        (λ e => throwError "aesop: error in norm unfold: {e.toMessageData}")
 
 inductive NormSeqResult where
   | proved (script : Array (DisplayRuleName × Option (Array Script.LazyStep)))

Aesop/Util/Tactic.lean

@@ -29,8 +29,6 @@ def replaceFVar (goal : MVarId) (fvarId : FVarId) (type : Expr) (proof : Expr) :
   let (newFVarId, goal) ← intro1Core goal (preserveBinderNames := true)
   return (goal, newFVarId, clearSuccess)
 
-open private getIntrosSize in Lean.MVarId.intros
-
 /-- Introduce as many binders as possible while unfolding definitions with the
 ambient transparency. -/
 partial def introsUnfolding (mvarId : MVarId) : MetaM (Array FVarId × MVarId) :=

AesopTest/EqualUpToIds.lean

@@ -57,7 +57,9 @@ Tactic 2:
   case zero
   n : Nat
   ⊢ True
-  case succ n n✝ : Nat ⊢ True
+  case succ
+  n n✝ : Nat
+  ⊢ True
 -/
 #guard_msgs in
 example (n m : Nat) : True := by

AesopTest/HeartbeatLimit.lean

@@ -24,7 +24,8 @@ example : Even 10 := by
   aesop
 
 /--
-error: aesop: error in norm simp: (deterministic) timeout at `simp`, maximum number of heartbeats (1) has been reached
+error: aesop: error in norm simp: tactic 'simp' failed, nested error:
+(deterministic) timeout at `simp`, maximum number of heartbeats (1) has been reached
 Use `set_option maxHeartbeats <num>` to set the limit.
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/

AesopTest/List.lean

@@ -106,7 +106,7 @@ namespace List
 -- is not particularly helpful for this file.
 attribute [-aesop] Aesop.BuiltinRules.ext
 
-attribute [simp] map List.bind
+attribute [simp] map List.flatMap
 
 instance : Pure List where
   pure x := [x]
@@ -318,39 +318,39 @@ theorem X.forall_mem_map_iff {f : α → β} {l : List α} {P : β → Prop} :
 @[simp] theorem X.map_eq_nil {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by
   aesop (add 1% cases List)
 
--- attribute [-simp] mem_join
-@[simp] theorem X.mem_join {a : α} : ∀ {L : List (List α)}, a ∈ join L ↔ ∃ l, l ∈ L ∧ a ∈ l := by
+attribute [-simp] mem_flatten
+@[simp] theorem X.mem_flatten {a : α} : ∀ {L : List (List α)}, a ∈ flatten L ↔ ∃ l, l ∈ L ∧ a ∈ l := by
   intro L; induction L <;> aesop
 
--- attribute [-simp] exists_of_mem_join
-theorem X.exists_of_mem_join {a : α} {L : List (List α)} : a ∈ join L → ∃ l, l ∈ L ∧ a ∈ l := by
+-- attribute [-simp] exists_of_mem_flatten
+theorem X.exists_of_mem_flatten {a : α} {L : List (List α)} : a ∈ flatten L → ∃ l, l ∈ L ∧ a ∈ l := by
   aesop
 
--- attribute [-simp] mem_join_of_mem
-theorem X.mem_join_of_mem {a : α} {L : List (List α)} {l} (lL : l ∈ L) (al : a ∈ l) : a ∈ join L := by
+-- attribute [-simp] mem_flatten_of_mem
+theorem X.mem_flatten_of_mem {a : α} {L : List (List α)} {l} (lL : l ∈ L) (al : a ∈ l) : a ∈ flatten L := by
   aesop
 
--- attribute [-simp] mem_bind
-@[simp] theorem X.mem_bind {b : β} {l : List α} {f : α → List β} : b ∈ l.bind f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
+-- attribute [-simp] mem_flatMap
+@[simp] theorem X.mem_flatMap {b : β} {l : List α} {f : α → List β} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
   induction l <;> aesop
 
--- attribute [-simp] exists_of_mem_bind
-theorem X.exists_of_mem_bind {l : List α} :
-    b ∈ l.bind f → ∃ a, a ∈ l ∧ b ∈ f a := by
+-- attribute [-simp] exists_of_mem_flatMap
+theorem X.exists_of_mem_flatMap {l : List α} :
+    b ∈ l.flatMap f → ∃ a, a ∈ l ∧ b ∈ f a := by
   aesop
 
--- attribute [-simp] mem_bind_of_mem
-theorem X.mem_bind_of_mem {l : List α} :
-    (∃ a, a ∈ l ∧ b ∈ f a) → b ∈ l.bind f := by
+-- attribute [-simp] mem_flatMap_of_mem
+theorem X.mem_flatMap_of_mem {l : List α} :
+    (∃ a, a ∈ l ∧ b ∈ f a) → b ∈ l.flatMap f := by
   induction l <;> aesop
 
--- attribute [-simp] bind_map
-theorem X.bind_map {g : α → List β} {f : β → γ} :
-  ∀ l : List α, map f (l.bind g) = l.bind (λa => (g a).map f) := by
+-- attribute [-simp] flatMap_map
+theorem X.flatMap_map {g : α → List β} {f : β → γ} :
+  ∀ l : List α, map f (l.flatMap g) = l.flatMap (λa => (g a).map f) := by
   intro l; induction l <;> aesop
 
-theorem map_bind' (g : β → List γ) (f : α → β) :
-  ∀ l : List α, (map f l).bind g = l.bind (λ a => g (f a)) := by
+theorem map_flatMap' (g : β → List γ) (f : α → β) :
+  ∀ l : List α, (map f l).flatMap g = l.flatMap (λ a => g (f a)) := by
   intro l; induction l <;> aesop
 
 -- theorem range_map (f : α → β) : set.range (map f) = {l | ∀ x ∈ l, x ∈ set.range f} :=
@@ -671,20 +671,25 @@ theorem replicate_subset_singleton (a : α) (n) : replicate n a ⊆ [a] := by
 theorem subset_singleton_iff {a : α} {L : List α} : L ⊆ [a] ↔ ∃ n, L = replicate n a :=
   ADMIT -- Nontrivial existential.
 
+attribute [-simp] map_const
+-- attribute [-simp] map_const'
 @[simp] theorem map_const'' (l : List α) (b : β) : map (λ _ => b) l = replicate l.length b := by
   induction l <;> aesop
 
 theorem eq_of_mem_map_const {b₁ b₂ : β} {l : List α} (h : b₁ ∈ map (λ _ => b₂) l) :
   b₁ = b₂ := by
   aesop
 
+attribute [-simp] map_replicate
 @[simp] theorem map_replicate' (f : α → β) (a : α) (n) : map f (replicate n a) = replicate n (f a) := by
   induction n <;> aesop
 
+attribute [-simp] tail_replicate
 @[simp] theorem tail_replicate' (a : α) (n) : tail (replicate n a) = replicate n.pred a := by
   aesop (add 1% cases Nat)
 
-@[simp] theorem join_replicate_nil' (n : Nat) : join (replicate n []) = @nil α := by
+attribute [-simp] flatten_replicate_nil
+@[simp] theorem flatten_replicate_nil' (n : Nat) : flatten (replicate n []) = @nil α := by
   induction n <;> aesop
 
 theorem replicate_left_injective {n : Nat} (hn : n ≠ 0) :
@@ -706,39 +711,39 @@ theorem replicate_right_injective (a : α) : Injective (λ n => replicate n a) :
 
 /-! ### pure -/
 
-@[simp]
-theorem mem_pure {α} (x y : α) :
+@[simp] theorem mem_pure {α} (x y : α) :
     x ∈ (pure y : List α) ↔ x = y := by
   aesop (add norm simp pure)
 
-/-! ### bind -/
+/-! ### flatMap -/
 
 instance : Bind List where
-  bind l f := List.bind l f
+  bind l f := List.flatMap l f
 
-@[simp] theorem bind_eq_bind {α β} (f : α → List β) (l : List α) :
-    l >>= f = l.bind f := rfl
+@[simp] theorem bind_eq_flatMap {α β} (f : α → List β) (l : List α) :
+    l >>= f = l.flatMap f := rfl
 
-attribute [-simp] bind_append
-theorem X.bind_append (f : α → List β) (l₁ l₂ : List α) :
-  (l₁ ++ l₂).bind f = l₁.bind f ++ l₂.bind f := by
+attribute [-simp] flatMap_append
+theorem X.flatMap_append (f : α → List β) (l₁ l₂ : List α) :
+  (l₁ ++ l₂).flatMap f = l₁.flatMap f ++ l₂.flatMap f := by
   induction l₁ <;> aesop
 
-@[simp] theorem bind_singleton'' (f : α → List β) (x : α) : [x].bind f = f x := by
+attribute [-simp] flatMap_singleton'
+@[simp] theorem X.flatMap_singleton' (f : α → List β) (x : α) : [x].flatMap f = f x := by
   aesop
 
-@[simp] theorem bind_singleton''' (l : List α) : l.bind (λ x => [x]) = l := by
+@[simp] theorem X.flatMap_singleton'' (l : List α) : l.flatMap (λ x => [x]) = l := by
   induction l <;> aesop
 
-theorem map_eq_bind' {α β} (f : α → β) (l : List α) : map f l = l.bind (λ x => [f x]) := by
+theorem map_eq_flatMap' {α β} (f : α → β) (l : List α) : map f l = l.flatMap (λ x => [f x]) := by
   induction l <;> aesop
 
-theorem bind_assoc' {α β γ : Type u} (l : List α) (f : α → List β) (g : β → List γ) :
-    (l.bind f).bind g = l.bind (λ x => (f x).bind g) :=
+theorem flatMap_assoc' {α β γ : Type u} (l : List α) (f : α → List β) (g : β → List γ) :
+    (l.flatMap f).flatMap g = l.flatMap (λ x => (f x).flatMap g) :=
   ADMIT
-  -- have aux {δ : Type u} (xs ys : List (List δ)) : join (xs ++ ys) = join xs ++ join ys := by
+  -- have aux {δ : Type u} (xs ys : List (List δ)) : flatten (xs ++ ys) = flatten xs ++ flatten ys := by
   --   induction xs <;> aesop
-  -- induction l <;> aesop (add norm [simp [bind_append], unfold [bind]])
+  -- induction l <;> aesop (add norm [simp [flatMap_append], unfold [flatMap]])
 
 /-! ### concat -/
 
@@ -770,6 +775,7 @@ attribute [simp] append_assoc
 theorem X.concat_append (a : α) (l₁ l₂ : List α) : concat l₁ a ++ l₂ = l₁ ++ a :: l₂ := by
   aesop
 
+-- attribute [-simp] length_concat
 theorem X.length_concat (a : α) (l : List α) : length (concat l a) = .succ (length l) := by
   aesop
 
@@ -790,9 +796,8 @@ attribute [-simp] reverse_cons
   -- aesop (add norm unfold reverse)
 
 -- Note: reverse_core is called reverseAux in Lean 4.
--- attribute [-simp] reverseAux_eq
-@[simp]
-theorem reverse_core_eq (l₁ l₂ : List α) : reverseAux l₁ l₂ = reverse l₁ ++ l₂ := by
+attribute [-simp] reverseAux_eq
+@[simp] theorem X.reverseAux_eq (l₁ l₂ : List α) : reverseAux l₁ l₂ = reverse l₁ ++ l₂ := by
   induction l₁ generalizing l₂ <;> aesop
 
 theorem reverse_cons' (a : α) (l : List α) : reverse (a::l) = concat (reverse l) a := by
@@ -801,9 +806,10 @@ theorem reverse_cons' (a : α) (l : List α) : reverse (a::l) = concat (reverse
 @[simp] theorem reverse_singleton (a : α) : reverse [a] = [a] := rfl
 
 -- TODO: after nightly-2024-08-27, `aesop` can not prove this anymore!
--- attribute [-simp] reverse_append in
--- @[simp] theorem X.reverse_append (s t : List α) : reverse (s ++ t) = (reverse t) ++ (reverse s) := by
---   induction s <;> aesop
+attribute [-simp] reverse_append in
+@[simp] theorem X.reverse_append (s t : List α) : reverse (s ++ t) = (reverse t) ++ (reverse s) :=
+  ADMIT
+  -- induction s <;> aesop
 
 -- attribute [-simp] reverse_concat
 theorem X.reverse_concat (l : List α) (a : α) : reverse (concat l a) = a :: reverse l := by

AesopTest/RulePatternLooseBVar.lean

@@ -9,7 +9,7 @@ Authors: Son Ho, Jannis Limperg
 
 import Aesop
 
-inductive ScalarTy :=
+inductive ScalarTy
 | U32
 
 @[simp]

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fc871f7039ac6d8ab993335bb35aba43286004a0",
+   "rev": "389fb58a2ff92e1ede0db37b1fedcb9a6162df94",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "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 = "main"
+rev = "nightly-testing"
 
 [[lean_lib]]
 name = "Aesop"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc1
+leanprover/lean4:nightly-2024-10-17