feat port: Data.List.Basic (#966)

cf9386b56953fb40904843af98b7a80757bbe7f9

Notes so far
There are various problems with theorems already having been ported. Sometimes there was a change in universe level order, implicit argument order, or explicit arguments order or explicicity of arguments. In these situations I did the following.
--Ignore the error and align the old lemma when the difference between the two was just universe.
--Align the old lemma with the new lemma but incluce a porting note when the difference was the order of implicit arguments
--Make a new lemma with a `'` at the end when the difference was to do with explicit arguments.

I also added a bunch of definitions that were not imported, possibly with the wrong names. These definitions are
`repeat`, `ret`, `empty`, `init`, `last`, `ilast`

There is a question to be answered about what to do with `list.nth_le`, which is discussed on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/list.2Enth_le)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>

Mathlib/Data/List/Card.lean

@@ -128,7 +128,7 @@ theorem card_subset_le : ∀ {as bs : List α}, as ⊆ bs → card as ≤ card b
       simp [h', card_subset_le hsub']
     | inr h' =>
       have : a ∈ bs := hsub (Mem.head ..)
-      simp [h', card_remove_of_mem this]
+      rw [card_cons_of_not_mem h', card_remove_of_mem this]
       apply Nat.add_le_add_right
       apply card_subset_le
       intro x xmem
@@ -140,10 +140,12 @@ theorem card_map_le (f : α → β) (as : List α) : card (as.map f) ≤ card as
   | nil => simp
   | cons a as ih =>
     cases Decidable.em (f a ∈ map f as) with
-    | inl h => simp [h]; apply Nat.le_trans ih (card_le_card_cons ..)
+    | inl h =>
+      rw [map, card_cons_of_mem h]
+      apply Nat.le_trans ih (card_le_card_cons ..)
     | inr h =>
       have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
-      simp [h, this]
+      rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
       exact Nat.add_le_add_right ih _
 
 theorem card_map_eq_of_inj_on {f : α → β} {as : List α} :
@@ -159,12 +161,12 @@ theorem card_map_eq_of_inj_on {f : α → β} {as : List α} :
         have : a = x := inj_on' (mem_cons_self ..) (mem_cons_of_mem _ hx.1) hx.2
         have h1 : a ∈ as := this ▸ hx.1
         have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
-        simp  [h1, mem_map_of_mem f h1, ih h2]
+        rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
     | inr h =>
       intro inj_on'
       have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
       have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
-      simp [h, h1, ih h2]
+      rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
 
 theorem card_eq_of_equiv {as bs : List α} (h : as.equiv bs) : card as = card bs :=
   let sub_and_sub := equiv_iff_subset_and_subset.1 h

Mathlib/Data/List/Defs.lean

@@ -324,11 +324,7 @@ def permutations' : List α → List (List α)
 
 end Permutations
 
-/-- `erasep p l` removes the first element of `l` satisfying the predicate `p`. -/
-def erasep (p : α → Prop) [DecidablePred p] : List α → List α
-  | [] => []
-  | a :: l => if p a then l else a :: erasep p l
-#align list.erasep List.erasep
+#align list.erasep List.erasePₓ -- prop -> bool
 
 /-- `extractp p l` returns a pair of an element `a` of `l` satisfying the predicate
   `p`, and `l`, with `a` removed. If there is no such element `a` it returns `(none, l)`. -/
@@ -409,8 +405,10 @@ def destutter (R : α → α → Prop) [DecidableRel R] : List α → List α
 
 #align list.range' List.range'
 #align list.reduce_option List.reduceOption
+-- Porting note: replace ilast' by getLastD
 #align list.ilast' List.ilast'
-#align list.last' List.last'
+-- Porting note: remove last' from Std
+#align list.last' List.getLast?
 #align list.rotate List.rotate
 #align list.rotate' List.rotate'
 

Mathlib/Data/Option/Basic.lean

@@ -93,6 +93,11 @@ theorem joinM_eq_join : joinM = @join α :=
 theorem bind_eq_bind {α β : Type _} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=
   rfl
 
+--Porting note: New lemma used to prove a theorem in Data.List.Basic
+theorem map_eq_bind (f : α → β) (o : Option α) :
+  Option.map f o = Option.bind o (some ∘ f) := by
+  cases o <;> rfl
+
 theorem map_coe {α β} {a : α} {f : α → β} : f <$> (a : Option α) = ↑(f a) :=
   rfl
 

Mathlib/Data/Stream/Init.lean

@@ -565,12 +565,12 @@ theorem length_take (n : ℕ) (s : Stream' α) : (take n s).length = n := by
   induction n generalizing s <;> simp [*]
 #align stream.length_take Stream'.length_take
 
-theorem nth_take_succ : ∀ (n : Nat) (s : Stream' α),
-    List.nth (take (succ n) s) n = some (nth s n)
+theorem get?_take_succ : ∀ (n : Nat) (s : Stream' α),
+    List.get? (take (succ n) s) n = some (nth s n)
   | 0, s => rfl
   | n + 1, s => by
-    rw [take_succ, add_one, List.nth, nth_take_succ n]; rfl
-#align stream.nth_take_succ Stream'.nth_take_succ
+    rw [take_succ, add_one, List.get?, get?_take_succ n]; rfl
+#align stream.nth_take_succ Stream'.get?_take_succ
 
 theorem append_take_drop : ∀ (n : Nat) (s : Stream' α),
     appendStream' (take n s) (drop n s) = s := by
@@ -591,7 +591,7 @@ theorem take_theorem (s₁ s₂ : Stream' α) : (∀ n : Nat, take n s₁ = take
     simp [take] at aux
     exact aux
   · have h₁ : some (nth s₁ (succ n)) = some (nth s₂ (succ n)) := by
-      rw [← nth_take_succ, ← nth_take_succ, h (succ (succ n))]
+      rw [← get?_take_succ, ← get?_take_succ, h (succ (succ n))]
     injection h₁
 #align stream.take_theorem Stream'.take_theorem
 

Mathlib/Data/Vector.lean

@@ -143,12 +143,12 @@ theorem map_cons (f : α → β) (a : α) : ∀ v : Vector α n, map f (cons a v
 
 /-- Mapping two vectors under a curried function of two variables. -/
 def map₂ (f : α → β → φ) : Vector α n → Vector β n → Vector φ n
-  | ⟨x, _⟩, ⟨y, _⟩ => ⟨List.map₂ f x y, by simp [*]⟩
+  | ⟨x, _⟩, ⟨y, _⟩ => ⟨List.zipWith f x y, by simp [*]⟩
 #align vector.map₂ Vector.map₂
 
 /-- Vector obtained by repeating an element. -/
 def «repeat» (a : α) (n : ℕ) : Vector α n :=
-  ⟨List.repeat a n, List.length_repeat a n⟩
+  ⟨List.replicate n a, List.length_replicate n a⟩
 #align vector.repeat Vector.repeat
 
 /-- Drop `i` elements from a vector of length `n`; we can have `i > n`. -/

Mathlib/Init/Data/List/Basic.lean

@@ -22,107 +22,63 @@ namespace List
 
 open Option Nat
 
-/-- Optionally return nth element of a list. -/
-@[simp]
-def nth : List α → ℕ → Option α
-  | [], _ => none
-  | a :: _, 0 => some a
-  | _ :: l, n + 1 => nth l n
-#align list.nth List.nth
+#align list.nth List.get?
 
 /-- nth element of a list `l` given `n < l.length`. -/
-def nthLe : ∀ (l : List α) (n), n < l.length → α
-  | [], n, h => absurd h n.not_lt_zero
-  | a :: _, 0, _ => a
-  | _ :: l, n + 1, h => nthLe l n (le_of_succ_le_succ h)
+@[deprecated get]
+def nthLe (l : List α) (n) (h : n < l.length) : α := get l ⟨n, h⟩
 #align list.nth_le List.nthLe
 
+set_option linter.deprecated false in
+@[deprecated]
+theorem nthLe_eq (l : List α) (n) (h : n < l.length) : nthLe l n h = get l ⟨n, h⟩ := rfl
+
 /-- The head of a list, or the default element of the type is the list is `nil`. -/
 @[simp] def headI [Inhabited α] : List α → α
 | []       => default
 | (a :: _) => a
 #align list.head List.headI
 
-/-- Mapping a pair of lists under a curried function of two variables. -/
-@[simp]
-def map₂ (f : α → β → γ) : List α → List β → List γ
-  | [], _ => []
-  | _, [] => []
-  | x :: xs, y :: ys => f x y :: map₂ f xs ys
-
-/-- Auxiliary function for `mapWithIndex`. -/
-def mapWithIndexCore (f : ℕ → α → β) : ℕ → List α → List β
-  | _, [] => []
-  | k, a :: as => f k a :: mapWithIndexCore f (k + 1) as
-#align list.map_with_index_core List.mapWithIndexCore
-
-/-- Given a function `f : ℕ → α → β` and `as : List α`, `as = [a₀, a₁, ...]`, returns the list
-`[f 0 a₀, f 1 a₁, ...]`. -/
-def mapWithIndex (f : ℕ → α → β) (as : List α) : List β :=
-  mapWithIndexCore f 0 as
-#align list.map_with_index List.mapWithIndex
+#align list.map₂ List.zipWith
+
+#noalign list.map_with_index_core
+
+#align list.map_with_index List.mapIdx
 
 /-- Find index of element with given property. -/
-def findIndex (p : α → Prop) [DecidablePred p] : List α → ℕ
-  | [] => 0
-  | a :: l => if p a then 0 else succ (findIndex p l)
+@[deprecated findIdx]
+def findIndex (p : α → Prop) [DecidablePred p] : List α → ℕ := List.findIdx p
 #align list.find_index List.findIndex
 
-/-- Update the nth element of a list. -/
-def updateNth : List α → ℕ → α → List α
-  | _ :: xs, 0, a => a :: xs
-  | x :: xs, i + 1, a => x :: updateNth xs i a
-  | [], _, _ => []
-#align list.update_nth List.updateNth
+#align list.update_nth List.set
 
-/-- Big or of a list of Booleans. -/
-def bor (l : List Bool) : Bool :=
-  any l id
-#align list.bor List.bor
+#align list.bor List.or
 
-/-- Big and of a list of Booleans. -/
-def band (l : List Bool) : Bool :=
-  all l id
-#align list.band List.band
+#align list.band List.and
 
 /-- List consisting of an element `a` repeated a specified number of times. -/
-@[simp]
-def «repeat» (a : α) : Nat → List α
-  | 0 => []
-  | succ n => a :: «repeat» a n
+@[deprecated replicate, simp]
+def «repeat» (a : α) (n : Nat) : List α := List.replicate n a
 #align list.repeat List.repeat
 
-/-- The last element of a non-empty list. -/
-def last : ∀ l : List α, l ≠ [] → α
-  | [], h => absurd rfl h
-  | [a], _ => a
-  | _ :: b :: l, _ => last (b :: l) fun h => List.noConfusion h
-#align list.last List.last
+#align list.last List.getLast
 
 /-- The last element of a list, with the default if list empty -/
-def ilast [Inhabited α] : List α → α
+def getLastI [Inhabited α] : List α → α
   | [] => default
   | [a] => a
   | [_, b] => b
-  | _ :: _ :: l => ilast l
-#align list.ilast List.ilast
+  | _ :: _ :: l => getLastI l
+#align list.ilast List.getLastI
 
-/-- Initial segment of a list, i.e., with the last element dropped. -/
-def init : List α → List α
-  | [] => []
-  | [_] => []
-  | a :: l => a :: init l
-#align list.init List.init
+#align list.init List.dropLast
 
 /-- List with a single given element. -/
-@[inline]
-protected def ret {α : Type u} (a : α) : List α :=
-  [a]
+@[inline] protected def ret {α : Type u} (a : α) : List α := [a]
 #align list.ret List.ret
 
 /-- `≤` implies not `>` for lists. -/
 theorem le_eq_not_gt [LT α] : ∀ l₁ l₂ : List α, (l₁ ≤ l₂) = ¬l₂ < l₁ := fun _ _ => rfl
 #align list.le_eq_not_gt List.le_eq_not_gt
 
-
 end List

Mathlib/Init/Data/List/Lemmas.lean

@@ -18,20 +18,11 @@ open List Nat
 
 namespace List
 
-/-- Length of the list obtained by `map₂` on a pair of lists
-is the length of the shorter of the two. -/
-@[simp]
-theorem length_map₂ (f : α → β → γ) (l₁) : ∀ l₂, length (map₂ f l₁ l₂) =
-    min (length l₁) (length l₂) := by
-  induction l₁ <;> intro l₂ <;> cases l₂ <;>
-    simp [*, add_one, min_succ_succ, Nat.zero_min, Nat.min_zero]
-#align list.length_map₂ List.length_map₂
+#align list.length_map₂ List.length_zipWith
+
+#align list.ball_nil List.forall_mem_nil
+#align list.ball_cons List.forall_mem_consₓ -- explicit → implicit arguments
 
-/-- Length of the list consisting of an element repeated `n` times is `n`. -/
-@[simp]
-theorem length_repeat (a : α) (n : ℕ) : length («repeat»  a n) = n := by
-  induction n <;> simp [*]
-#align list.length_repeat List.length_repeat
 
 section MapAccumr
 

Mathlib/Testing/SlimCheck/Sampleable.lean

@@ -148,7 +148,7 @@ def Fin.shrink {n : Nat} (m : Fin n.succ) :
   let shrinks := Nat.shrink m.val
   shrinks.map (λ x => { x with property := (by
     simp_wf
-    exact Nat.succ_lt_succ $ lt_of_le_of_lt (Nat.mod_le _ _) x.property) })
+    exact lt_of_le_of_lt (Nat.mod_le _ _) x.property) })
 
 instance Fin.shrinkable {n : Nat} : Shrinkable (Fin n.succ) where
   shrink := Fin.shrink