Merge remote-tracking branch 'upstream/main' into binaryRec

.github/workflows/build.yml

@@ -14,26 +14,14 @@ jobs:
     name: Build
     runs-on: ubuntu-latest
     steps:
-      - name: install elan
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
       - uses: actions/checkout@v4
 
-      - name: build batteries
-        id: build
-        run: lake build -Kwerror
-
-      - name: test batteries
-        if: steps.build.outcome == 'success'
-        run: lake test
-
-      - name: lint batteries
-        if: steps.build.outcome == 'success'
-        run: make lint
+      - id: lean-action
+        name: build, test, and lint batteries
+        uses: leanprover/lean-action@v1-beta
+        with:
+          build-args: '-Kwerror'
+          lint-module: 'Batteries'
 
       - name: Check that all files are imported
         run: lake env lean scripts/check_imports.lean

Batteries/CodeAction/Deprecated.lean

@@ -29,10 +29,10 @@ def deprecatedCodeActionProvider : CodeActionProvider := fun params snap => do
   let mut i := 0
   let doc ← readDoc
   let mut msgs := #[]
-  for m in snap.msgLog.msgs do
+  for m in snap.msgLog.toList do
     if m.data.isDeprecationWarning then
       if h : _ then
-        msgs := msgs.push (snap.cmdState.messages.msgs[i])
+        msgs := msgs.push (snap.cmdState.messages.toList[i])
     i := i + 1
   if msgs.isEmpty then return #[]
   let start := doc.meta.text.lspPosToUtf8Pos params.range.start

Batteries/Data/Array/Basic.lean

@@ -153,6 +153,50 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
 -/
 @[inline] def join (l : Array (Array α)) : Array α := l.foldl (· ++ ·) #[]
 
+/-!
+### Safe Nat Indexed Array functions
+The functions in this section offer variants of Array functions which use `Nat` indices
+instead of `Fin` indices. All these functions have as parameter a proof that the index is
+valid for the array. But this parameter has a default argument `by get_elem_tactic` which
+should prove the index bound.
+-/
+
+/--
+`setN a i h x` sets an element in a vector using a Nat index which is provably valid.
+A proof by `get_elem_tactic` is provided as a default argument for `h`.
+This will perform the update destructively provided that `a` has a reference count of 1 when called.
+-/
+def setN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) (x : α) : Array α :=
+  a.set ⟨i, h⟩ 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.
+-/
+def 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⟩
+
+/--
+`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.
+-/
+def swapAtN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) (x : α) : α × Array α :=
+  swapAt a ⟨i,h⟩ x
+
+/--
+`eraseIdxN a i h` Removes the element at position `i` from a vector of length `n`.
+`h : i < a.size` has a default argument `by get_elem_tactic` which tries to supply a proof
+that the index is valid.
+This function takes worst case O(n) time because it has to backshift all elements at positions
+greater than i.
+-/
+def eraseIdxN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
+  a.feraseIdx ⟨i, h⟩
+
 end Array
 
 

Batteries/Data/Array/Lemmas.lean

@@ -115,3 +115,15 @@ theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L 
 /-! ### erase -/
 
 @[simp] proof_wanted erase_data [BEq α] {l : Array α} {a : α} : (l.erase a).data = l.data.erase a
+
+/-! ### shrink -/
+
+theorem size_shrink_loop (a : Array α) (n) : (shrink.loop n a).size = a.size - n := by
+  induction n generalizing a with simp[shrink.loop]
+  | succ n ih =>
+      simp[ih]
+      omega
+
+theorem size_shrink (a : Array α) (n) : (a.shrink n).size = min a.size n := by
+  simp [shrink, size_shrink_loop]
+  omega

Batteries/Data/BinomialHeap/Basic.lean

@@ -394,10 +394,10 @@ theorem Heap.WF.merge' (h₁ : s₁.WF le n) (h₂ : s₂.WF le n) :
     · let ⟨ih₁, ih₂⟩ := merge' (s₁ := .cons ..)
         ⟨Nat.le_succ_of_le hr₁, this, ht₁.of_rankGT hl₁⟩
         (ht₂.of_le (Nat.le_succ_of_le hr₁))
-      exact ⟨ih₁, fun _ => ih₂ ⟨fun _ => ht₂.rankGT.of_le hr₁, fun h => Nat.lt_succ_of_le hr₁⟩⟩
+      exact ⟨ih₁, fun _ => ih₂ ⟨fun _ => ht₂.rankGT.of_le hr₁, fun _ => Nat.lt_succ_of_le hr₁⟩⟩
     · let ⟨ih₁, ih₂⟩ := merge' (s₂ := .cons ..) (ht₁.of_le (Nat.le_succ_of_le hr₁))
         ⟨Nat.le_succ_of_le hr₁, this, ht₂.of_rankGT hl₂⟩
-      exact ⟨ih₁, fun _ => ih₂ ⟨fun h => Nat.lt_succ_of_le hr₁, fun _ => ht₁.rankGT.of_le hr₁⟩⟩
+      exact ⟨ih₁, fun _ => ih₂ ⟨fun _ => Nat.lt_succ_of_le hr₁, fun _ => ht₁.rankGT.of_le hr₁⟩⟩
     · let ⟨ih₁, ih₂⟩ := merge' ht₁ ht₂
       exact ⟨⟨Nat.le_succ_of_le hr₁, this, ih₁.of_rankGT (ih₂ (iff_of_false hl₁ hl₂))⟩,
         fun _ => Nat.lt_succ_of_le hr₁⟩

Batteries/Data/ByteArray.lean

@@ -14,9 +14,6 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data
 
 /-! ### uget/uset -/
 
-@[simp] theorem ugetElem_eq_getElem (a : ByteArray) {i : USize} (h : i.toNat < a.size) :
-    a[i] = a[i.toNat] := rfl
-
 @[simp] theorem uset_eq_set (a : ByteArray) {i : USize} (h : i.toNat < a.size) (v : UInt8) :
     a.uset i v h = a.set ⟨i.toNat, h⟩ v := rfl
 

Batteries/Data/Fin/Basic.lean

@@ -14,17 +14,3 @@ def enum (n) : Array (Fin n) := Array.ofFn id
 
 /-- `list n` is the list of all elements of `Fin n` in order -/
 def list (n) : List (Fin n) := (enum n).data
-
-/-- Folds over `Fin n` from the left: `foldl 3 f x = f (f (f x 0) 1) 2`. -/
-@[inline] def foldl (n) (f : α → Fin n → α) (init : α) : α := loop init 0 where
-  /-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)`  -/
-  loop (x : α) (i : Nat) : α :=
-    if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
-  termination_by n - i
-
-/-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
-@[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop ⟨n, Nat.le_refl n⟩ init where
-  /-- Inner loop for `Fin.foldr`. `Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))`  -/
-  loop : {i // i ≤ n} → α → α
-  | ⟨0, _⟩, x => x
-  | ⟨i+1, h⟩, x => loop ⟨i, Nat.le_of_lt h⟩ (f ⟨i, h⟩ x)

Batteries/Data/Fin/Lemmas.lean

@@ -38,6 +38,22 @@ protected theorem le_antisymm {x y : Fin n} (h1 : x ≤ y) (h2 : y ≤ x) : x =
 theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by
   apply List.ext_get; simp; intro i; cases i <;> simp
 
+theorem list_succ_last (n) : list (n+1) = (list n).map castSucc ++ [last n] := by
+  rw [list_succ]
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [list_succ, List.map_cons castSucc, ih]
+    simp [Function.comp_def, succ_castSucc]
+
+theorem list_reverse (n) : (list n).reverse = (list n).map rev := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    conv => lhs; rw [list_succ_last]
+    conv => rhs; rw [list_succ]
+    simp [List.reverse_map, ih, Function.comp_def, rev_succ]
+
 /-! ### foldl -/
 
 theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : m < n) :
@@ -56,11 +72,18 @@ theorem foldl_loop (f : α → Fin (n+1) → α) (x) (h : m < n+1) :
     rw [foldl_loop_lt, foldl_loop_eq, foldl_loop_eq]
 termination_by n - m
 
-theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x := by simp [foldl, foldl.loop]
+@[simp] theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x := by simp [foldl, foldl.loop]
 
 theorem foldl_succ (f : α → Fin (n+1) → α) (x) :
     foldl (n+1) f x = foldl n (fun x i => f x i.succ) (f x 0) := foldl_loop ..
 
+theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
+    foldl (n+1) f x = f (foldl n (f · ·.castSucc) x) (last n) := by
+  rw [foldl_succ]
+  induction n generalizing x with
+  | zero => simp [foldl_succ, Fin.last]
+  | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]
+
 theorem foldl_eq_foldl_list (f : α → Fin n → α) (x) : foldl n f x = (list n).foldl f x := by
   induction n generalizing x with
   | zero => rw [foldl_zero, list_zero, List.foldl_nil]
@@ -84,13 +107,33 @@ theorem foldr_loop (f : Fin (n+1) → α → α) (x) (h : m+1 ≤ n+1) :
   | zero => simp [foldr_loop_zero, foldr_loop_succ]
   | succ m ih => rw [foldr_loop_succ, ih, foldr_loop_succ, Fin.succ]
 
-theorem foldr_zero (f : Fin 0 → α → α) (x) :
+@[simp] theorem foldr_zero (f : Fin 0 → α → α) (x) :
     foldr 0 f x = x := foldr_loop_zero ..
 
 theorem foldr_succ (f : Fin (n+1) → α → α) (x) :
     foldr (n+1) f x = f 0 (foldr n (fun i => f i.succ) x) := foldr_loop ..
 
+theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) :
+    foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by
+  induction n generalizing x with
+  | zero => simp [foldr_succ, Fin.last]
+  | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]
+
 theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) : foldr n f x = (list n).foldr f x := by
   induction n with
   | zero => rw [foldr_zero, list_zero, List.foldr_nil]
   | succ n ih => rw [foldr_succ, ih, list_succ, List.foldr_cons, List.foldr_map]
+
+/-! ### foldl/foldr -/
+
+theorem foldl_rev (f : Fin n → α → α) (x) :
+    foldl n (fun x i => f i.rev x) x = foldr n f x := by
+  induction n generalizing x with
+  | zero => simp
+  | succ n ih => rw [foldl_succ, foldr_succ_last, ← ih]; simp [rev_succ]
+
+theorem foldr_rev (f : α → Fin n → α) (x) :
+     foldr n (fun i x => f x i.rev) x = foldl n f x := by
+  induction n generalizing x with
+  | zero => simp
+  | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ]

Batteries/Data/List/Lemmas.lean

@@ -272,7 +272,15 @@ theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) :=
     · simp
     · simp [hl]
 
-/-! ### modify nth -/
+/-! ### modifyNth -/
+
+@[simp] theorem modifyNth_nil (f : α → α) (n) : [].modifyNth f n = [] := by cases n <;> rfl
+
+@[simp] theorem modifyNth_zero_cons (f : α → α) (a : α) (l : List α) :
+    (a :: l).modifyNth f 0 = f a :: l := rfl
+
+@[simp] theorem modifyNth_succ_cons (f : α → α) (a : α) (l : List α) (n) :
+    (a :: l).modifyNth f (n + 1) = a :: l.modifyNth f n := by rfl
 
 theorem modifyNthTail_id : ∀ n (l : List α), l.modifyNthTail id n = l
   | 0, _ => rfl

Batteries/Data/Nat/Basic.lean

@@ -28,6 +28,15 @@ protected def strongRec {motive : Nat → Sort _} (ind : ∀ n, (∀ m, m < n 
 protected def strongRecOn (t : Nat) {motive : Nat → Sort _}
   (ind : ∀ n, (∀ m, m < n → motive m) → motive n) : motive t := Nat.strongRec ind t
 
+/--
+  Strong recursor via a `Nat`-valued measure
+-/
+@[elab_as_elim]
+def strongRecMeasure (f : α → Nat) {motive : α → Sort _}
+    (ind : ∀ x, (∀ y, f y < f x → motive y) → motive x) (x : α) : motive x :=
+  ind x fun y _ => strongRecMeasure f ind y
+termination_by f x
+
 /--
   Simple diagonal recursor for `Nat`
 -/

Batteries/Data/PairingHeap.lean

@@ -246,8 +246,8 @@ theorem Heap.WF.merge (h₁ : s₁.WF le) (h₂ : s₂.WF le) :
 theorem Heap.WF.combine (h : s.NodeWF le a) : (combine le s).WF le :=
   match s with
   | .nil => nil
-  | .node b c .nil => node h.2.1
-  | .node b₁ c₁ (.node b₂ c₂ s) => merge (merge_node h.2.1 h.2.2.2.1) (combine h.2.2.2.2)
+  | .node _b _c .nil => node h.2.1
+  | .node _b₁ _c₁ (.node _b₂ _c₂ _s) => merge (merge_node h.2.1 h.2.2.2.1) (combine h.2.2.2.2)
 
 theorem Heap.WF.deleteMin {s : Heap α} (h : s.WF le)
     (eq : s.deleteMin le = some (a, s')) : s'.WF le := by

Batteries/Data/RBMap/Alter.lean

@@ -100,8 +100,8 @@ protected theorem Balanced.ins {path : Path α}
     | .balanced .nil => exact ih (.balanced (.red hl .nil))
     | .balanced (.red ha hb) => exact ih (.redred rfl hl (.red ha hb))
     | .balanced (.black ha hb) => exact ih (.balanced (.red hl (.black ha hb)))
-  | blackL hr hp ih => exact have ⟨c, h⟩ := ht.balance1 hr; ih (.balanced h)
-  | blackR hl hp ih => exact have ⟨c, h⟩ := ht.balance2 hl; ih (.balanced h)
+  | blackL hr _hp ih => exact have ⟨c, h⟩ := ht.balance1 hr; ih (.balanced h)
+  | blackR hl _hp ih => exact have ⟨c, h⟩ := ht.balance2 hl; ih (.balanced h)
 
 protected theorem Balanced.insertNew {path : Path α} (H : path.Balanced c n black 0) :
     ∃ n, (path.insertNew v).Balanced black n := H.ins (.balanced (.red .nil .nil))

Batteries/Data/String.lean

@@ -1,2 +1,3 @@
 import Batteries.Data.String.Basic
 import Batteries.Data.String.Lemmas
+import Batteries.Data.String.Matcher