Merge remote-tracking branch 'origin/master' into simplc

.github/dependabot.yml

@@ -0,0 +1,8 @@
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "monthly"
+    commit-message:
+      prefix: "chore: CI"

.github/workflows/actionlint.yml

@@ -17,6 +17,6 @@ jobs:
     - name: Checkout
       uses: actions/checkout@v4
     - name: actionlint
-      uses: raven-actions/actionlint@v1
+      uses: raven-actions/actionlint@v2
       with:
         pyflakes: false # we do not use python scripts

.github/workflows/ci.yml

@@ -492,7 +492,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -536,7 +536,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
         with:
           body_path: diff.md
           prerelease: true

.github/workflows/nix-ci.yml

@@ -129,7 +129,7 @@ jobs:
           python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT"
           echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
       - name: Publish manual to Netlify
-        uses: nwtgck/actions-netlify@v2.0
+        uses: nwtgck/actions-netlify@v3.0
         id: publish-manual
         with:
           publish-dir: ./dist

.github/workflows/pr-release.yml

@@ -60,7 +60,7 @@ jobs:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.

.github/workflows/stale.yml

@@ -11,7 +11,7 @@ jobs:
   stale:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/stale@v8
+      - uses: actions/stale@v9
         with:
           days-before-stale: -1
           days-before-pr-stale: 30

src/Init/Data/Array/Bootstrap.lean

@@ -23,7 +23,7 @@ theorem foldlM_eq_foldlM_toList.aux [Monad m]
   · 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]
-    rw (occs := .pos [2]) [← List.get_drop_eq_drop _ _ ‹_›]
+    rw (occs := .pos [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 

src/Init/Data/Array/GetLit.lean

@@ -41,6 +41,6 @@ where
   getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
     rfl
   go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
-    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.get_drop_eq_drop, *]
+    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.getElem_cons_drop_succ_eq_drop, *]
 
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -10,6 +10,7 @@ import Init.Data.List.Monadic
 import Init.Data.List.Range
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
+import Init.Data.List.Nat.Erase
 import Init.Data.List.Monadic
 import Init.Data.List.OfFn
 import Init.Data.Array.Mem
@@ -246,7 +247,7 @@ where
   aux (i r) :
       mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
     unfold mapM.map; split
-    · rw [← List.get_drop_eq_drop _ i ‹_›]
+    · rw [← List.getElem_cons_drop_succ_eq_drop ‹_›]
       simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
         pure_bind]
       rfl
@@ -1460,6 +1461,10 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
+theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} :
+    a.feraseIdx i = a.eraseIdx i.1 := by
+  simp [eraseIdx]
+
 end Array
 
 open Array
@@ -1611,14 +1616,72 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   apply ext'
   simp
 
-@[simp] theorem toArray_extract (l : List α) (start stop : Nat) :
+@[simp] theorem extract_toArray (l : List α) (start stop : Nat) :
     l.toArray.extract start stop = ((l.drop start).take (stop - start)).toArray := by
   apply ext'
   simp
 
 @[simp] theorem toArray_ofFn (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f := by
   ext <;> simp
 
+theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
+    takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
+  rw [takeWhile.go, takeWhile.go]
+  simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+    getElem_toArray, getElem_cons_succ]
+  split
+  rw [takeWhile_go_succ]
+  rfl
+
+theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
+    Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by
+  induction l generalizing i r with
+  | nil => simp [takeWhile.go]
+  | cons a l ih =>
+    rw [takeWhile.go]
+    cases i with
+    | zero =>
+      simp [takeWhile_go_succ, ih, takeWhile_cons]
+      split <;> simp
+    | succ i =>
+      simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+        getElem_toArray, getElem_cons_succ, drop_succ_cons]
+      split <;> rename_i h₁
+      · rw [takeWhile_go_succ, ih]
+        rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
+        split <;> simp_all
+      · simp_all [drop_eq_nil_of_le]
+
+@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
+    l.toArray.takeWhile p = (l.takeWhile p).toArray := by
+  simp [Array.takeWhile, takeWhile_go_toArray]
+
+@[simp] theorem feraseIdx_toArray (l : List α) (i : Fin l.toArray.size) :
+    l.toArray.feraseIdx i = (l.eraseIdx i).toArray := by
+  rw [feraseIdx]
+  split <;> rename_i h
+  · rw [feraseIdx_toArray]
+    simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]
+    rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]
+    simp
+  · rcases i with ⟨i, w⟩
+    simp at h w
+    have t : i = l.length - 1 := by omega
+    simp [t]
+termination_by l.length - i
+decreasing_by
+  rename_i h
+  simp at h
+  simp
+  omega
+
+@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) :
+    l.toArray.eraseIdx i = (l.eraseIdx i).toArray := by
+  rw [Array.eraseIdx]
+  split
+  · simp
+  · simp_all [eraseIdx_eq_self.2]
+
 end List
 
 namespace Array
@@ -1629,6 +1692,20 @@ namespace Array
 @[simp] theorem toList_ofFn (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f := by
   apply List.ext_getElem <;> simp
 
+@[simp] theorem toList_takeWhile (p : α → Bool) (as : Array α) :
+    (as.takeWhile p).toList = as.toList.takeWhile p := by
+  induction as; simp
+
+@[simp] theorem toList_feraseIdx (as : Array α) (i : Fin as.size) :
+    (as.feraseIdx i).toList = as.toList.eraseIdx i.1 := by
+  induction as
+  simp
+
+@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) :
+    (as.eraseIdx i).toList = as.toList.eraseIdx i := by
+  induction as
+  simp
+
 end Array
 
 /-! ### Deprecations -/

src/Init/Data/List/Attach.lean

@@ -169,6 +169,13 @@ theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : Li
     (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ [] := by
   simp
 
+theorem pmap_eq_self {l : List α} {p : α → Prop} (hp : ∀ (a : α), a ∈ l → p a)
+    (f : (a : α) → p a → α) : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by
+  rw [pmap_eq_map_attach]
+  conv => lhs; rhs; rw [← attach_map_subtype_val l]
+  rw [map_inj_left]
+  simp
+
 @[simp]
 theorem attach_eq_nil_iff {l : List α} : l.attach = [] ↔ l = [] :=
   pmap_eq_nil_iff

src/Init/Data/List/Nat/Erase.lean

@@ -64,3 +64,82 @@ theorem getElem_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : j < (l.era
     (l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
   rw [getElem_eraseIdx, dif_neg]
   omega
+
+theorem eraseIdx_set_eq {l : List α} {i : Nat} {a : α} :
+    (l.set i a).eraseIdx i = l.eraseIdx i := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    rw [getElem_eraseIdx, getElem_eraseIdx]
+    split <;>
+    · rw [getElem_set_ne]
+      omega
+
+theorem eraseIdx_set_lt {l : List α} {i : Nat} {j : Nat} {a : α} (h : j < i) :
+    (l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    simp only [length_eraseIdx, length_set] at h₁
+    simp only [getElem_eraseIdx, getElem_set]
+    split
+    · split
+      · split
+        · rfl
+        · omega
+      · split
+        · omega
+        · rfl
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : i - 1 ≠ n := by omega
+        simp [t]
+
+theorem eraseIdx_set_gt {l : List α} {i : Nat} {j : Nat} {a : α} (h : i < j) :
+    (l.set i a).eraseIdx j = (l.eraseIdx j).set i a := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+  · intro n h₁ h₂
+    simp only [length_eraseIdx, length_set] at h₁
+    simp only [getElem_eraseIdx, getElem_set]
+    split
+    · rfl
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : i ≠ n := by omega
+        simp [t]
+
+@[simp] theorem set_getElem_succ_eraseIdx_succ
+    {l : List α} {i : Nat} (h : i + 1 < l.length) :
+    (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i := by
+  apply ext_getElem
+  · simp only [length_set, length_eraseIdx, h, ↓reduceIte]
+    rw [if_pos]
+    omega
+  · intro n h₁ h₂
+    simp [getElem_set, getElem_eraseIdx]
+    split
+    · split
+      · omega
+      · simp_all
+    · split
+      · split
+        · rfl
+        · omega
+      · have t : ¬ n < i := by omega
+        simp [t]
+
+@[simp] theorem eraseIdx_length_sub_one (l : List α) :
+    (l.eraseIdx (l.length - 1)) = l.dropLast := by
+  apply ext_getElem
+  · simp [length_eraseIdx]
+    omega
+  · intro n h₁ h₂
+    rw [getElem_eraseIdx_of_lt, getElem_dropLast]
+    simp_all
+
+end List

src/Init/Data/List/TakeDrop.lean

@@ -190,7 +190,7 @@ theorem set_drop {l : List α} {n m : Nat} {a : α} :
 theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
     (l.take i).concat l[i] = l.take (i+1) :=
   Eq.symm <| (append_left_inj _).1 <| (take_append_drop (i+1) l).trans <| by
-    rw [concat_eq_append, append_assoc, singleton_append, get_drop_eq_drop, take_append_drop]
+    rw [concat_eq_append, append_assoc, singleton_append, getElem_cons_drop_succ_eq_drop, take_append_drop]
 
 @[deprecated take_succ_cons (since := "2024-07-25")]
 theorem take_cons_succ : (a::as).take (i+1) = a :: as.take i := rfl

src/Init/Data/Option/Lemmas.lean

@@ -374,9 +374,15 @@ end choice
 
 -- See `Init.Data.Option.List` for lemmas about `toList`.
 
-@[simp] theorem or_some : (some a).or o = some a := rfl
+@[simp] theorem some_or : (some a).or o = some a := rfl
 @[simp] theorem none_or : none.or o = o := rfl
 
+@[deprecated some_or (since := "2024-11-03")] theorem or_some : (some a).or o = some a := rfl
+
+/-- This will be renamed to `or_some` once the existing deprecated lemma is removed. -/
+@[simp] theorem or_some' {o : Option α} : o.or (some a) = o.getD a := by
+  cases o <;> rfl
+
 theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
   cases o <;> rfl
 

src/Init/GetElem.lean

@@ -211,10 +211,13 @@ instance : GetElem (List α) Nat α fun as i => i < as.length where
   | _ :: _, 0, _ => .head ..
   | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
 
-theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
+theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.length) :
+    as[i] :: as.drop (i+1) = as.drop i :=
   match as, i with
   | _::_, 0   => rfl
-  | _::_, i+1 => get_drop_eq_drop _ i _
+  | _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) _
+
+@[deprecated (since := "2024-11-05")] abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop
 
 end List