fix: proofs on months and removed Lean.Data.Rat from Lean.Dat

.github/workflows/pr-body.yml

@@ -1,6 +1,7 @@
 name: Check PR body for changelog convention
 
 on:
+  merge_group:
   pull_request:
     types: [opened, synchronize, reopened, edited, labeled, converted_to_draft, ready_for_review]
 
@@ -9,6 +10,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check PR body
+        if: github.event_name == 'pull_request'
         uses: actions/github-script@v7
         with:
           script: |

src/Init/Core.lean

@@ -1922,12 +1922,12 @@ represents an element of `Squash α` the same as `α` itself
 `Squash.lift` will extract a value in any subsingleton `β` from a function on `α`,
 while `Nonempty.rec` can only do the same when `β` is a proposition.
 -/
-def Squash (α : Type u) := Quot (fun (_ _ : α) => True)
+def Squash (α : Sort u) := Quot (fun (_ _ : α) => True)
 
 /-- The canonical quotient map into `Squash α`. -/
-def Squash.mk {α : Type u} (x : α) : Squash α := Quot.mk _ x
+def Squash.mk {α : Sort u} (x : α) : Squash α := Quot.mk _ x
 
-theorem Squash.ind {α : Type u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
+theorem Squash.ind {α : Sort u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
   Quot.ind h
 
 /-- If `β` is a subsingleton, then a function `α → β` lifts to `Squash α → β`. -/

src/Init/Data.lean

@@ -42,3 +42,4 @@ import Init.Data.PLift
 import Init.Data.Zero
 import Init.Data.NeZero
 import Init.Data.Function
+import Init.Data.RArray

src/Init/Data/Array.lean

@@ -18,3 +18,4 @@ import Init.Data.Array.Bootstrap
 import Init.Data.Array.GetLit
 import Init.Data.Array.MapIdx
 import Init.Data.Array.Set
+import Init.Data.Array.Monadic

src/Init/Data/Array/Attach.lean

@@ -43,6 +43,13 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
     l.attach.toList = l.toList.attachWith (· ∈ l) (by simp [mem_toList]) := by
   simp [attach]
 
+@[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
+    l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
+      l.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+  simp only [List.attachWith, List.attach, List.map_pmap]
+  apply List.pmap_congr_left
+  simp
+
 /-! ## unattach
 
 `Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
@@ -83,7 +90,7 @@ def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (
 
 @[simp] theorem unattach_attach {l : Array α} : l.attach.unattach = l := by
   cases l
-  simp
+  simp only [List.attach_toArray, List.unattach_toArray, List.unattach_attachWith]
 
 @[simp] theorem unattach_attachWith {p : α → Prop} {l : Array α}
     {H : ∀ a ∈ l, p a} :

src/Init/Data/Array/Basic.lean

@@ -166,13 +166,14 @@ count of 1 when called.
 -/
 @[extern "lean_array_fswap"]
 def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
-  let v₁ := a.get i
-  let v₂ := a.get j
+  let v₁ := a[i]
+  let v₂ := a[j]
   let a'  := a.set i v₂
   a'.set j v₁ (Nat.lt_of_lt_of_eq j.isLt (size_set a i v₂ _).symm)
 
 @[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
-  show ((a.set i (a.get j)).set j (a.get i) (Nat.lt_of_lt_of_eq j.isLt (size_set a i (a.get j) _).symm)).size = a.size
+  show ((a.set i a[j]).set j a[i]
+    (Nat.lt_of_lt_of_eq j.isLt (size_set a i a[j] _).symm)).size = a.size
   rw [size_set, size_set]
 
 /--
@@ -246,10 +247,10 @@ def get? (a : Array α) (i : Nat) : Option α :=
   if h : i < a.size then some a[i] else none
 
 def back? (a : Array α) : Option α :=
-  a.get? (a.size - 1)
+  a[a.size - 1]?
 
 @[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
-  let e := a.get i
+  let e := a[i]
   let a := a.set i v
   (e, a)
 
@@ -273,24 +274,22 @@ def take (a : Array α) (n : Nat) : Array α :=
 @[inline]
 unsafe def modifyMUnsafe [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
   if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩
-    let v                := a.get idx
+    let v                := a[i]
     -- Replace a[i] by `box(0)`.  This ensures that `v` remains unshared if possible.
     -- Note: we assume that arrays have a uniform representation irrespective
     -- of the element type, and that it is valid to store `box(0)` in any array.
-    let a'               := a.set idx (unsafeCast ())
+    let a'               := a.set i (unsafeCast ())
     let v ← f v
-    pure <| a'.set idx v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
+    pure <| a'.set i v (Nat.lt_of_lt_of_eq h (size_set a ..).symm)
   else
     pure a
 
 @[implemented_by modifyMUnsafe]
 def modifyM [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
   if h : i < a.size then
-    let idx := ⟨i, h⟩
-    let v   := a.get idx
+    let v   := a[i]
     let v ← f v
-    pure <| a.set idx v
+    pure <| a.set i v
   else
     pure a
 
@@ -443,6 +442,8 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α 
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
+@[deprecated mapM (since := "2024-11-11")] abbrev sequenceMap := @mapM
+
 /-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
 def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
@@ -455,30 +456,30 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
         apply Nat.le_add_right
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get ⟨j, j_lt⟩)))
+      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get j j_lt)))
   map as.size 0 rfl (mkEmpty as.size)
 
 @[inline]
-def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Nat → α → m β) : m (Array β) :=
+def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) :=
   as.mapFinIdxM fun i a => f i a
 
 @[inline]
-def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) := do
+def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do
   for a in as do
     match (← f a) with
     | some b => return b
     | _      => pure ⟨⟩
   return none
 
 @[inline]
-def findM? {α : Type} {m : Type → Type} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α) := do
+def findM? {α : Type} {m : Type → Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := do
   for a in as do
     if (← p a) then
       return a
   return none
 
 @[inline]
-def findIdxM? [Monad m] (as : Array α) (p : α → m Bool) : m (Option Nat) := do
+def findIdxM? [Monad m] (p : α → m Bool) (as : Array α) : m (Option Nat) := do
   let mut i := 0
   for a in as do
     if (← p a) then
@@ -530,7 +531,7 @@ def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
   return !(← as.anyM (start := start) (stop := stop) fun v => return !(← p v))
 
 @[inline]
-def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) :=
+def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) :=
   let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β)
     | 0,   _ => pure none
     | i+1, h => do
@@ -544,7 +545,7 @@ def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
   find as.size (Nat.le_refl _)
 
 @[inline]
-def findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α) :=
+def findRevM? {α : Type} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) :=
   as.findSomeRevM? fun a => return if (← p a) then some a else none
 
 @[inline]
@@ -573,37 +574,37 @@ def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → 
   Id.run <| as.mapFinIdxM f
 
 @[inline]
-def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Nat → α → β) : Array β :=
+def mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) : Array β :=
   Id.run <| as.mapIdxM f
 
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
 def zipWithIndex (arr : Array α) : Array (α × Nat) :=
   arr.mapIdx fun i a => (a, i)
 
 @[inline]
-def find? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
+def find? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
   Id.run <| as.findM? p
 
 @[inline]
-def findSome? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β :=
+def findSome? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
   Id.run <| as.findSomeM? f
 
 @[inline]
-def findSome! {α : Type u} {β : Type v} [Inhabited β] (a : Array α) (f : α → Option β) : β :=
-  match findSome? a f with
+def findSome! {α : Type u} {β : Type v} [Inhabited β] (f : α → Option β) (a : Array α) : β :=
+  match a.findSome? f with
   | some b => b
   | none   => panic! "failed to find element"
 
 @[inline]
-def findSomeRev? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β :=
+def findSomeRev? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
   Id.run <| as.findSomeRevM? f
 
 @[inline]
-def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
+def findRev? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
   Id.run <| as.findRevM? p
 
 @[inline]
-def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
+def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   loop (j : Nat) :=
     if h : j < as.size then
@@ -618,8 +619,7 @@ def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
   if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩;
-    if a.get idx == v then some idx
+    if a[i] == v then some ⟨i, h⟩
     else indexOfAux a v (i+1)
   else none
 decreasing_by simp_wf; decreasing_trivial_pre_omega
@@ -744,7 +744,7 @@ where
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
-    if p (as.get ⟨as.size - 1, Nat.sub_lt h (by decide)⟩) then
+    if p (as[as.size - 1]'(Nat.sub_lt h (by decide))) then
       popWhile p as.pop
     else
       as
@@ -756,7 +756,7 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   go (i : Nat) (r : Array α) : Array α :=
     if h : i < as.size then
-      let a := as.get ⟨i, h⟩
+      let a := as[i]
       if p a then
         go (i+1) (r.push a)
       else

src/Init/Data/Array/Bootstrap.lean

@@ -15,26 +15,26 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-theorem foldlM_eq_foldlM_toList.aux [Monad m]
+theorem foldlM_toList.aux [Monad m]
     (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
     foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b := by
   unfold foldlM.loop
   split; split
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
-    simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
+    simp [foldlM_toList.aux f arr i (j+1) H]
     rw (occs := .pos [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
-theorem foldlM_eq_foldlM_toList [Monad m]
+@[simp] theorem foldlM_toList [Monad m]
     (f : β → α → m β) (init : β) (arr : Array α) :
-    arr.foldlM f init = arr.toList.foldlM f init := by
-  simp [foldlM, foldlM_eq_foldlM_toList.aux]
+    arr.toList.foldlM f init = arr.foldlM f init := by
+  simp [foldlM, foldlM_toList.aux]
 
-theorem foldl_eq_foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
-    arr.foldl f init = arr.toList.foldl f init :=
-  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_toList ..
+@[simp] theorem foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
+    arr.toList.foldl f init = arr.foldl f init :=
+  List.foldl_eq_foldlM .. ▸ foldlM_toList ..
 
 theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
     (f : α → β → m β) (arr : Array α) (init : β) (i h) :
@@ -51,23 +51,23 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
   match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
-theorem foldrM_eq_foldrM_toList [Monad m]
+@[simp] theorem foldrM_toList [Monad m]
     (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.toList.foldrM f init := by
+    arr.toList.foldrM f init = arr.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
 
-theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
-    arr.foldr f init = arr.toList.foldr f init :=
-  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_toList ..
+@[simp] theorem foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
+    arr.toList.foldr f init = arr.foldr f init :=
+  List.foldr_eq_foldrM .. ▸ foldrM_toList ..
 
 @[simp] theorem push_toList (arr : Array α) (a : α) : (arr.push a).toList = arr.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
 @[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.toList ++ l := by
-  simp [toListAppend, foldr_eq_foldr_toList]
+  simp [toListAppend, ← foldr_toList]
 
 @[simp] theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList := by
-  simp [toListImpl, foldr_eq_foldr_toList]
+  simp [toListImpl, ← foldr_toList]
 
 @[simp] theorem pop_toList (arr : Array α) : arr.pop.toList = arr.toList.dropLast := rfl
 
@@ -76,7 +76,7 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
 @[simp] theorem toList_append (arr arr' : Array α) :
     (arr ++ arr').toList = arr.toList ++ arr'.toList := by
   rw [← append_eq_append]; unfold Array.append
-  rw [foldl_eq_foldl_toList]
+  rw [← foldl_toList]
   induction arr'.toList generalizing arr <;> simp [*]
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
@@ -98,20 +98,44 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing arr <;> simp [*]
 
-@[deprecated foldlM_eq_foldlM_toList (since := "2024-09-09")]
-abbrev foldlM_eq_foldlM_data := @foldlM_eq_foldlM_toList
+@[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")]
+theorem foldrM_eq_foldrM_toList [Monad m]
+    (f : α → β → m β) (init : β) (arr : Array α) :
+    arr.foldrM f init = arr.toList.foldrM f init := by
+  simp
+
+@[deprecated "Use the reverse direction of `foldlM_toList`." (since := "2024-11-13")]
+theorem foldlM_eq_foldlM_toList [Monad m]
+    (f : β → α → m β) (init : β) (arr : Array α) :
+    arr.foldlM f init = arr.toList.foldlM f init:= by
+  simp
+
+@[deprecated "Use the reverse direction of `foldr_toList`." (since := "2024-11-13")]
+theorem foldr_eq_foldr_toList
+    (f : α → β → β) (init : β) (arr : Array α) :
+    arr.foldr f init = arr.toList.foldr f init := by
+  simp
+
+@[deprecated "Use the reverse direction of `foldl_toList`." (since := "2024-11-13")]
+theorem foldl_eq_foldl_toList
+    (f : β → α → β) (init : β) (arr : Array α) :
+    arr.foldl f init = arr.toList.foldl f init:= by
+  simp
+
+@[deprecated foldlM_toList (since := "2024-09-09")]
+abbrev foldlM_eq_foldlM_data := @foldlM_toList
 
-@[deprecated foldl_eq_foldl_toList (since := "2024-09-09")]
-abbrev foldl_eq_foldl_data := @foldl_eq_foldl_toList
+@[deprecated foldl_toList (since := "2024-09-09")]
+abbrev foldl_eq_foldl_data := @foldl_toList
 
 @[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
 abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
 
-@[deprecated foldrM_eq_foldrM_toList (since := "2024-09-09")]
-abbrev foldrM_eq_foldrM_data := @foldrM_eq_foldrM_toList
+@[deprecated foldrM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_foldrM_data := @foldrM_toList
 
-@[deprecated foldr_eq_foldr_toList (since := "2024-09-09")]
-abbrev foldr_eq_foldr_data := @foldr_eq_foldr_toList
+@[deprecated foldr_toList (since := "2024-09-09")]
+abbrev foldr_eq_foldr_data := @foldr_toList
 
 @[deprecated push_toList (since := "2024-09-09")]
 abbrev push_data := @push_toList