chore: split Init.Data.Array.Lemmas for better bootstrapping (#5255)

This allows significantly reducing the imports of `Init.Data.List.Impl`.

src/Init/Data/Array.lean

@@ -14,3 +14,4 @@ import Init.Data.Array.Attach
 import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas
 import Init.Data.Array.TakeDrop
+import Init.Data.Array.Bootstrap

src/Init/Data/Array/Basic.lean

@@ -799,9 +799,11 @@ theorem ext' {as bs : Array α} (h : as.data = bs.data) : as = bs := by
 @[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).data = acc.data ++ as := by
   induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
 
-theorem data_toArray (as : List α) : as.toArray.data = as := by
+@[simp] theorem data_toArray (as : List α) : as.toArray.data = as := by
   simp [List.toArray, Array.mkEmpty]
 
+@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
+
 theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
   apply ext'
   simp [toArrayLit, data_toArray]

src/Init/Data/Array/Bootstrap.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+
+prelude
+import Init.Data.List.TakeDrop
+
+/-!
+## Bootstrapping theorems about arrays
+
+This file contains some theorems about `Array` and `List` needed for `Init.Data.List.Impl`.
+-/
+
+namespace Array
+
+theorem foldlM_eq_foldlM_data.aux [Monad m]
+    (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
+    foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.data.drop j).foldlM f b := by
+  unfold foldlM.loop
+  split; split
+  · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
+  · rename_i i; rw [Nat.succ_add] at H
+    simp [foldlM_eq_foldlM_data.aux f arr i (j+1) H]
+    rw (config := {occs := .pos [2]}) [← List.get_drop_eq_drop _ _ ‹_›]
+    rfl
+  · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
+
+theorem foldlM_eq_foldlM_data [Monad m]
+    (f : β → α → m β) (init : β) (arr : Array α) :
+    arr.foldlM f init = arr.data.foldlM f init := by
+  simp [foldlM, foldlM_eq_foldlM_data.aux]
+
+theorem foldl_eq_foldl_data (f : β → α → β) (init : β) (arr : Array α) :
+    arr.foldl f init = arr.data.foldl f init :=
+  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_data ..
+
+theorem foldrM_eq_reverse_foldlM_data.aux [Monad m]
+    (f : α → β → m β) (arr : Array α) (init : β) (i h) :
+    (arr.data.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f arr 0 i h init := by
+  unfold foldrM.fold
+  match i with
+  | 0 => simp [List.foldlM, List.take]
+  | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]; rfl
+
+theorem foldrM_eq_reverse_foldlM_data [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
+    arr.foldrM f init = arr.data.reverse.foldlM (fun x y => f y x) init := by
+  have : arr = #[] ∨ 0 < arr.size :=
+    match arr with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
+  match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
+  simp [foldrM, h, ← foldrM_eq_reverse_foldlM_data.aux, List.take_length]
+
+theorem foldrM_eq_foldrM_data [Monad m]
+    (f : α → β → m β) (init : β) (arr : Array α) :
+    arr.foldrM f init = arr.data.foldrM f init := by
+  rw [foldrM_eq_reverse_foldlM_data, List.foldlM_reverse]
+
+theorem foldr_eq_foldr_data (f : α → β → β) (init : β) (arr : Array α) :
+    arr.foldr f init = arr.data.foldr f init :=
+  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_data ..
+
+@[simp] theorem push_data (arr : Array α) (a : α) : (arr.push a).data = arr.data ++ [a] := by
+  simp [push, List.concat_eq_append]
+
+@[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.data ++ l := by
+  simp [toListAppend, foldr_eq_foldr_data]
+
+@[simp] theorem toList_eq (arr : Array α) : arr.toList = arr.data := by
+  simp [toList, foldr_eq_foldr_data]
+
+@[simp] theorem pop_data (arr : Array α) : arr.pop.data = arr.data.dropLast := rfl
+
+@[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl
+
+@[simp] theorem append_data (arr arr' : Array α) :
+    (arr ++ arr').data = arr.data ++ arr'.data := by
+  rw [← append_eq_append]; unfold Array.append
+  rw [foldl_eq_foldl_data]
+  induction arr'.data generalizing arr <;> simp [*]
+
+@[simp] theorem appendList_eq_append
+    (arr : Array α) (l : List α) : arr.appendList l = arr ++ l := rfl
+
+@[simp] theorem appendList_data (arr : Array α) (l : List α) :
+    (arr ++ l).data = arr.data ++ l := by
+  rw [← appendList_eq_append]; unfold Array.appendList
+  induction l generalizing arr <;> simp [*]
+
+end Array

src/Init/Data/Array/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Lemmas
+import Init.Data.List.Impl
 import Init.Data.List.Monadic
 import Init.Data.List.Range
 import Init.Data.Array.Mem
@@ -29,8 +30,6 @@ attribute [simp] data_toArray uset
 
 @[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
 
-@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
-
 @[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
 theorem getElem_eq_data_getElem (a : Array α) (h : i < a.size) : a[i] = a.data[i] := by
@@ -40,54 +39,6 @@ theorem getElem_eq_data_getElem (a : Array α) (h : i < a.size) : a[i] = a.data[
 theorem getElem_eq_data_get (a : Array α) (h : i < a.size) : a[i] = a.data.get ⟨i, h⟩ := by
   simp [getElem_eq_data_getElem]
 
-theorem foldlM_eq_foldlM_data.aux [Monad m]
-    (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
-    foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.data.drop j).foldlM f b := by
-  unfold foldlM.loop
-  split; split
-  · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
-  · rename_i i; rw [Nat.succ_add] at H
-    simp [foldlM_eq_foldlM_data.aux f arr i (j+1) H]
-    rw (config := {occs := .pos [2]}) [← List.get_drop_eq_drop _ _ ‹_›]
-    rfl
-  · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
-
-theorem foldlM_eq_foldlM_data [Monad m]
-    (f : β → α → m β) (init : β) (arr : Array α) :
-    arr.foldlM f init = arr.data.foldlM f init := by
-  simp [foldlM, foldlM_eq_foldlM_data.aux]
-
-theorem foldl_eq_foldl_data (f : β → α → β) (init : β) (arr : Array α) :
-    arr.foldl f init = arr.data.foldl f init :=
-  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_data ..
-
-theorem foldrM_eq_reverse_foldlM_data.aux [Monad m]
-    (f : α → β → m β) (arr : Array α) (init : β) (i h) :
-    (arr.data.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f arr 0 i h init := by
-  unfold foldrM.fold
-  match i with
-  | 0 => simp [List.foldlM, List.take]
-  | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]; rfl
-
-theorem foldrM_eq_reverse_foldlM_data [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.data.reverse.foldlM (fun x y => f y x) init := by
-  have : arr = #[] ∨ 0 < arr.size :=
-    match arr with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
-  match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
-  simp [foldrM, h, ← foldrM_eq_reverse_foldlM_data.aux, List.take_length]
-
-theorem foldrM_eq_foldrM_data [Monad m]
-    (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.data.foldrM f init := by
-  rw [foldrM_eq_reverse_foldlM_data, List.foldlM_reverse]
-
-theorem foldr_eq_foldr_data (f : α → β → β) (init : β) (arr : Array α) :
-    arr.foldr f init = arr.data.foldr f init :=
-  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_data ..
-
-@[simp] theorem push_data (arr : Array α) (a : α) : (arr.push a).data = arr.data ++ [a] := by
-  simp [push, List.concat_eq_append]
-
 theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
   simp [foldrM_eq_reverse_foldlM_data, -size_push]
@@ -102,12 +53,6 @@ theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α)
 @[simp] theorem foldr_push' (f : α → β → β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldr f init (start := arr.size + 1) = arr.foldr f (f a init) := foldrM_push' ..
 
-@[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.data ++ l := by
-  simp [toListAppend, foldr_eq_foldr_data]
-
-@[simp] theorem toList_eq (arr : Array α) : arr.toList = arr.data := by
-  simp [toList, foldr_eq_foldr_data]
-
 /-- A more efficient version of `arr.toList.reverse`. -/
 @[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
 
@@ -155,24 +100,6 @@ where
   simp only [← data_length]
   simp
 
-@[simp] theorem pop_data (arr : Array α) : arr.pop.data = arr.data.dropLast := rfl
-
-@[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl
-
-@[simp] theorem append_data (arr arr' : Array α) :
-    (arr ++ arr').data = arr.data ++ arr'.data := by
-  rw [← append_eq_append]; unfold Array.append
-  rw [foldl_eq_foldl_data]
-  induction arr'.data generalizing arr <;> simp [*]
-
-@[simp] theorem appendList_eq_append
-    (arr : Array α) (l : List α) : arr.appendList l = arr ++ l := rfl
-
-@[simp] theorem appendList_data (arr : Array α) (l : List α) :
-    (arr ++ l).data = arr.data ++ l := by
-  rw [← appendList_eq_append]; unfold Array.appendList
-  induction l generalizing arr <;> simp [*]
-
 @[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)
 
 @[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :

src/Init/Data/Bool.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: F. G. Dorais
 -/
 prelude
-import Init.BinderPredicates
+import Init.NotationExtra
 
 /-- Boolean exclusive or -/
 abbrev xor : Bool → Bool → Bool := bne

src/Init/Data/List/Impl.lean

@@ -3,9 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-
 prelude
-import Init.Data.Array.Lemmas
+import Init.Data.Array.Bootstrap
 
 /-!
 ## Tail recursive implementations for `List` definitions.

src/Init/Data/List/Lemmas.lean

@@ -8,9 +8,8 @@ import Init.Data.Bool
 import Init.Data.Option.Lemmas
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
-import Init.PropLemmas
 import Init.Control.Lawful.Basic
-import Init.Hints
+import Init.BinderPredicates
 
 /-! # Theorems about `List` operations.
 

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -5,6 +5,7 @@ Authors: Josh Clune
 -/
 prelude
 import Init.Data.List.Erase
+import Init.Data.Array.Lemmas
 import Std.Sat.CNF.Basic
 import Std.Tactic.BVDecide.LRAT.Internal.PosFin
 import Std.Tactic.BVDecide.LRAT.Internal.Assignment