chore: bump toolchain to v4.10.0-rc1, and merge changes from nightly-…

…testing (#144)

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

Aesop/Index.lean

@@ -88,10 +88,6 @@ def foldM [Monad m] (ri : Index α) (f : σ → Rule α → m σ) (init : σ) :
 def fold (ri : Index α) (f : σ → Rule α → σ) (init : σ) : σ :=
   Id.run $ ri.foldM (init := init) f
 
-def size : Index α → Nat
-  | { byHyp, byTarget, unindexed } =>
-    byHyp.size + byTarget.size + unindexed.size
-
 -- May return duplicate `IndexMatchLocation`s.
 @[inline]
 private def applicableByTargetRules (ri : Index α) (goal : MVarId)
@@ -127,7 +123,7 @@ private def applicableByHypRules (ri : Index α) (goal : MVarId)
 private def applicableUnindexedRules (ri : Index α) (include? : Rule α → Bool) :
     Array (Rule α × Array IndexMatchLocation) :=
   -- Assumption: include? is true for most rules.
-  ri.unindexed.fold (init := Array.mkEmpty ri.unindexed.size) λ acc r =>
+  ri.unindexed.fold (init := #[]) λ acc r =>
     if include? r then
       acc.push (r, #[.none])
     else

Aesop/RuleSet.lean

@@ -163,7 +163,7 @@ def BaseRuleSet.trace (rs : BaseRuleSet) (traceOpt : TraceOption) :
     return
   withConstAesopTraceNode traceOpt (return "Erased rules") do
     aesop_trace![traceOpt] "(Note: even if these rules appear in the sections below, they will not be applied by Aesop.)"
-    let erased := rs.erased.fold (init := Array.mkEmpty rs.erased.size)
+    let erased := rs.erased.fold (init := #[])
       λ ary r => ary.push r
     for r in erased.qsortOrd do
       aesop_trace![traceOpt] r

Aesop/Tree/ExtractProof.lean

@@ -55,11 +55,8 @@ private def getNewConsts (oldEnv newEnv : Environment) :
     HashMap Name ConstantInfo := Id.run do
   let oldMap₂ := oldEnv.constants.map₂
   let newMap₂ := newEnv.constants.map₂
-  if oldMap₂.size == newMap₂.size then
-    HashMap.empty
-  else
-    newMap₂.foldl (init := HashMap.empty) λ cs n c =>
-      if oldMap₂.contains n then cs else cs.insert n c
+  newMap₂.foldl (init := HashMap.empty) λ cs n c =>
+    if oldMap₂.contains n then cs else cs.insert n c
 
 -- For each declaration `d` that appears in `newState` but not in
 -- `oldState`, add `d` to the environment. We assume that the environment in
@@ -77,10 +74,9 @@ open Match in
 private def copyMatchEqnsExtState (oldEnv newEnv : Environment) : CoreM Unit := do
   let oldState := matchEqnsExt.getState oldEnv
   let newState := matchEqnsExt.getState newEnv
-  if newState.map.size > oldState.map.size then
-    for (n, eqns) in newState.map do
-      if !oldState.map.contains n then
-        registerMatchEqns n eqns
+  for (n, eqns) in newState.map do
+    if !oldState.map.contains n then
+      registerMatchEqns n eqns
 
 private def copyEnvModifications (oldEnv newEnv : Environment) : CoreM Unit := do
   copyNewDeclarations oldEnv newEnv

Aesop/Util/Basic.lean

@@ -60,7 +60,7 @@ def toList [BEq α] [Hashable α] (s : PersistentHashSet α) :
 @[inline]
 def toArray [BEq α] [Hashable α] (s : PersistentHashSet α) :
     Array α :=
-  s.fold (init := Array.mkEmpty s.size) λ as a => as.push a
+  s.fold (init := #[]) λ as a => as.push a
 
 end PersistentHashSet
 

Aesop/Util/UnorderedArraySet.lean

@@ -57,7 +57,7 @@ protected def ofHashSet [Hashable α] (xs : HashSet α) : UnorderedArraySet α :
   ⟨xs.toArray⟩
 
 protected def ofPersistentHashSet [Hashable α] (xs : PersistentHashSet α) : UnorderedArraySet α :=
-  ⟨xs.fold (init := Array.mkEmpty xs.size) λ as a => as.push a⟩
+  ⟨xs.fold (init := #[]) λ as a => as.push a⟩
 
 protected def toArray (s : UnorderedArraySet α) : Array α :=
   s.rep

AesopTest/List.lean

@@ -355,7 +355,7 @@ theorem X.bind_map {g : α → List β} {f : β → γ} :
   ∀ l : List α, map f (l.bind g) = l.bind (λa => (g a).map f) := by
   intro l; induction l <;> aesop
 
-theorem map_bind (g : β → List γ) (f : α → β) :
+theorem map_bind' (g : β → List γ) (f : α → β) :
   ∀ l : List α, (map f l).bind g = l.bind (λ a => g (f a)) := by
   intro l; induction l <;> aesop
 
@@ -674,20 +674,20 @@ 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.
 
-@[simp] theorem map_const (l : List α) (b : β) : map (λ _ => b) l = replicate l.length b := by
+@[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
 
-@[simp] theorem map_replicate (f : α → β) (a : α) (n) : map f (replicate n a) = replicate n (f a) := by
+@[simp] theorem map_replicate' (f : α → β) (a : α) (n) : map f (replicate n a) = replicate n (f a) := by
   induction n <;> aesop
 
 @[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
+@[simp] theorem join_replicate_nil' (n : Nat) : join (replicate n []) = @nil α := by
   induction n <;> aesop
 
 theorem replicate_left_injective {n : Nat} (hn : n ≠ 0) :
@@ -705,7 +705,7 @@ theorem replicate_right_injective (a : α) : Injective (λ n => replicate n a) :
 
 @[simp] theorem replicate_right_inj {a : α} {n m : Nat} :
     replicate n a = replicate m a ↔ n = m := by
-  induction n generalizing m <;> aesop (add 1% cases Nat)
+  aesop
 
 /-! ### pure -/
 
@@ -726,16 +726,16 @@ theorem bind_append (f : α → List β) (l₁ l₂ : List α) :
   (l₁ ++ l₂).bind f = l₁.bind f ++ l₂.bind f := by
   induction l₁ <;> aesop
 
-@[simp] theorem bind_singleton (f : α → List β) (x : α) : [x].bind f = f x := by
+@[simp] theorem bind_singleton'' (f : α → List β) (x : α) : [x].bind f = f x := by
   aesop
 
-@[simp] theorem bind_singleton' (l : List α) : l.bind (λ x => [x]) = l := by
+@[simp] theorem bind_singleton''' (l : List α) : l.bind (λ 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_bind' {α β} (f : α → β) (l : List α) : map f l = l.bind (λ x => [f x]) := by
   induction l <;> aesop
 
-theorem bind_assoc {α β γ : Type u} (l : List α) (f : α → List β) (g : β → List γ) :
+theorem bind_assoc' {α β γ : Type u} (l : List α) (f : α → List β) (g : β → List γ) :
     (l.bind f).bind g = l.bind (λ x => (f x).bind g) :=
   ADMIT
   -- have aux {δ : Type u} (xs ys : List (List δ)) : join (xs ++ ys) = join xs ++ join ys := by
@@ -844,19 +844,19 @@ attribute [-simp] length_reverse
 @[simp] theorem X.length_reverse (l : List α) : length (reverse l) = length l := by
   induction l <;> aesop
 
-theorem map_reverse (f : α → β) (l : List α) : map f (reverse l) = reverse (map f l) := by
+theorem map_reverse' (f : α → β) (l : List α) : map f (reverse l) = reverse (map f l) := by
   induction l <;> aesop
 
 -- attribute [-simp] map_reverseAux
 theorem map_reverse_core (f : α → β) (l₁ l₂ : List α) :
   map f (reverseAux l₁ l₂) = reverseAux (map f l₁) (map f l₂) := by
-  aesop (add norm simp reverse_map)
+  aesop (add norm simp map_reverse')
 
 attribute [-simp] mem_reverse
 @[simp] theorem X.mem_reverse {a : α} {l : List α} : a ∈ reverse l ↔ a ∈ l := by
   induction l <;> aesop
 
-@[simp] theorem reverse_replicate (a : α) (n) : reverse (replicate n a) = replicate n a :=
+@[simp] theorem reverse_replicate' (a : α) (n) : reverse (replicate n a) = replicate n a :=
   ADMIT -- Several missing lemmas.
 
 /-! ### empty -/
@@ -911,7 +911,7 @@ theorem last_mem : ∀ {l : List α} (h : l ≠ []), last l h ∈ l := by
 
 theorem last_replicate_succ (a m : Nat) :
   (replicate m.succ a).last
-    (ne_nil_of_length_eq_succ
+    (ne_nil_of_length_eq_add_one
       (show (replicate m.succ a).length = m.succ by rw [length_replicate])) =
   a := by
   induction m <;> aesop

lake-manifest.json

@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
+   "scope": "",
+   "rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.10.0-rc1