Trigger CI for leanprover/lean4#6334

Batteries/Data/Array/Lemmas.lean

@@ -49,7 +49,7 @@ where
        ((l.toList.drop i).indexOf? a).map (·+i) = (indexOfAux l a i).map Fin.val := by
     rw [indexOfAux]
     if h : i < l.size then
-      rw [List.drop_eq_getElem_cons h, ←getElem_eq_getElem_toList, List.indexOf?_cons]
+      rw [List.drop_eq_getElem_cons h, getElem_toList, List.indexOf?_cons]
       if h' : l[i] == a then
         simp [h, h']
       else

Batteries/Data/Fin/Basic.lean

@@ -17,3 +17,75 @@ alias enum := Array.finRange
 
 @[deprecated (since := "2024-11-15")]
 alias list := List.finRange
+
+/-- Heterogeneous fold over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`, where
+`f 2 : α 3 → α 2`, `f 1 : α 2 → α 1`, etc.
+
+This is the dependent version of `Fin.foldr`. -/
+@[inline] def dfoldr (n : Nat) (α : Fin (n + 1) → Sort _)
+    (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last n)) : α 0 :=
+  loop n (Nat.lt_succ_self n) init where
+  /-- Inner loop for `Fin.dfoldr`.
+    `Fin.dfoldr.loop n α f i h x = f 0 (f 1 (... (f i x)))`  -/
+  @[specialize] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α 0 :=
+    match i with
+    | i + 1 => loop i (Nat.lt_of_succ_lt h) (f ⟨i, Nat.lt_of_succ_lt_succ h⟩ x)
+    | 0 => x
+
+/-- Heterogeneous monadic fold over `Fin n` from right to left:
+```
+Fin.foldrM n f xₙ = do
+  let xₙ₋₁ : α (n-1) ← f (n-1) xₙ
+  let xₙ₋₂ : α (n-2) ← f (n-2) xₙ₋₁
+  ...
+  let x₀ : α 0 ← f 0 x₁
+  pure x₀
+```
+This is the dependent version of `Fin.foldrM`, defined using `Fin.dfoldr`. -/
+@[inline] def dfoldrM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _)
+    (f : ∀ (i : Fin n), α i.succ → m (α i.castSucc)) (init : α (last n)) : m (α 0) :=
+  dfoldr n (fun i => m (α i)) (fun i x => x >>= f i) (pure init)
+
+/-- Heterogeneous fold over `Fin n` from the left: `foldl 3 f x = f 0 (f 1 (f 2 x))`, where
+`f 0 : α 0 → α 1`, `f 1 : α 1 → α 2`, etc.
+
+This is the dependent version of `Fin.foldl`. -/
+@[inline] def dfoldl (n : Nat) (α : Fin (n + 1) → Sort _)
+    (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) :=
+  loop 0 (Nat.zero_lt_succ n) init where
+  /-- Inner loop for `Fin.dfoldl`. `Fin.dfoldl.loop n α f i h x = f n (f (n-1) (... (f i x)))` -/
+  @[semireducible, specialize] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α (last n) :=
+    if h' : i < n then
+      loop (i + 1) (Nat.succ_lt_succ h') (f ⟨i, h'⟩ x)
+    else
+      haveI : ⟨i, h⟩ = last n := by ext; simp; omega
+      _root_.cast (congrArg α this) x
+
+/-- Heterogeneous monadic fold over `Fin n` from left to right:
+```
+Fin.foldlM n f x₀ = do
+  let x₁ : α 1 ← f 0 x₀
+  let x₂ : α 2 ← f 1 x₁
+  ...
+  let xₙ : α n ← f (n-1) xₙ₋₁
+  pure xₙ
+```
+This is the dependent version of `Fin.foldlM`. -/
+@[inline] def dfoldlM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _)
+    (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (init : α 0) : m (α (last n)) :=
+  loop 0 (Nat.zero_lt_succ n) init where
+  /-- Inner loop for `Fin.dfoldlM`.
+    ```
+  Fin.foldM.loop n α f i h xᵢ = do
+    let xᵢ₊₁ : α (i+1) ← f i xᵢ
+    ...
+    let xₙ : α n ← f (n-1) xₙ₋₁
+    pure xₙ
+  ```
+  -/
+  @[semireducible, specialize] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α (last n)) :=
+    if h' : i < n then
+      (f ⟨i, h'⟩ x) >>= loop (i + 1) (Nat.succ_lt_succ h')
+    else
+      haveI : ⟨i, h⟩ = last n := by ext; simp; omega
+      _root_.cast (congrArg (fun i => m (α i)) this) (pure x)

Batteries/Data/Fin/Fold.lean

@@ -1,12 +1,147 @@
 /-
 Copyright (c) 2024 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: François G. Dorais
+Authors: François G. Dorais, Quang Dao
 -/
 import Batteries.Data.List.FinRange
+import Batteries.Data.Fin.Basic
 
 namespace Fin
 
+/-! ### dfoldr -/
+
+theorem dfoldr_loop_zero (f : (i : Fin n) → α i.succ → α i.castSucc) (x) :
+    dfoldr.loop n α f 0 (Nat.zero_lt_succ n) x = x := rfl
+
+theorem dfoldr_loop_succ (f : (i : Fin n) → α i.succ → α i.castSucc) (h : i < n) (x) :
+      dfoldr.loop n α f (i+1) (Nat.add_lt_add_right h 1) x =
+        dfoldr.loop n α f i (Nat.lt_add_right 1 h) (f ⟨i, h⟩ x) := rfl
+
+theorem dfoldr_loop (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (h : i+1 ≤ n+1) (x) :
+      dfoldr.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x =
+        f 0 (dfoldr.loop n (α ∘ succ) (f ·.succ) i h x) := by
+  induction i with
+  | zero => rfl
+  | succ i ih => exact ih ..
+
+@[simp] theorem dfoldr_zero (f : (i : Fin 0) → α i.succ → α i.castSucc) (x) :
+    dfoldr 0 α f x = x := rfl
+
+theorem dfoldr_succ (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x) :
+    dfoldr (n+1) α f x = f 0 (dfoldr n (α ∘ succ) (f ·.succ) x) := dfoldr_loop ..
+
+theorem dfoldr_succ_last (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x) :
+    dfoldr (n+1) α f x = dfoldr n (α ∘ castSucc) (f ·.castSucc) (f (last n) x) := by
+  induction n with
+  | zero => simp only [dfoldr_succ, dfoldr_zero, last, zero_eta]
+  | succ n ih => rw [dfoldr_succ, ih (α := α ∘ succ) (f ·.succ), dfoldr_succ]; congr
+
+theorem dfoldr_eq_dfoldrM (f : (i : Fin n) → α i.succ → α i.castSucc) (x) :
+    dfoldr n α f x = dfoldrM (m:=Id) n α f x := rfl
+
+theorem dfoldr_eq_foldr (f : Fin n → α → α) (x : α) : dfoldr n (fun _ => α) f x = foldr n f x := by
+  induction n with
+  | zero => simp only [dfoldr_zero, foldr_zero]
+  | succ n ih => simp only [dfoldr_succ, foldr_succ, Function.comp_apply, Function.comp_def, ih]
+
+/-! ### dfoldrM -/
+
+@[simp] theorem dfoldrM_zero [Monad m] (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x) :
+    dfoldrM 0 α f x = pure x := rfl
+
+theorem dfoldrM_succ [Monad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc))
+    (x) : dfoldrM (n+1) α f x = dfoldrM n (α ∘ succ) (f ·.succ) x >>= f 0 := dfoldr_succ ..
+
+theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] (f : (i : Fin n) → α → m α) (x : α) :
+    dfoldrM n (fun _ => α) f x = foldrM n f x := by
+  induction n generalizing x with
+  | zero => simp only [dfoldrM_zero, foldrM_zero]
+  | succ n ih => simp only [dfoldrM_succ, foldrM_succ, Function.comp_def, ih]
+
+/-! ### dfoldl -/
+
+theorem dfoldl_loop_lt (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (h : i < n) (x) :
+    dfoldl.loop n α f i (Nat.lt_add_right 1 h) x =
+      dfoldl.loop n α f (i+1) (Nat.add_lt_add_right h 1) (f ⟨i, h⟩ x) := by
+  rw [dfoldl.loop, dif_pos h]
+
+theorem dfoldl_loop_eq (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (x) :
+    dfoldl.loop n α f n (Nat.le_refl _) x = x := by
+  rw [dfoldl.loop, dif_neg (Nat.lt_irrefl _), cast_eq]
+
+@[simp] theorem dfoldl_zero (f : (i : Fin 0) → α i.castSucc → α i.succ) (x) :
+    dfoldl 0 α f x = x := dfoldl_loop_eq ..
+
+theorem dfoldl_loop (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (h : i < n+1) (x) :
+    dfoldl.loop (n+1) α f i (Nat.lt_add_right 1 h) x =
+      dfoldl.loop n (α ∘ succ) (f ·.succ ·) i h (f ⟨i, h⟩ x) := by
+  if h' : i < n then
+    rw [dfoldl_loop_lt _ h _]
+    rw [dfoldl_loop_lt _ h' _, dfoldl_loop]; rfl
+  else
+    cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
+    rw [dfoldl_loop_lt]
+    rw [dfoldl_loop_eq, dfoldl_loop_eq]
+
+theorem dfoldl_succ (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x) :
+    dfoldl (n+1) α f x = dfoldl n (α ∘ succ) (f ·.succ ·) (f 0 x) := dfoldl_loop ..
+
+theorem dfoldl_succ_last (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x) :
+    dfoldl (n+1) α f x = f (last n) (dfoldl n (α ∘ castSucc) (f ·.castSucc ·) x) := by
+  rw [dfoldl_succ]
+  induction n with
+  | zero => simp [dfoldl_succ, last]
+  | succ n ih => rw [dfoldl_succ, @ih (α ∘ succ) (f ·.succ ·), dfoldl_succ]; congr
+
+theorem dfoldl_eq_foldl (f : Fin n → α → α) (x : α) :
+    dfoldl n (fun _ => α) f x = foldl n (fun x i => f i x) x := by
+  induction n generalizing x with
+  | zero => simp only [dfoldl_zero, foldl_zero]
+  | succ n ih =>
+    simp only [dfoldl_succ, foldl_succ, Function.comp_apply, Function.comp_def]
+    congr; simp only [ih]
+
+/-! ### dfoldlM -/
+
+theorem dfoldlM_loop_lt [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (h : i < n) (x) :
+    dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x =
+      (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by
+  rw [dfoldlM.loop, dif_pos h]
+
+theorem dfoldlM_loop_eq [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x) :
+    dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by
+  rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq]
+
+@[simp] theorem dfoldlM_zero [Monad m] (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x) :
+    dfoldlM 0 α f x = pure x := dfoldlM_loop_eq ..
+
+theorem dfoldlM_loop [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (h : i < n+1)
+    (x) : dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x =
+      f ⟨i, h⟩ x >>= (dfoldlM.loop n (α ∘ succ) (f ·.succ ·) i h .) := by
+  if h' : i < n then
+    rw [dfoldlM_loop_lt _ h _]
+    congr; funext
+    rw [dfoldlM_loop_lt _ h' _, dfoldlM_loop]; rfl
+  else
+    cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
+    rw [dfoldlM_loop_lt]
+    congr; funext
+    rw [dfoldlM_loop_eq, dfoldlM_loop_eq]
+
+theorem dfoldlM_succ [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x) :
+    dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) :=
+  dfoldlM_loop ..
+
+theorem dfoldlM_eq_foldlM [Monad m] (f : (i : Fin n) → α → m α) (x : α) :
+    dfoldlM n (fun _ => α) f x = foldlM n (fun x i => f i x) x := by
+  induction n generalizing x with
+  | zero => simp only [dfoldlM_zero, foldlM_zero]
+  | succ n ih =>
+    simp only [dfoldlM_succ, foldlM_succ, Function.comp_apply, Function.comp_def]
+    congr; ext; simp only [ih]
+
+/-! ### `Fin.fold{l/r}{M}` equals `List.fold{l/r}{M}` -/
+
 theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x) :
     foldlM n f x = (List.finRange n).foldlM f x := by
   induction n generalizing x with

Batteries/Data/HashMap/WF.lean

@@ -26,7 +26,7 @@ theorem toList_update (self : Buckets α β) (i d h) :
 theorem exists_of_update (self : Buckets α β) (i d h) :
     ∃ l₁ l₂, self.1.toList = l₁ ++ self.1[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
       (self.update i d h).1.toList = l₁ ++ d :: l₂ := by
-  simp only [Array.length_toList, Array.ugetElem_eq_getElem, Array.getElem_eq_getElem_toList]
+  simp only [Array.length_toList, Array.ugetElem_eq_getElem, Array.getElem_toList]
   exact List.exists_of_set h
 
 theorem update_update (self : Buckets α β) (i d d' h h') :
@@ -46,7 +46,7 @@ theorem WF.mk' [BEq α] [Hashable α] (h) : (Buckets.mk n h : Buckets α β).WF
   refine ⟨fun _ h => ?_, fun i h => ?_⟩
   · simp only [Buckets.mk, mkArray, List.mem_replicate, ne_eq] at h
     simp [h, List.Pairwise.nil]
-  · simp [Buckets.mk, empty', mkArray, Array.getElem_eq_getElem_toList, AssocList.All]
+  · simp [Buckets.mk, empty', mkArray, Array.getElem_toList, AssocList.All]
 
 theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H : buckets.WF)
     (h₁ : ∀ [PartialEquivBEq α] [LawfulHashable α],
@@ -60,7 +60,7 @@ theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H :
     | .inl hl => H.1 _ hl
     | .inr rfl => h₁ (H.1 _ (Array.getElem_mem_toList ..))
   · revert hp
-    simp only [Array.getElem_eq_getElem_toList, toList_update, List.getElem_set,
+    simp only [← Array.getElem_toList, toList_update, List.getElem_set,
       Array.length_toList, update_size]
     split <;> intro hp
     · next eq => exact eq ▸ h₂ (H.2 _ _) _ hp
@@ -110,7 +110,7 @@ where
           List.length_nil, Nat.sum_append, List.sum_cons, Nat.zero_add, Array.length_toList]
         rw [Nat.add_assoc, Nat.add_assoc, Nat.add_assoc]; congr 1
         (conv => rhs; rw [Nat.add_left_comm]); congr 1
-        rw [← Array.getElem_eq_getElem_toList]
+        rw [Array.getElem_toList]
         have := @reinsertAux_size α β _; simp [Buckets.size] at this
         induction source[i].toList generalizing target <;> simp [*, Nat.succ_add]; rfl
     · next H =>
@@ -173,7 +173,7 @@ where
       · match List.mem_or_eq_of_mem_set hl with
         | .inl hl => exact hs₁ _ hl
         | .inr e => exact e ▸ .nil
-      · simp only [Array.length_toList, Array.size_set, Array.getElem_eq_getElem_toList,
+      · simp only [Array.length_toList, Array.size_set, ← Array.getElem_toList,
           Array.toList_set, List.getElem_set]
         split
         · nofun
@@ -371,7 +371,7 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable
     have := H.out.2.1 _ h
     rw [← List.pairwise_map (R := (¬ · == ·))] at this ⊢
     exact this.sublist (H3 l.toList)
-  · simp only [Array.size_mk, List.length_map, Array.length_toList, Array.getElem_eq_getElem_toList,
+  · simp only [Array.size_mk, List.length_map, Array.length_toList, ← Array.getElem_toList,
       List.getElem_map] at h ⊢
     have := H.out.2.2 _ h
     simp only [AssocList.All, List.toList_toAssocList, List.mem_reverse, List.mem_filterMap,

Batteries/Data/MLList/Basic.lean

@@ -174,7 +174,7 @@ def fixl [Monad m] {α β : Type u} (f : α → m (α × List β)) (s : α) : ML
 
 /-- Compute, inside the monad, whether a `MLList` is empty. -/
 def isEmpty [Monad m] (xs : MLList m α) : m (ULift Bool) :=
-  (ULift.up ∘ Option.isSome) <$> uncons xs
+  (ULift.up ∘ Option.isNone) <$> uncons xs
 
 /-- Convert a `List` to a `MLList`. -/
 def ofList : List α → MLList m α

Batteries/Data/UnionFind/Basic.lean

@@ -296,7 +296,6 @@ theorem findAux_s {self : UnionFind} {x : Fin self.size} :
     apply dif_pos
     exact parent'_lt ..
 
-set_option linter.deprecated false in
 theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
     rankD (findAux self x).s i = self.rank i := by
   if h : i < self.size then
@@ -307,11 +306,10 @@ theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
     split <;>
       simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt _ x.2⟩), -Array.get_eq_getElem]
   else
-    simp only [rankD, Array.data_length, Array.get_eq_getElem, rank]
+    simp only [rankD, Array.length_toList, Array.get_eq_getElem, rank]
     rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
 termination_by self.rankMax - self.rank x
 
-set_option linter.deprecated false in
 theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
     parentD (findAux self x).s i =
     if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt _ x.2⟩).s i := by
@@ -321,7 +319,7 @@ theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
   · next h =>
     rw [parentD]; split <;> rename_i h'
     · rw [Array.getElem_modify (by simpa using h')]
-      simp only [Array.data_length, @eq_comm _ i]
+      simp only [Array.length_toList, @eq_comm _ i]
       split <;> simp [← parentD_eq, -Array.get_eq_getElem]
     · rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]
       rw [parentD, dif_neg]; simpa using h'