chore: remove cross-cutting dep (#729)

... Data.Array.Lemmas -> Data.Fin.Lemmas

Std/Data/Array.lean

@@ -1,4 +1,5 @@
 import Std.Data.Array.Basic
+import Std.Data.Array.Init.Lemmas
 import Std.Data.Array.Lemmas
 import Std.Data.Array.Match
 import Std.Data.Array.Merge

Std/Data/Array/Init/Lemmas.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2021 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Mario Carneiro, Gabriel Ebner
+-/
+
+/-! # Bootstrapping properties of Arrays -/
+
+namespace Array
+
+@[simp] theorem size_ofFn_go {n} (f : Fin n → α) (i acc) :
+    (ofFn.go f i acc).size = acc.size + (n - i) := by
+  if hin : i < n then
+    unfold ofFn.go
+    have : 1 + (n - (i + 1)) = n - i :=
+      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
+    rw [dif_pos hin, size_ofFn_go f (i+1), size_push, Nat.add_assoc, this]
+  else
+    have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
+    unfold ofFn.go
+    simp [hin, this]
+termination_by n - i
+
+@[simp] theorem size_ofFn (f : Fin n → α) : (ofFn f).size = n := by simp [ofFn]
+
+theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
+    (hki : k < n) (hin : i ≤ n) (hi : i = acc.size)
+    (hacc : ∀ j, ∀ hj : j < acc.size, acc[j] = f ⟨j, Nat.lt_of_lt_of_le hj (hi ▸ hin)⟩) :
+    haveI : acc.size + (n - acc.size) = n := Nat.add_sub_cancel' (hi ▸ hin)
+    (ofFn.go f i acc)[k]'(by simp [*]) = f ⟨k, hki⟩ := by
+  unfold ofFn.go
+  if hin : i < n then
+    have : 1 + (n - (i + 1)) = n - i :=
+      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
+    simp only [dif_pos hin]
+    rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]
+    cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
+    | inl hj => simp [get_push, hj, hacc j hj]
+    | inr hj => simp [get_push, *]
+  else
+    simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
+termination_by n - i
+
+@[simp] theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h) :
+    (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
+  getElem_ofFn_go _ _ _ (by simp) (by simp) nofun

Std/Data/Array/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro, Gabriel Ebner
 -/
 import Std.Data.Nat.Lemmas
 import Std.Data.List.Lemmas
+import Std.Data.Array.Init.Lemmas
 import Std.Data.Array.Basic
 import Std.Tactic.SeqFocus
 import Std.Util.ProofWanted
@@ -246,43 +247,6 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
     simp [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this] at h
     rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.data.length_reverse ▸ ‹_›)]
 
-@[simp] theorem size_ofFn_go {n} (f : Fin n → α) (i acc) :
-    (ofFn.go f i acc).size = acc.size + (n - i) := by
-  if hin : i < n then
-    unfold ofFn.go
-    have : 1 + (n - (i + 1)) = n - i :=
-      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
-    rw [dif_pos hin, size_ofFn_go f (i+1), size_push, Nat.add_assoc, this]
-  else
-    have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
-    unfold ofFn.go
-    simp [hin, this]
-termination_by n - i
-
-@[simp] theorem size_ofFn (f : Fin n → α) : (ofFn f).size = n := by simp [ofFn]
-
-theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
-    (hki : k < n) (hin : i ≤ n) (hi : i = acc.size)
-    (hacc : ∀ j, ∀ hj : j < acc.size, acc[j] = f ⟨j, Nat.lt_of_lt_of_le hj (hi ▸ hin)⟩) :
-    haveI : acc.size + (n - acc.size) = n := Nat.add_sub_cancel' (hi ▸ hin)
-    (ofFn.go f i acc)[k]'(by simp [*]) = f ⟨k, hki⟩ := by
-  unfold ofFn.go
-  if hin : i < n then
-    have : 1 + (n - (i + 1)) = n - i :=
-      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
-    simp only [dif_pos hin]
-    rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]
-    cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
-    | inl hj => simp [get_push, hj, hacc j hj]
-    | inr hj => simp [get_push, *]
-  else
-    simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
-termination_by n - i
-
-@[simp] theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h) :
-    (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
-  getElem_ofFn_go _ _ _ (by simp) (by simp) nofun
-
 theorem forIn_eq_data_forIn [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
     forIn as b f = forIn as.data b f := by

Std/Data/Fin/Lemmas.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Std.Data.Fin.Basic
-import Std.Data.Array.Lemmas
+import Std.Data.List.Init.Lemmas
+import Std.Data.Array.Init.Lemmas
 
 namespace Fin
 
@@ -24,7 +25,7 @@ attribute [norm_cast] val_last
 @[simp] theorem length_list (n) : (list n).length = n := by simp [list]
 
 @[simp] theorem get_list (i : Fin (list n).length) : (list n).get i = i.cast (length_list n) := by
-  cases i; simp only [list]; rw [←Array.getElem_eq_data_get, getElem_enum, cast_mk]
+  cases i; simp only [list]; rw [← Array.getElem_eq_data_get, getElem_enum, cast_mk]
 
 @[simp] theorem list_zero : list 0 = [] := rfl
 
@@ -55,7 +56,7 @@ theorem foldl_succ (f : α → Fin (n+1) → α) (x) :
     foldl (n+1) f x = foldl n (fun x i => f x i.succ) (f x 0) := foldl_loop ..
 
 theorem foldl_eq_foldl_list (f : α → Fin n → α) (x) : foldl n f x = (list n).foldl f x := by
-  induction n using Nat.recAux generalizing x with
+  induction n generalizing x with
   | zero => rfl
   | succ n ih => rw [foldl_succ, ih, list_succ, List.foldl_cons, List.foldl_map]
 
@@ -69,14 +70,14 @@ theorem foldr_loop_succ (f : Fin n → α → α) (x) (h : m < n) :
 theorem foldr_loop (f : Fin (n+1) → α → α) (x) (h : m+1 ≤ n+1) :
     foldr.loop (n+1) f ⟨m+1, h⟩ x =
       f 0 (foldr.loop n (fun i => f i.succ) ⟨m, Nat.le_of_succ_le_succ h⟩ x) := by
-  induction m using Nat.recAux generalizing x with
+  induction m generalizing x with
   | zero => simp [foldr_loop_zero, foldr_loop_succ]
   | succ m ih => rw [foldr_loop_succ, ih]; rfl
 
 theorem foldr_succ (f : Fin (n+1) → α → α) (x) :
     foldr (n+1) f x = f 0 (foldr n (fun i => f i.succ) x) := foldr_loop ..
 
 theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) : foldr n f x = (list n).foldr f x := by
-  induction n using Nat.recAux with
+  induction n with
   | zero => rfl
   | succ n ih => rw [foldr_succ, ih, list_succ, List.foldr_cons, List.foldr_map]

Std/Data/List.lean

@@ -1,6 +1,7 @@
 import Std.Data.List.Basic
 import Std.Data.List.Count
 import Std.Data.List.Init.Attach
+import Std.Data.List.Init.Lemmas
 import Std.Data.List.Lemmas
 import Std.Data.List.Pairwise
 import Std.Data.List.Perm

Std/Data/List/Init/Lemmas.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+
+/-! # Bootstrapping properties of Lists -/
+
+namespace List
+
+@[ext] theorem ext : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
+  | [], [], _ => rfl
+  | a :: l₁, [], h => nomatch h 0
+  | [], a' :: l₂, h => nomatch h 0
+  | a :: l₁, a' :: l₂, h => by
+    have h0 : some a = some a' := h 0
+    injection h0 with aa; simp only [aa, ext fun n => h (n+1)]
+
+theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
+    (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ :=
+  ext fun n =>
+    if h₁ : n < length l₁ then by
+      rw [get?_eq_get, get?_eq_get, h n h₁ (by rwa [← hl])]
+    else by
+      have h₁ := Nat.le_of_not_lt h₁
+      rw [get?_len_le h₁, get?_len_le]; rwa [← hl]
+
+@[simp] theorem get_map (f : α → β) {l n} : get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) :=
+  Option.some.inj <| by rw [← get?_eq_get, get?_map, get?_eq_get]; rfl
+
+/-! ### foldl / foldr -/
+
+theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) :
+    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
+  induction l generalizing init <;> simp [*]
+
+theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) :
+    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
+  induction l generalizing init <;> simp [*]

Std/Data/List/Lemmas.lean

@@ -7,6 +7,7 @@ import Std.Control.ForInStep.Lemmas
 import Std.Data.Bool
 import Std.Data.Fin.Basic
 import Std.Data.Nat.Lemmas
+import Std.Data.List.Init.Lemmas
 import Std.Data.List.Basic
 import Std.Data.Option.Lemmas
 import Std.Classes.BEq
@@ -780,9 +781,6 @@ theorem get?_inj
       rw [mem_iff_get?]
     exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
 
-@[simp] theorem get_map (f : α → β) {l n} : get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) :=
-  Option.some.inj <| by rw [← get?_eq_get, get?_map, get?_eq_get]; rfl
-
 /--
 If one has `get l i hi` in a formula and `h : l = l'`, one can not `rw h` in the formula as
 `hi` gives `i < l.length` and not `i < l'.length`. The theorem `get_of_eq` can be used to make
@@ -823,23 +821,6 @@ theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
     (x :: xs).get ⟨n, by simp [h]⟩ = (x :: xs).getLast (cons_ne_nil x xs) := by
   rw [getLast_eq_get]; cases h; rfl
 
-@[ext] theorem ext : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
-  | [], [], _ => rfl
-  | a :: l₁, [], h => nomatch h 0
-  | [], a' :: l₂, h => nomatch h 0
-  | a :: l₁, a' :: l₂, h => by
-    have h0 : some a = some a' := h 0
-    injection h0 with aa; simp only [aa, ext fun n => h (n+1)]
-
-theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
-    (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ :=
-  ext fun n =>
-    if h₁ : n < length l₁ then by
-      rw [get?_eq_get, get?_eq_get, h n h₁ (by rwa [← hl])]
-    else by
-      have h₁ := Nat.le_of_not_lt h₁
-      rw [get?_len_le h₁, get?_len_le]; rwa [← hl]
-
 theorem get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a
   | _a::_, 0, rfl => rfl
   | _::l, _+1, e => get!_of_get? (l := l) e
@@ -1985,14 +1966,6 @@ theorem disjoint_of_disjoint_append_right_right (d : Disjoint l (l₁ ++ l₂))
 
 /-! ### foldl / foldr -/
 
-theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) :
-    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
-  induction l generalizing init <;> simp [*]
-
-theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) :
-    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
-  induction l generalizing init <;> simp [*]
-
 theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁)
     (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
   induction l generalizing init <;> simp [*, H]