Trigger CI for leanprover/lean4#6083

.github/workflows/labels-from-status.yml

@@ -34,6 +34,7 @@ jobs:
       if: github.event.pull_request.state == 'closed'
       uses: actions-ecosystem/action-remove-labels@v1
       with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
         labels: |
           WIP
           awaiting-author
@@ -48,6 +49,7 @@ jobs:
         ! contains(github.event.pull_request.labels.*.name, 'WIP')
       uses: actions-ecosystem/action-add-labels@v1
       with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
         labels: WIP
 
     - name: Label unlabeled other PR as awaiting-review
@@ -59,4 +61,5 @@ jobs:
         ! contains(github.event.pull_request.labels.*.name, 'WIP')
       uses: actions-ecosystem/action-add-labels@v1
       with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
         labels: awaiting-review

Batteries/Data/Array/Basic.lean

@@ -137,23 +137,9 @@ This will perform the update destructively provided that `a` has a reference cou
 abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α :=
   a.set i x
 
-/--
-`swapN a i j hi hj` swaps two `Nat` indexed entries in an `Array α`.
-Uses `get_elem_tactic` to supply a proof that the indices are in range.
-`hi` and `hj` are both given a default argument `by get_elem_tactic`.
-This will perform the update destructively provided that `a` has a reference count of 1 when called.
--/
-abbrev swapN (a : Array α) (i j : Nat)
-    (hi : i < a.size := by get_elem_tactic) (hj : j < a.size := by get_elem_tactic) : Array α :=
-  Array.swap a ⟨i,hi⟩ ⟨j, hj⟩
+@[deprecated (since := "2024-11-24")] alias swapN := swap
 
-/--
-`swapAtN a i h x` swaps the entry with index `i : Nat` in the vector for a new entry `x`.
-The old entry is returned alongwith the modified vector.
-Automatically generates proof of `i < a.size` with `get_elem_tactic` where feasible.
--/
-abbrev swapAtN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) :
-    α × Array α := swapAt a ⟨i,h⟩ x
+@[deprecated (since := "2024-11-24")] alias swapAtN := swapAt
 
 @[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 

Batteries/Data/Array/Lemmas.lean

@@ -25,14 +25,6 @@ theorem forIn_eq_forIn_toList [Monad m]
 @[deprecated (since := "2024-09-09")] alias data_zipWith := toList_zipWith
 @[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith
 
-@[simp] theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
-    (as.zipWith bs f).size = min as.size bs.size := by
-  rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
-
-@[simp] theorem size_zip (as : Array α) (bs : Array β) :
-    (as.zip bs).size = min as.size bs.size :=
-  as.size_zipWith bs Prod.mk
-
 /-! ### filter -/
 
 theorem size_filter_le (p : α → Bool) (l : Array α) :
@@ -90,99 +82,139 @@ theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
 
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
 
--- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
--- and am hoping it is not necessary to get Mathlib working again
-
--- /-! ### insertAt -/
-
--- private theorem size_insertAt_loop (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size) :
---     (insertAt.loop as i bs j).size = bs.size := by
---   unfold insertAt.loop
---   split
---   · rw [size_insertAt_loop, size_swap]
---   · rfl
-
--- @[simp] theorem size_insertAt (as : Array α) (i : Fin (as.size+1)) (v : α) :
---     (as.insertAt i v).size = as.size + 1 := by
---   rw [insertAt, size_insertAt_loop, size_push]
-
--- private theorem get_insertAt_loop_lt (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
---     (k) (hk : k < (insertAt.loop as i bs j).size) (h : k < i) :
---     (insertAt.loop as i bs j)[k] = bs[k]'(size_insertAt_loop .. ▸ hk) := by
---   unfold insertAt.loop
---   split
---   · have h1 : k ≠ j - 1 := by omega
---     have h2 : k ≠ j := by omega
---     rw [get_insertAt_loop_lt, getElem_swap, if_neg h1, if_neg h2]
---     exact h
---   · rfl
-
--- private theorem get_insertAt_loop_gt (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
---     (k) (hk : k < (insertAt.loop as i bs j).size) (hgt : j < k) :
---     (insertAt.loop as i bs j)[k] = bs[k]'(size_insertAt_loop .. ▸ hk) := by
---   unfold insertAt.loop
---   split
---   · have h1 : k ≠ j - 1 := by omega
---     have h2 : k ≠ j := by omega
---     rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_neg h2]
---     exact Nat.lt_of_le_of_lt (Nat.pred_le _) hgt
---   · rfl
-
--- private theorem get_insertAt_loop_eq (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
---     (k) (hk : k < (insertAt.loop as i bs j).size) (heq : i = k) (h : i.val ≤ j.val) :
---     (insertAt.loop as i bs j)[k] = bs[j] := by
---   unfold insertAt.loop
---   split
---   · next h =>
---     rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_swap, if_pos rfl]
---     exact heq
---     exact Nat.le_pred_of_lt h
---   · congr; omega
-
--- private theorem get_insertAt_loop_gt_le (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
---     (k) (hk : k < (insertAt.loop as i bs j).size) (hgt : i < k) (hle : k ≤ j) :
---     (insertAt.loop as i bs j)[k] = bs[k-1] := by
---   unfold insertAt.loop
---   split
---   · next h =>
---     if h0 : k = j then
---       cases h0
---       have h1 : j.val ≠ j - 1 := by omega
---       rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_pos rfl]; rfl
---       exact Nat.pred_lt_of_lt hgt
---     else
---       have h1 : k - 1 ≠ j - 1 := by omega
---       have h2 : k - 1 ≠ j := by omega
---       rw [get_insertAt_loop_gt_le, getElem_swap, if_neg h1, if_neg h2]
---       apply Nat.le_of_lt_add_one
---       rw [Nat.sub_one_add_one]
---       exact Nat.lt_of_le_of_ne hle h0
---       exact Nat.not_eq_zero_of_lt h
---       exact hgt
---   · next h =>
---     absurd h
---     exact Nat.lt_of_lt_of_le hgt hle
-
--- theorem getElem_insertAt_lt (as : Array α) (i : Fin (as.size+1)) (v : α)
---     (k) (hlt : k < i.val) {hk : k < (as.insertAt i v).size} {hk' : k < as.size} :
---     (as.insertAt i v)[k] = as[k] := by
---   simp only [insertAt]
---   rw [get_insertAt_loop_lt, getElem_push, dif_pos hk']
---   exact hlt
-
--- theorem getElem_insertAt_gt (as : Array α) (i : Fin (as.size+1)) (v : α)
---     (k) (hgt : k > i.val) {hk : k < (as.insertAt i v).size} {hk' : k - 1 < as.size} :
---     (as.insertAt i v)[k] = as[k - 1] := by
---   simp only [insertAt]
---   rw [get_insertAt_loop_gt_le, getElem_push, dif_pos hk']
---   exact hgt
---   rw [size_insertAt] at hk
---   exact Nat.le_of_lt_succ hk
-
--- theorem getElem_insertAt_eq (as : Array α) (i : Fin (as.size+1)) (v : α)
---     (k) (heq : i.val = k) {hk : k < (as.insertAt i v).size} :
---     (as.insertAt i v)[k] = v := by
---   simp only [insertAt]
---   rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_push_eq]
---   exact heq
---   exact Nat.le_of_lt_succ i.is_lt
+/-! ### insertAt -/
+
+@[simp] private theorem size_insertIdx_loop (as : Array α) (i : Nat) (j : Fin as.size) :
+    (insertIdx.loop i as j).size = as.size := by
+  unfold insertIdx.loop
+  split
+  · rw [size_insertIdx_loop, size_swap]
+  · rfl
+
+@[simp] theorem size_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
+    (as.insertIdx i v).size = as.size + 1 := by
+  rw [insertIdx, size_insertIdx_loop, size_push]
+
+@[deprecated size_insertIdx (since := "2024-11-20")] alias size_insertAt := size_insertIdx
+
+theorem getElem_insertIdx_loop_lt {as : Array α} {i : Nat} {j : Fin as.size} {k : Nat} {h}
+    (w : k < i) :
+    (insertIdx.loop i as j)[k] = as[k]'(by simpa using h) := by
+  unfold insertIdx.loop
+  split <;> rename_i h₁
+  · simp only
+    rw [getElem_insertIdx_loop_lt w]
+    rw [getElem_swap]
+    split <;> rename_i h₂
+    · simp_all
+      omega
+    · split <;> rename_i h₃
+      · omega
+      · simp_all
+  · rfl
+
+theorem getElem_insertIdx_loop_eq {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {h} :
+    (insertIdx.loop i as ⟨j, hj⟩)[i] = if i ≤ j then as[j] else as[i]'(by simpa using h) := by
+  unfold insertIdx.loop
+  split <;> rename_i h₁
+  · simp at h₁
+    have : j - 1 < j := by omega
+    rw [getElem_insertIdx_loop_eq]
+    rw [getElem_swap]
+    simp
+    split <;> rename_i h₂
+    · rw [if_pos (by omega)]
+    · omega
+  · simp at h₁
+    by_cases h' : i = j
+    · simp [h']
+    · have t : ¬ i ≤ j := by omega
+      simp [t]
+
+theorem getElem_insertIdx_loop_gt {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size}
+    {k : Nat} {h} (w : i < k) :
+    (insertIdx.loop i as ⟨j, hj⟩)[k] =
+      if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by
+  unfold insertIdx.loop
+  split <;> rename_i h₁
+  · simp only
+    simp only at h₁
+    have : j - 1 < j := by omega
+    rw [getElem_insertIdx_loop_gt w]
+    rw [getElem_swap]
+    split <;> rename_i h₂
+    · rw [if_neg (by omega), if_neg (by omega)]
+      have t : k ≤ j := by omega
+      simp [t]
+    · rw [getElem_swap]
+      rw [if_neg (by omega)]
+      split <;> rename_i h₃
+      · simp [h₃]
+      · have t : ¬ k ≤ j := by omega
+        simp [t]
+  · simp only at h₁
+    have t : ¬ k ≤ j := by omega
+    simp [t]
+
+theorem getElem_insertIdx_loop {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {k : Nat} {h} :
+    (insertIdx.loop i as ⟨j, hj⟩)[k] =
+      if h₁ : k < i then
+        as[k]'(by simpa using h)
+      else
+        if h₂ : k = i then
+          if i ≤ j then as[j] else as[i]'(by simpa [h₂] using h)
+        else
+          if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by
+  split <;> rename_i h₁
+  · rw [getElem_insertIdx_loop_lt h₁]
+  · split <;> rename_i h₂
+    · subst h₂
+      rw [getElem_insertIdx_loop_eq]
+    · rw [getElem_insertIdx_loop_gt (by omega)]
+
+theorem getElem_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
+    (k) (h' : k < (as.insertIdx i v).size) :
+    (as.insertIdx i v)[k] =
+      if h₁ : k < i then
+        as[k]'(by omega)
+      else
+        if h₂ : k = i then
+          v
+        else
+          as[k - 1]'(by simp at h'; omega) := by
+  unfold insertIdx
+  rw [getElem_insertIdx_loop]
+  simp only [size_insertIdx] at h'
+  replace h' : k ≤ as.size := by omega
+  simp only [getElem_push, h, ↓reduceIte, Nat.lt_irrefl, ↓reduceDIte, h', dite_eq_ite]
+  split <;> rename_i h₁
+  · rw [dif_pos (by omega)]
+  · split <;> rename_i h₂
+    · simp [h₂]
+    · split <;> rename_i h₃
+      · rfl
+      · omega
+
+theorem getElem_insertIdx_lt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
+    (k) (h' : k < (as.insertIdx i v).size) (h : k < i) :
+    (as.insertIdx i v)[k] = as[k] := by
+  simp [getElem_insertIdx, h]
+
+@[deprecated getElem_insertIdx_lt (since := "2024-11-20")] alias getElem_insertAt_lt :=
+getElem_insertIdx_lt
+
+theorem getElem_insertIdx_eq (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
+    (as.insertIdx i v)[i]'(by simp; omega) = v := by
+  simp [getElem_insertIdx, h]
+
+@[deprecated getElem_insertIdx_eq (since := "2024-11-20")] alias getElem_insertAt_eq :=
+getElem_insertIdx_eq
+
+theorem getElem_insertIdx_gt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
+    (k) (h' : k < (as.insertIdx i v).size) (h : i < k) :
+    (as.insertIdx i v)[k] = as[k-1]'(by simp at h'; omega) := by
+  rw [getElem_insertIdx]
+  rw [dif_neg (by omega), dif_neg (by omega)]
+
+@[deprecated getElem_insertIdx_gt (since := "2024-11-20")] alias getElem_insertAt_gt :=
+getElem_insertIdx_gt

Batteries/Data/BinaryHeap.lean

@@ -67,9 +67,9 @@ def heapifyUp (lt : α → α → Bool) (a : Vector α sz) (i : Fin sz) :
   match i with
   | ⟨0, _⟩ => a
   | ⟨i'+1, hi⟩ =>
-    let j := ⟨i'/2, by get_elem_tactic⟩
+    let j := i'/2
     if lt a[j] a[i] then
-      heapifyUp lt (a.swap i j) j
+      heapifyUp lt (a.swap i j) ⟨j, by get_elem_tactic⟩
     else a
 
 /-- `O(1)`. Build a new empty heap. -/
@@ -107,7 +107,7 @@ def popMax (self : BinaryHeap α lt) : BinaryHeap α lt :=
   if h0 : self.size = 0 then self else
     have hs : self.size - 1 < self.size := Nat.pred_lt h0
     have h0 : 0 < self.size := Nat.zero_lt_of_ne_zero h0
-    let v := self.vector.swap ⟨_, h0⟩ ⟨_, hs⟩ |>.pop
+    let v := self.vector.swap _ _ h0 hs |>.pop
     if h : 0 < self.size - 1 then
       ⟨heapifyDown lt v ⟨0, h⟩ |>.toArray⟩
     else
@@ -136,7 +136,7 @@ def insertExtractMax (self : BinaryHeap α lt) (x : α) : α × BinaryHeap α lt
   | none => (x, self)
   | some m =>
     if lt x m then
-      let v := self.vector.set ⟨0, size_pos_of_max e⟩ x
+      let v := self.vector.set 0 x (size_pos_of_max e)
       (m, ⟨heapifyDown lt v ⟨0, size_pos_of_max e⟩ |>.toArray⟩)
     else (x, self)
 
@@ -145,7 +145,7 @@ def replaceMax (self : BinaryHeap α lt) (x : α) : Option α × BinaryHeap α l
   match e : self.max with
   | none => (none, ⟨self.vector.push x |>.toArray⟩)
   | some m =>
-    let v := self.vector.set ⟨0, size_pos_of_max e⟩ x
+    let v := self.vector.set 0 x (size_pos_of_max e)
     (some m, ⟨heapifyDown lt v ⟨0, size_pos_of_max e⟩ |>.toArray⟩)
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `x ≤ self.get i`. -/

Batteries/Data/Range/Lemmas.lean

@@ -45,11 +45,6 @@ theorem mem_range'_elems (r : Range) (h : x ∈ List.range' r.start r.numElems r
     refine Nat.not_le.1 fun h =>
       Nat.not_le.2 h' <| (numElems_le_iff (Nat.pos_of_ne_zero step0)).2 h
 
--- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
--- and am hoping it is not necessary to get Mathlib working again
-
-/-
-
 theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
     forIn' r init f =
@@ -62,12 +57,15 @@ theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
   suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _
   intro H; dsimp only [forIn', Range.forIn']
   if h : start < stop then
-    simp [numElems, Nat.not_le.2 h, L]; split
+    simp only [numElems, Nat.not_le.2 h, ↓reduceIte, L]; split
     · subst step
       suffices ∀ n H init,
           forIn'.loop start stop 0 f n start (Nat.le_refl _) init =
           forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ ..
-      intro n; induction n with (intro H init; unfold forIn'.loop; simp [*])
+      intro n; induction n with
+        (intro H init
+         unfold forIn'.loop
+         simp only [↓reduceDIte, Nat.add_zero, List.pmap, List.forIn_cons, List.forIn_nil, h])
       | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
     · next step0 =>
       have hstep := Nat.pos_of_ne_zero step0
@@ -89,10 +87,15 @@ theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
           have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..))
             (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by
               rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff]
-          have := h2 0; simp at this
-          rw [forIn'.loop]; simp [this, ih]; rfl
+          have := h2 0
+          simp only [Nat.mul_zero, Nat.add_zero, Nat.le_zero_eq, Nat.add_one_ne_zero, iff_false,
+            Nat.not_le] at this
+          rw [forIn'.loop]
+          simp only [this, ↓reduceDIte, ih, List.pmap, List.forIn_cons]
+          rfl
   else
-    simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
+    simp only [numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), List.range'_zero,
+      List.pmap, List.forIn_nil, L]
     cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
 
 theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
@@ -102,5 +105,3 @@ theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
   · simp [forIn, forIn']
   · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
     intro L; induction L generalizing init <;> intro H <;> simp [*]
-
--/