chore: merge #1111

.github/workflows/build.yml

@@ -10,7 +10,7 @@ on:
 name: ci
 
 concurrency:
-  group: build-${{ github.ref }}
+  group: build-${{ github.sha }}
   cancel-in-progress: true
 
 jobs:

Batteries.lean

@@ -23,6 +23,7 @@ import Batteries.Data.DList
 import Batteries.Data.Fin
 import Batteries.Data.FloatArray
 import Batteries.Data.HashMap
+import Batteries.Data.Int
 import Batteries.Data.LazyList
 import Batteries.Data.List
 import Batteries.Data.MLList

Batteries/Data/Array/Lemmas.lean

@@ -61,8 +61,10 @@ where
 
 /-! ### erase -/
 
-@[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} :
-    (l.erase a).toList = l.toList.erase a
+@[simp] theorem toList_erase [BEq α] (l : Array α) (a : α) :
+    (l.erase a).toList = l.toList.erase a := by
+  simp only [erase, ← List.eraseIdx_indexOf_eq_erase, List.indexOf_eq_indexOf?, length_toList]
+  cases h : l.indexOf? a <;> simp [Array.indexOf?_toList, List.eraseIdx_of_length_le, *]
 
 @[simp] theorem size_eraseIdxIfInBounds (a : Array α) (i : Nat) :
     (a.eraseIdxIfInBounds i).size = if i < a.size then a.size-1 else a.size := by

Batteries/Data/ByteArray.lean

@@ -118,10 +118,20 @@ theorem get_extract_aux {a : ByteArray} {start stop} (h : i < (a.extract start s
 /-! ### ofFn -/
 
 /--- `ofFn f` with `f : Fin n → UInt8` returns the byte array whose `i`th element is `f i`. --/
-def ofFn (f : Fin n → UInt8) : ByteArray where
-  data := .ofFn f
+@[inline] def ofFn (f : Fin n → UInt8) : ByteArray :=
+  Fin.foldl n (fun acc i => acc.push (f i)) (mkEmpty n)
+
+@[simp] theorem ofFn_zero (f : Fin 0 → UInt8) : ofFn f = empty := rfl
+
+theorem ofFn_succ (f : Fin (n+1) → UInt8) :
+    ofFn f = (ofFn fun i => f i.castSucc).push (f (Fin.last n)) := by
+  simp [ofFn, Fin.foldl_succ_last, mkEmpty]
+
+@[simp] theorem data_ofFn (f : Fin n → UInt8) : (ofFn f).data = .ofFn f := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simp [ofFn_succ, Array.ofFn_succ, ih, Fin.last]
 
-@[simp] theorem data_ofFn (f : Fin n → UInt8) : (ofFn f).data = .ofFn f := rfl
 @[deprecated (since := "2024-08-13")] alias ofFn_data := data_ofFn
 
 @[simp] theorem size_ofFn (f : Fin n → UInt8) : (ofFn f).size = n := by
@@ -134,19 +144,6 @@ def ofFn (f : Fin n → UInt8) : ByteArray where
 @[simp] theorem getElem_ofFn (f : Fin n → UInt8) (i) (h : i < (ofFn f).size) :
     (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ := get_ofFn f ⟨i, h⟩
 
-private def ofFnAux (f : Fin n → UInt8) : ByteArray := go 0 (mkEmpty n) where
-  go (i : Nat) (acc : ByteArray) : ByteArray :=
-    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by n - i
-
-@[csimp] private theorem ofFn_eq_ofFnAux : @ofFn = @ofFnAux := by
-  funext n f; ext1; simp [ofFnAux, Array.ofFn, data_ofFnAux, mkEmpty]
-where
-  data_ofFnAux {n} (f : Fin n → UInt8) (i) {acc} :
-      (ofFnAux.go f i acc).data = Array.ofFn.go f i acc.data := by
-    rw [ofFnAux.go, Array.ofFn.go]; split; rw [data_ofFnAux f (i+1), data_push]; rfl
-  termination_by n - i
-
 /-! ### map/mapM -/
 
 /--

Batteries/Data/Int.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2025 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+import Batteries.Data.Nat.Lemmas
+
+namespace Int
+
+/--
+`testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`, using the two's
+complement convention for negative `m`.
+-/
+def testBit : Int → Nat → Bool
+  | ofNat m, n => Nat.testBit m n
+  | negSucc m, n => !(Nat.testBit m n)
+
+/--
+Construct an integer from a sequence of bits using little endian convention.
+
+The sign is determined using the two's complement convention: the result is negative if and only if
+`n > 0` and `f (n-1) = true`.
+-/
+def ofBits (f : Fin n → Bool) :=
+  if 2 * Nat.ofBits f < 2 ^ n then
+    ofNat (Nat.ofBits f)
+  else
+    subNatNat (Nat.ofBits f) (2 ^ n)
+
+@[simp] theorem ofBits_zero (f : Fin 0 → Bool) : ofBits f = 0 := by
+  simp [ofBits]
+
+@[simp] theorem testBit_ofBits_lt {f : Fin n → Bool} (h : i < n) :
+    (ofBits f).testBit i = f ⟨i, h⟩ := by
+  simp only [ofBits]
+  split
+  · simp only [testBit, Nat.testBit_ofBits_lt, h]
+  · have hlt := Nat.ofBits_lt_two_pow f
+    simp [subNatNat_of_lt hlt, testBit, Nat.sub_sub, Nat.testBit_two_pow_sub_succ hlt, h]
+
+@[simp] theorem testBit_ofBits_ge {f : Fin n → Bool} (h : i ≥ n) :
+    (ofBits f).testBit i = decide (ofBits f < 0) := by
+  simp only [ofBits]
+  split
+  · have hge : ¬ ofNat (Nat.ofBits f) < 0 := by rw [Int.not_lt]; exact ofNat_nonneg ..
+    simp only [testBit, Nat.testBit_ofBits_ge _ _ h, hge, decide_false]
+  · have hlt := Nat.ofBits_lt_two_pow f
+    have h : 2 ^ n - Nat.ofBits f - 1 < 2 ^ i :=
+      Nat.lt_of_lt_of_le (by omega) (Nat.pow_le_pow_right Nat.zero_lt_two h)
+    simp [testBit, subNatNat_of_lt hlt, Nat.testBit_lt_two_pow h, negSucc_lt_zero]
+
+theorem testBit_ofBits (f : Fin n → Bool) :
+    (ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else decide (ofBits f < 0) := by
+  split <;> simp_all

Batteries/Data/List/Basic.lean

@@ -1064,3 +1064,10 @@ where
   | a :: as, acc => match (a :: as).dropPrefix? i with
     | none => go as (a :: acc)
     | some s => (acc.reverse, s)
+
+/--
+`findMap? f l` returns the `f x` for the first element `x` such that `f x` is `some _`, or
+`none` if no such element is found.
+-/
+def findMap? (f : α → Option β) (l : List α) : Option β :=
+  l.foldl (fun r x => r <|> f x) none

Batteries/Data/List/Lemmas.lean

@@ -7,6 +7,7 @@ import Batteries.Control.ForInStep.Lemmas
 import Batteries.Data.List.Basic
 import Batteries.Tactic.Init
 import Batteries.Tactic.Alias
+import Batteries.Util.ProofWanted
 
 namespace List
 
@@ -633,6 +634,73 @@ theorem dropInfix?_eq_some_iff [BEq α] {l i p s : List α} :
 @[simp] theorem dropInfix?_nil [BEq α] {s : List α} : dropInfix? s [] = some ([], s) := by
   simp [dropInfix?_eq_some_iff]
 
+/-! ### findMap? -/
+
+private theorem findMap?_aux (f : α → Option β) (xs : List α) :
+    xs.foldl (fun r x => r <|> f x) t = (t <|> xs.findMap? f) := by
+  simp only [findMap?]
+  induction xs with
+  | nil => simp
+  | cons x xs ih => cases t <;> simp [ih]
+
+@[simp] theorem findMap?_nil (f : α → Option β) : [].findMap? f = none := rfl
+
+theorem findMap?_cons (f : α → Option β) : (x :: xs).findMap? f = (f x <|> xs.findMap? f) := by
+  rw [findMap?, foldl_cons, findMap?_aux, none_orElse]
+
+theorem exists_eq_some_of_findMap?_eq_some {f : α → Option β} {xs : List α}
+    (h : xs.findMap? f = some z) : ∃ x ∈ xs, f x = some z := by
+  induction xs with
+  | nil => contradiction
+  | cons x xs ih =>
+    rw [findMap?_cons] at h
+    match hx : f x with
+    | some y =>
+      rw [hx, some_orElse] at h
+      cases h; refine ⟨x, ?_, hx⟩; simp
+    | none =>
+      rw [hx, none_orElse] at h
+      match ih h with
+      | ⟨x, hmem, hx⟩ => refine ⟨x, ?_, hx⟩; simp [hmem]
+
+theorem eq_none_of_findMap?_eq_none_of_mem {f : α → Option β} {xs : List α}
+    (h : xs.findMap? f = none) (hx : x ∈ xs) : f x = none := by
+  induction xs with
+  | nil => contradiction
+  | cons x xs ih =>
+    rw [findMap?_cons] at h
+    match hx : f x with
+    | some y =>
+      rw [hx, some_orElse] at h
+      contradiction
+    | none =>
+      next hmem =>
+      rw [hx, none_orElse] at h
+      cases hmem
+      · exact hx
+      · apply ih h
+        assumption
+
+proof_wanted findMap?_isSome {f : α → Option β} {xs : List α} :
+    (xs.findMap? f).isSome ↔ ∃ x ∈ xs, (f x).isSome
+
+proof_wanted findMap?_eq_none {f : α → Option β} {xs : List α} :
+    xs.findMap? f = none ↔ ∀ x ∈ xs, f x = none
+
+proof_wanted findMap?_singleton {f : α → Option β} {x : α} : [x].findMap? f = f x
+
+proof_wanted findMap?_append {f : α → Option β} {xs ys : List α} :
+    (xs ++ ys).findMap? f = (xs.findMap? f <|> ys.findMap? f)
+
+proof_wanted findMap?_flatMap {g : α → List β} {f : β → Option γ} {xs : List α} :
+    (xs.flatMap g).findMap? f = xs.findMap? fun x => (g x).findMap? f
+
+proof_wanted findMap?_flatten {f : α → Option β} {xss : List (List α)} :
+    xss.flatten.findMap? f = xss.findMap? fun xs => xs.findMap? f
+
+proof_wanted findMap?_map {g : α → β} {f : β → Option γ} {xs : List α} :
+    (xs.map g).findMap? f = xs.findMap? fun x => f (g x)
+
 /-! ### deprecations -/
 
 @[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff

Batteries/Data/Vector/Basic.lean

@@ -39,8 +39,6 @@ namespace Vector
 @[deprecated "Use `#v[]`." (since := "2024-11-27")]
 def empty (α : Type u) : Vector α 0 := #v[]
 
-proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α n)
-
 /--
 Returns `true` when all elements of the vector are pairwise distinct using `==` for comparison.
 -/

Batteries/Data/Vector/Lemmas.lean

@@ -203,6 +203,13 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem toArray_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) :
     (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
 
+theorem isEqv_eq_toArray_isEqv_toArray (a b : Vector α n) :
+    a.isEqv b r = a.toArray.isEqv b.toArray r :=
+  match a, b with | ⟨_,_⟩, ⟨_,_⟩ => mk_isEqv_mk ..
+
+theorem beq_eq_toArray_beq [BEq α] (a b : Vector α n) : (a == b) = (a.toArray == b.toArray) := by
+  simp [(· == ·), isEqv_eq_toArray_isEqv_toArray]
+
 /-! ### toList lemmas -/
 
 theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by simp
@@ -291,3 +298,9 @@ instance instDecidableExistsVectorZero (P : Vector α 0 → Prop) [Decidable (P
 instance instDecidableExistsVectorSucc (P : Vector α (n+1) → Prop)
     [Decidable (∀ (x : α) (v : Vector α n), ¬ P (v.push x))] : Decidable (∃ v, P v) :=
   decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+
+instance (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α n) where
+  rfl {a} := by simp_all [beq_eq_toArray_beq]
+  eq_of_beq {a b h} := by
+    apply toArray_injective
+    simp_all [beq_eq_toArray_beq]