Trigger CI for leanprover/lean4#4154

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

@@ -110,20 +110,6 @@ Unlike `bagInter` this does not preserve multiplicity: `[1, 1].inter [1]` is `[1
 
 instance [BEq α] : Inter (List α) := ⟨List.inter⟩
 
-/--
-Split a list at an index.
-```
-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.toList ++ take n xs, drop n xs)`
-  if `n < length xs`, else `(l, [])`. -/
-  go : List α → Nat → Array α → List α × List α
-  | [], _, _ => (l, [])
-  | x :: xs, n+1, acc => go xs n (acc.push x)
-  | xs, _, acc => (acc.toList, xs)
-
 /--
 Split a list at an index. Ensures the left list always has the specified length
 by right padding with the provided default element.
@@ -132,13 +118,13 @@ splitAtD 2 [a, b, c] x = ([a, b], [c])
 splitAtD 4 [a, b, c] x = ([a, b, c, x], [])
 ```
 -/
-def splitAtD (n : Nat) (l : List α) (dflt : α) : List α × List α := go n l #[] where
-  /-- Auxiliary for `splitAtD`: `splitAtD.go dflt n l acc = (acc.toList ++ left, right)`
+def splitAtD (n : Nat) (l : List α) (dflt : α) : List α × List α := go n l [] where
+  /-- Auxiliary for `splitAtD`: `splitAtD.go dflt n l acc = (acc.reverse ++ left, right)`
   if `splitAtD n l dflt = (left, right)`. -/
-  go : Nat → List α → Array α → List α × List α
-  | n+1, x :: xs, acc => go n xs (acc.push x)
-  | 0, xs, acc => (acc.toList, xs)
-  | n, [], acc => (acc.toListAppend (replicate n dflt), [])
+  go : Nat → List α → List α → List α × List α
+  | n+1, x :: xs, acc => go n xs (x :: acc)
+  | 0, xs, acc => (acc.reverse, xs)
+  | n, [], acc => (acc.reverseAux (replicate n dflt), [])
 
 /--
 Split a list at every element satisfying a predicate. The separators are not in the result.
@@ -544,7 +530,7 @@ theorem sections_eq_nil_of_isEmpty : ∀ {L}, L.any isEmpty → @sections α L =
   | l :: L, h => by
     simp only [any, foldr, Bool.or_eq_true] at h
     match l, h with
-    | [], .inl rfl => simp; induction sections L <;> simp [*]
+    | [], .inl rfl => simp
     | l, .inr h => simp [sections, sections_eq_nil_of_isEmpty h]
 
 @[csimp] theorem sections_eq_sectionsTR : @sections = @sectionsTR := by
@@ -1141,30 +1127,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
@@ -1181,13 +1143,13 @@ 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| + |r|)`. Merge two lists using `s` as a switch.
+`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 merge (s : α → α → Bool) (l r : List α) : List α :=
-  loop l r []
+def insertP (p : α → Bool) (a : α) (l : List α) : List α :=
+  loop l []
 where
-  /-- Inner loop for `List.merge`. Tail recursive. -/
-  loop : List α → List α → List α → List α
-  | [], r, t => reverseAux t r
-  | l, [], t => reverseAux t l
-  | a::l, b::r, t => bif s a b then loop l (b::r) (a::t) else loop (a::l) r (b::t)
+  /-- 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)

Batteries/Data/List/Lemmas.lean

@@ -562,45 +562,36 @@ theorem indexOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈
         specialize ih m
         simpa
 
-theorem merge_loop_nil_left (s : α → α → Bool) (r t) :
-    merge.loop s [] r t = reverseAux t r := by
-  rw [merge.loop]
-
-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
-
-theorem merge_loop (s : α → α → Bool) (l r t) :
-    merge.loop s l r t = reverseAux t (merge s l r) := by
-  rw [merge]; generalize hn : l.length + r.length = n
-  induction n using Nat.recAux generalizing l r t with
-  | zero =>
-    rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_add_eq_zero_left hn)]
-    rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_add_eq_zero_right hn)]
-    simp only [merge.loop, reverseAux]
-  | succ n ih =>
-    match l, r with
-    | [], r => simp only [merge_loop_nil_left]; rfl
-    | l, [] => simp only [merge_loop_nil_right]; rfl
-    | a::l, b::r =>
-      simp only [merge.loop, cond]
-      split
-      · have hn : l.length + (b :: r).length = n := by
-          apply Nat.add_right_cancel (m:=1)
-          rw [←hn]; simp only [length_cons, Nat.add_succ, Nat.succ_add]
-        rw [ih _ _ (a::t) hn, ih _ _ [] hn, ih _ _ [a] hn]; rfl
-      · have hn : (a::l).length + r.length = n := by
-          apply Nat.add_right_cancel (m:=1)
-          rw [←hn]; simp only [length_cons, Nat.add_succ, Nat.succ_add]
-        rw [ih _ _ (b::t) hn, ih _ _ [] hn, ih _ _ [b] hn]; rfl
-
-@[simp] theorem merge_nil (s : α → α → Bool) (l) : merge s l [] = l := merge_loop_nil_right ..
-
-@[simp] theorem nil_merge (s : α → α → Bool) (r) : merge s [] r = r := merge_loop_nil_left ..
+/-! ### 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 <;> simp
+
+@[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]
+
+/-! ### merge -/
 
 theorem cons_merge_cons (s : α → α → Bool) (a b l r) :
-  merge s (a::l) (b::r) = if s a b then a :: merge s l (b::r) else b :: merge s (a::l) r := by
-  simp only [merge, merge.loop, cond]; split <;> (next hs => rw [hs, merge_loop]; rfl)
+    merge s (a::l) (b::r) = if s a b then a :: merge s l (b::r) else b :: merge s (a::l) r := by
+  simp only [merge]
 
 @[simp] theorem cons_merge_cons_pos (s : α → α → Bool) (l r) (h : s a b) :
     merge s (a::l) (b::r) = a :: merge s l (b::r) := by
@@ -621,19 +612,18 @@ theorem cons_merge_cons (s : α → α → Bool) (a b l r) :
     · simp_arith [length_merge s l (b::r)]
     · simp_arith [length_merge s (a::l) r]
 
-@[simp]
-theorem mem_merge {s : α → α → Bool} : x ∈ merge s l r ↔ x ∈ l ∨ x ∈ r := by
-  match l, r with
-  | l, [] => simp
-  | [], l => simp
-  | a::l, b::r =>
-    rw [cons_merge_cons]
-    split
-    · simp [mem_merge (l := l) (r := b::r), or_assoc]
-    · simp [mem_merge (l := a::l) (r := r), or_assoc, or_left_comm]
-
 theorem mem_merge_left (s : α → α → Bool) (h : x ∈ l) : x ∈ merge s l r :=
   mem_merge.2 <| .inl h
 
 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 [*]