chore: reset to nightly-testing

Batteries/Data/Array/Lemmas.lean

@@ -14,57 +14,113 @@ namespace Array
 theorem forIn_eq_forIn_toList [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
     forIn as b f = forIn as.toList b f := by
-  cases as
-  simp
+  let rec loop : ∀ {i h b j}, j + i = as.size →
+      Array.forIn.loop as f i h b = forIn (as.toList.drop j) b f
+    | 0, _, _, _, rfl => by rw [List.drop_length]; rfl
+    | i+1, _, _, j, ij => by
+      simp only [forIn.loop, Nat.add]
+      have j_eq : j = size as - 1 - i := by simp [← ij, ← Nat.add_assoc]
+      have : as.size - 1 - i < as.size := j_eq ▸ ij ▸ Nat.lt_succ_of_le (Nat.le_add_right ..)
+      have : as[size as - 1 - i] :: as.toList.drop (j + 1) = as.toList.drop j := by
+        rw [j_eq]; exact List.getElem_cons_drop _ _ this
+      simp only [← this, List.forIn_cons]; congr; funext x; congr; funext b
+      rw [loop (i := i)]; rw [← ij, Nat.succ_add]; rfl
+  conv => lhs; simp only [forIn, Array.forIn]
+  rw [loop (Nat.zero_add _)]; rfl
 
 @[deprecated (since := "2024-09-09")] alias forIn_eq_forIn_data := forIn_eq_forIn_toList
 @[deprecated (since := "2024-08-13")] alias forIn_eq_data_forIn := forIn_eq_forIn_data
 
 /-! ### zipWith / zip -/
 
+theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
+    (as.zipWith bs f).toList = as.toList.zipWith f bs.toList := by
+  let rec loop : ∀ (i : Nat) cs, i ≤ as.size → i ≤ bs.size →
+      (zipWithAux f as bs i cs).toList =
+        cs.toList ++ (as.toList.drop i).zipWith f (bs.toList.drop i) := by
+    intro i cs hia hib
+    unfold zipWithAux
+    by_cases h : i = as.size ∨ i = bs.size
+    case pos =>
+      have : ¬(i < as.size) ∨ ¬(i < bs.size) := by
+        cases h <;> simp_all only [Nat.not_lt, Nat.le_refl, true_or, or_true]
+      -- Cleaned up aesop output below
+      simp_all only [Nat.not_lt]
+      cases h <;> [(cases this); (cases this)]
+      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
+                      List.zipWith_nil_left, List.append_nil]
+      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
+                      List.zipWith_nil_left, List.append_nil]
+      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
+                      List.zipWith_nil_right, List.append_nil]
+        split <;> simp_all only [Nat.not_lt]
+      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
+                      List.zipWith_nil_right, List.append_nil]
+        split <;> simp_all only [Nat.not_lt]
+    case neg =>
+      rw [not_or] at h
+      have has : i < as.size := Nat.lt_of_le_of_ne hia h.1
+      have hbs : i < bs.size := Nat.lt_of_le_of_ne hib h.2
+      simp only [has, hbs, dite_true]
+      rw [loop (i+1) _ has hbs, Array.push_toList]
+      have h₁ : [f as[i] bs[i]] = List.zipWith f [as[i]] [bs[i]] := rfl
+      let i_as : Fin as.toList.length := ⟨i, has⟩
+      let i_bs : Fin bs.toList.length := ⟨i, hbs⟩
+      rw [h₁, List.append_assoc]
+      congr
+      rw [← List.zipWith_append (h := by simp), getElem_eq_toList_getElem,
+        getElem_eq_toList_getElem]
+      show List.zipWith f (as.toList[i_as] :: List.drop (i_as + 1) as.toList)
+        ((List.get bs.toList i_bs) :: List.drop (i_bs + 1) bs.toList) =
+        List.zipWith f (List.drop i as.toList) (List.drop i bs.toList)
+      simp only [toList_length, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem]
+  simp [zipWith, loop 0 #[] (by simp) (by simp)]
 @[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 β) :
+theorem toList_zip (as : Array α) (bs : Array β) :
+    (as.zip bs).toList = as.toList.zip bs.toList :=
+  toList_zipWith Prod.mk as bs
+@[deprecated (since := "2024-09-09")] alias data_zip := toList_zip
+@[deprecated (since := "2024-08-13")] alias zip_eq_zip_data := data_zip
+
+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 α) :
     (l.filter p).size ≤ l.size := by
-  simp only [← length_toList, toList_filter]
+  simp only [← toList_length, filter_toList]
   apply List.length_filter_le
 
 /-! ### flatten -/
 
-@[deprecated (since := "2024-09-09")] alias data_join := toList_flatten
-@[deprecated (since := "2024-08-13")] alias join_data := toList_flatten
-@[deprecated (since := "2024-10-15")] alias mem_join := mem_flatten
-
-/-! ### indexOf? -/
-
-theorem indexOf?_toList [BEq α] {a : α} {l : Array α} :
-    l.toList.indexOf? a = (l.indexOf? a).map Fin.val := by
-  simpa using aux l 0
-where
-  aux (l : Array α) (i : Nat) :
-       ((l.toList.drop i).indexOf? a).map (·+i) = (indexOfAux l a i).map Fin.val := by
-    rw [indexOfAux]
-    if h : i < l.size then
-      rw [List.drop_eq_getElem_cons h, ←getElem_eq_getElem_toList, List.indexOf?_cons]
-      if h' : l[i] == a then
-        simp [h, h']
-      else
-        simp [h, h', ←aux l (i+1), Function.comp_def, ←Nat.add_assoc, Nat.add_right_comm]
-    else
-      have h' : l.size ≤ i := Nat.le_of_not_lt h
-      simp [h, List.drop_of_length_le h', List.indexOf?]
-  termination_by l.size - i
+@[simp] theorem toList_join {l : Array (Array α)} : l.join.toList = (l.toList.map toList).join := by
+  dsimp [join]
+  simp only [foldl_eq_foldl_toList]
+  generalize l.toList = l
+  have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
+  exact this #[]
+  induction l with
+  | nil => simp
+  | cons h => induction h.toList <;> simp [*]
+@[deprecated (since := "2024-09-09")] alias data_join := toList_join
+@[deprecated (since := "2024-08-13")] alias join_data := data_join
+
+theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l := by
+  simp only [mem_def, toList_join, List.mem_join, List.mem_map]
+  intro l
+  constructor
+  · rintro ⟨_, ⟨s, m, rfl⟩, h⟩
+    exact ⟨s, m, h⟩
+  · rintro ⟨s, h₁, h₂⟩
+    refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
 
 /-! ### erase -/
 

Batteries/Data/Array/Pairwise.lean

@@ -20,12 +20,12 @@ that `as` is strictly sorted and `as.Pairwise (· ≤ ·)` asserts that `as` is
 def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwise R
 
 theorem pairwise_iff_get {as : Array α} : as.Pairwise R ↔
-    ∀ (i j : Fin as.size), i < j → R (as.get i i.2) (as.get j j.2) := by
-  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_getElem_toList]
+    ∀ (i j : Fin as.size), i < j → R (as.get i) (as.get j) := by
+  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_toList_get]; rfl
 
 theorem pairwise_iff_getElem {as : Array α} : as.Pairwise R ↔
     ∀ (i j : Nat) (_ : i < as.size) (_ : j < as.size), i < j → R as[i] as[j] := by
-  unfold Pairwise; simp [List.pairwise_iff_getElem, length_toList]
+  unfold Pairwise; simp [List.pairwise_iff_getElem, toList_length]; rfl
 
 instance (R : α → α → Prop) [DecidableRel R] (as) : Decidable (Pairwise R as) :=
   have : (∀ (j : Fin as.size) (i : Fin j.val), R as[i.val] (as[j.val])) ↔ Pairwise R as := by
@@ -46,7 +46,7 @@ theorem pairwise_pair : #[a, b].Pairwise R ↔ R a b := by
 
 theorem pairwise_append {as bs : Array α} :
     (as ++ bs).Pairwise R ↔ as.Pairwise R ∧ bs.Pairwise R ∧ (∀ x ∈ as, ∀ y ∈ bs, R x y) := by
-  unfold Pairwise; simp [← mem_toList, toList_append, ← List.pairwise_append]
+  unfold Pairwise; simp [← mem_toList, append_toList, ← List.pairwise_append]
 
 theorem pairwise_push {as : Array α} :
     (as.push a).Pairwise R ↔ as.Pairwise R ∧ (∀ x ∈ as, R x a) := by

Batteries/Data/Fin/Lemmas.lean

@@ -10,6 +10,10 @@ namespace Fin
 
 attribute [norm_cast] val_last
 
+/-! ### last -/
+
+@[simp] theorem last_zero : last 0 = 0 := rfl
+
 /-! ### clamp -/
 
 @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl
@@ -27,7 +31,7 @@ attribute [norm_cast] val_last
 
 @[simp] theorem getElem_list (i : Nat) (h : i < (list n).length) :
     (list n)[i] = cast (length_list n) ⟨i, h⟩ := by
-  simp only [list]; rw [← Array.getElem_eq_getElem_toList, getElem_enum, cast_mk]
+  simp only [list]; rw [← Array.getElem_eq_toList_getElem, getElem_enum, cast_mk]
 
 @[deprecated getElem_list (since := "2024-06-12")]
 theorem get_list (i : Fin (list n).length) : (list n).get i = i.cast (length_list n) := by

Batteries/Data/HashMap/Basic.lean

@@ -37,7 +37,7 @@ def update (data : Buckets α β) (i : USize)
 The number of elements in the bucket array.
 Note: this is marked `noncomputable` because it is only intended for specification.
 -/
-noncomputable def size (data : Buckets α β) : Nat := (data.1.toList.map (·.toList.length)).sum
+noncomputable def size (data : Buckets α β) : Nat := .sum (data.1.toList.map (·.toList.length))
 
 @[simp] theorem update_size (self : Buckets α β) (i d h) :
     (self.update i d h).1.size = self.1.size := Array.size_uset _ _ _ h