Trigger CI for leanprover/lean4#5088

Batteries.lean

@@ -19,6 +19,7 @@ import Batteries.Data.BinomialHeap
 import Batteries.Data.BitVec
 import Batteries.Data.Bool
 import Batteries.Data.ByteArray
+import Batteries.Data.ByteSubarray
 import Batteries.Data.Char
 import Batteries.Data.DList
 import Batteries.Data.Fin
@@ -37,6 +38,7 @@ import Batteries.Data.String
 import Batteries.Data.Sum
 import Batteries.Data.UInt
 import Batteries.Data.UnionFind
+import Batteries.Data.Vector
 import Batteries.Lean.AttributeExtra
 import Batteries.Lean.Delaborator
 import Batteries.Lean.Except
@@ -79,6 +81,7 @@ import Batteries.Tactic.Congr
 import Batteries.Tactic.Exact
 import Batteries.Tactic.Init
 import Batteries.Tactic.Instances
+import Batteries.Tactic.Lemma
 import Batteries.Tactic.Lint
 import Batteries.Tactic.Lint.Basic
 import Batteries.Tactic.Lint.Frontend

Batteries/Data/ByteSubarray.lean

@@ -0,0 +1,105 @@
+
+/-
+Copyright (c) 2021 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, François G. Dorais
+-/
+
+namespace Batteries
+
+/-- A subarray of a `ByteArray`. -/
+structure ByteSubarray where
+  /-- `O(1)`. Get data array of a `ByteSubarray`. -/
+  array : ByteArray
+  /-- `O(1)`. Get start index of a `ByteSubarray`. -/
+  start : Nat
+  /-- `O(1)`. Get stop index of a `ByteSubarray`. -/
+  stop : Nat
+  /-- Start index is before stop index. -/
+  start_le_stop : start ≤ stop
+  /-- Stop index is before end of data array. -/
+  stop_le_array_size : stop ≤ array.size
+
+namespace ByteSubarray
+
+/-- `O(1)`. Get the size of a `ByteSubarray`. -/
+protected def size (self : ByteSubarray) := self.stop - self.start
+
+/-- `O(1)`. Test if a `ByteSubarray` is empty. -/
+protected def isEmpty (self : ByteSubarray) := self.start != self.stop
+
+theorem stop_eq_start_add_size (self : ByteSubarray) : self.stop = self.start + self.size := by
+  rw [ByteSubarray.size, Nat.add_sub_cancel' self.start_le_stop]
+
+/-- `O(n)`. Extract a `ByteSubarray` to a `ByteArray`. -/
+def toByteArray (self : ByteSubarray) : ByteArray :=
+  self.array.extract self.start self.stop
+
+/-- `O(1)`. Get the element at index `i` from the start of a `ByteSubarray`. -/
+@[inline] def get (self : ByteSubarray) (i : Fin self.size) : UInt8 :=
+  have : self.start + i.1 < self.array.size := by
+    apply Nat.lt_of_lt_of_le _ self.stop_le_array_size
+    rw [stop_eq_start_add_size]
+    apply Nat.add_lt_add_left i.is_lt self.start
+  self.array[self.start + i.1]
+
+instance : GetElem ByteSubarray Nat UInt8 fun self i => i < self.size where
+  getElem self i h := self.get ⟨i, h⟩
+
+/-- `O(1)`. Pop the last element of a `ByteSubarray`. -/
+@[inline] def pop (self : ByteSubarray) : ByteSubarray :=
+  if h : self.start = self.stop then self else
+    {self with
+      stop := self.stop - 1
+      start_le_stop := Nat.le_pred_of_lt (Nat.lt_of_le_of_ne self.start_le_stop h)
+      stop_le_array_size := Nat.le_trans (Nat.pred_le _) self.stop_le_array_size
+    }
+
+/-- `O(1)`. Pop the first element of a `ByteSubarray`. -/
+@[inline] def popFront (self : ByteSubarray) : ByteSubarray :=
+  if h : self.start = self.stop then self else
+    {self with
+      start := self.start + 1
+      start_le_stop := Nat.succ_le_of_lt (Nat.lt_of_le_of_ne self.start_le_stop h)
+    }
+
+/-- Folds a monadic function over a `ByteSubarray` from left to right. -/
+@[inline] def foldlM [Monad m] (self : ByteSubarray) (f : β → UInt8 → m β) (init : β) : m β :=
+  self.array.foldlM f init self.start self.stop
+
+/-- Folds a function over a `ByteSubarray` from left to right. -/
+@[inline] def foldl (self : ByteSubarray) (f : β → UInt8 → β) (init : β) : β :=
+  self.foldlM (m:=Id) f init
+
+/-- Implementation of `forIn` for a `ByteSubarray`. -/
+@[specialize]
+protected def forIn [Monad m] (self : ByteSubarray) (init : β) (f : UInt8 → β → m (ForInStep β)) :
+    m β := loop self.size (Nat.le_refl _) init
+where
+  /-- Inner loop of the `forIn` implementation for `ByteSubarray`. -/
+  loop (i : Nat) (h : i ≤ self.size) (b : β) : m β := do
+    match i, h with
+    | 0,   _ => pure b
+    | i+1, h =>
+      match (← f self[self.size - 1 - i] b) with
+      | ForInStep.done b  => pure b
+      | ForInStep.yield b => loop i (Nat.le_of_succ_le h) b
+
+instance : ForIn m ByteSubarray UInt8 where
+  forIn := ByteSubarray.forIn
+
+instance : Stream ByteSubarray UInt8 where
+  next? s := s[0]? >>= fun x => (x, s.popFront)
+
+end Batteries.ByteSubarray
+
+/-- `O(1)`. Coerce a byte array into a byte slice. -/
+def ByteArray.toByteSubarray (array : ByteArray) : Batteries.ByteSubarray where
+  array := array
+  start := 0
+  stop := array.size
+  start_le_stop := Nat.zero_le _
+  stop_le_array_size := Nat.le_refl _
+
+instance : Coe ByteArray Batteries.ByteSubarray where
+  coe := ByteArray.toByteSubarray

Batteries/Data/List/Basic.lean

@@ -117,10 +117,14 @@ splitAt 2 [a, b, c] = ([a, b], [c])
 ```
 -/
 def splitAt (n : Nat) (l : List α) : List α × List α := go l n [] where
-  /-- Auxiliary for `splitAt`: `splitAt.go l n xs acc = (acc.reverse ++ take n xs, drop n xs)`
-  if `n < length xs`, else `(l, [])`. -/
+  /--
+  Auxiliary for `splitAt`:
+  `splitAt.go l xs n acc = (acc.reverse ++ take n xs, drop n xs)` if `n < xs.length`,
+  and `(l, [])` otherwise.
+  -/
   go : List α → Nat → List α → List α × List α
-  | [], _, _ => (l, [])
+  | [], _, _ => (l, []) -- This branch ensures the pointer equality of the result with the input
+                        -- without any runtime branching cost.
   | x :: xs, n+1, acc => go xs n (x :: acc)
   | xs, _, acc => (acc.reverse, xs)
 
@@ -137,7 +141,7 @@ def splitAtD (n : Nat) (l : List α) (dflt : α) : List α × List α := go n l
   if `splitAtD n l dflt = (left, right)`. -/
   go : Nat → List α → List α → List α × List α
   | n+1, x :: xs, acc => go n xs (x :: acc)
-  | 0, xs, acc => (acc, xs)
+  | 0, xs, acc => (acc.reverse, xs)
   | n, [], acc => (acc.reverseAux (replicate n dflt), [])
 
 /--
@@ -1141,30 +1145,6 @@ protected def traverse [Applicative F] (f : α → F β) : List α → F (List 
   | [] => pure []
   | x :: xs => List.cons <$> f x <*> List.traverse f xs
 
-/--
-`Perm l₁ l₂` or `l₁ ~ l₂` asserts that `l₁` and `l₂` are permutations
-of each other. This is defined by induction using pairwise swaps.
--/
-inductive Perm : List α → List α → Prop
-  /-- `[] ~ []` -/
-  | nil : Perm [] []
-  /-- `l₁ ~ l₂ → x::l₁ ~ x::l₂` -/
-  | cons (x : α) {l₁ l₂ : List α} : Perm l₁ l₂ → Perm (x :: l₁) (x :: l₂)
-  /-- `x::y::l ~ y::x::l` -/
-  | swap (x y : α) (l : List α) : Perm (y :: x :: l) (x :: y :: l)
-  /-- `Perm` is transitive. -/
-  | trans {l₁ l₂ l₃ : List α} : Perm l₁ l₂ → Perm l₂ l₃ → Perm l₁ l₃
-
-@[inherit_doc] scoped infixl:50 " ~ " => Perm
-
-/--
-`O(|l₁| * |l₂|)`. Computes whether `l₁` is a permutation of `l₂`. See `isPerm_iff` for a
-characterization in terms of `List.Perm`.
--/
-def isPerm [BEq α] : List α → List α → Bool
-  | [], l₂ => l₂.isEmpty
-  | a :: l₁, l₂ => l₂.contains a && l₁.isPerm (l₂.erase a)
-
 /--
 `Subperm l₁ l₂`, denoted `l₁ <+~ l₂`, means that `l₁` is a sublist of
 a permutation of `l₂`. This is an analogue of `l₁ ⊆ l₂` which respects
@@ -1180,6 +1160,18 @@ See `isSubperm_iff` for a characterization in terms of `List.Subperm`.
 -/
 def isSubperm [BEq α] (l₁ l₂ : List α) : Bool := ∀ x ∈ l₁, count x l₁ ≤ count x l₂
 
+/--
+`O(|l|)`. Inserts `a` in `l` right before the first element such that `p` is true, or at the end of
+the list if `p` always false on `l`.
+-/
+def insertP (p : α → Bool) (a : α) (l : List α) : List α :=
+  loop l []
+where
+  /-- Inner loop for `insertP`. Tail recursive. -/
+  loop : List α → List α → List α
+  | [], r => reverseAux (a :: r) [] -- Note: `reverseAux` is tail recursive.
+  | b :: l, r => bif p b then reverseAux (a :: r) (b :: l) else loop l (b :: r)
+
 /--
 `O(|l| + |r|)`. Merge two lists using `s` as a switch.
 -/

Batteries/Data/List/Lemmas.lean

@@ -189,6 +189,25 @@ theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) :
 
 @[deprecated (since := "2024-05-06")] alias length_removeNth := length_eraseIdx
 
+/-! ### splitAt -/
+
+theorem splitAt_go (n : Nat) (l acc : List α) :
+    splitAt.go l xs n acc =
+      if n < xs.length then (acc.reverse ++ xs.take n, xs.drop n) else (l, []) := by
+  induction xs generalizing n acc with
+  | nil => simp [splitAt.go]
+  | cons x xs ih =>
+    cases n with
+    | zero => simp [splitAt.go]
+    | succ n =>
+      rw [splitAt.go, take_succ_cons, drop_succ_cons, ih n (x :: acc),
+        reverse_cons, append_assoc, singleton_append, length_cons]
+      simp only [Nat.succ_lt_succ_iff]
+
+theorem splitAt_eq (n : Nat) (l : List α) : splitAt n l = (l.take n, l.drop n) := by
+  rw [splitAt, splitAt_go, reverse_nil, nil_append]
+  split <;> simp_all [take_of_length_le, drop_of_length_le]
+
 /-! ### eraseP -/
 
 @[simp] theorem extractP_eq_find?_eraseP
@@ -562,10 +581,37 @@ theorem indexOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈
         specialize ih m
         simpa
 
+/-! ### insertP -/
+
+theorem insertP_loop (a : α) (l r : List α) :
+    insertP.loop p a l r = reverseAux r (insertP p a l) := by
+  induction l generalizing r with simp [insertP, insertP.loop, cond]
+  | cons b l ih => rw [ih (b :: r), ih [b]]; split <;> rfl
+
+@[simp] theorem insertP_nil (p : α → Bool) (a) : insertP p a [] = [a] := rfl
+
+@[simp] theorem insertP_cons_pos (p : α → Bool) (a b l) (h : p b) :
+    insertP p a (b :: l) = a :: b :: l := by
+  simp only [insertP, insertP.loop, cond, h]; rfl
+
+@[simp] theorem insertP_cons_neg (p : α → Bool) (a b l) (h : ¬ p b) :
+    insertP p a (b :: l) = b :: insertP p a l := by
+  simp only [insertP, insertP.loop, cond, h]; exact insertP_loop ..
+
+@[simp] theorem length_insertP (p : α → Bool) (a l) : (insertP p a l).length = l.length + 1 := by
+  induction l with simp [insertP, insertP.loop, cond]
+  | cons _ _ ih => split <;> simp [insertP_loop, ih]
+
+@[simp] theorem mem_insertP (p : α → Bool) (a l) : a ∈ insertP p a l := by
+  induction l with simp [insertP, insertP.loop, cond]
+  | cons _ _ ih => split <;> simp [insertP_loop, ih]
+
 theorem merge_loop_nil_left (s : α → α → Bool) (r t) :
     merge.loop s [] r t = reverseAux t r := by
   rw [merge.loop]
 
+/-! ### merge -/
+
 theorem merge_loop_nil_right (s : α → α → Bool) (l t) :
     merge.loop s l [] t = reverseAux t l := by
   cases l <;> rw [merge.loop]; intro; contradiction
@@ -637,3 +683,13 @@ theorem mem_merge_left (s : α → α → Bool) (h : x ∈ l) : x ∈ merge s l
 
 theorem mem_merge_right (s : α → α → Bool) (h : x ∈ r) : x ∈ merge s l r :=
   mem_merge.2 <| .inr h
+
+/-! ### foldlM and foldrM -/
+
+theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :
+    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
+  induction l generalizing g init <;> simp [*]
+
+theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : List β₁)
+    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
+  induction l generalizing g init <;> simp [*]