diff --git a/data/list/basic.lean b/data/list/basic.lean
index 44d1a911694be..79237fbc338aa 100644
--- a/data/list/basic.lean
+++ b/data/list/basic.lean
@@ -9,7 +9,7 @@ import
   tactic.interactive tactic.mk_iff_of_inductive_prop tactic.split_ifs
   logic.basic logic.function logic.relation
   algebra.group order.basic
-  data.nat.basic data.option data.bool data.prod data.sigma data.fin
+  data.list.defs data.nat.basic data.option data.bool data.prod data.sigma data.fin
 open function nat
 
 namespace list
@@ -283,12 +283,6 @@ begin
     { simp only [cons_append, @eq_comm _ a, ih, and_assoc, and_or_distrib_left, exists_and_distrib_left] } }
 end
 
-/-- Split a list at an index. `split 2 [a, b, c] = ([a, b], [c])` -/
-def split_at : ℕ → list α → list α × list α
-| 0        a         := ([], a)
-| (succ n) []        := ([], [])
-| (succ n) (x :: xs) := let (l, r) := split_at n xs in (x :: l, r)
-
 @[simp] theorem split_at_eq_take_drop : ∀ (n : ℕ) (l : list α), split_at n l = (take n l, drop n l)
 | 0        a         := rfl
 | (succ n) []        := rfl
@@ -409,11 +403,6 @@ append_bind _ _ _
 
 /- concat -/
 
-/-- Concatenate an element at the end of a list. `concat [a, b] c = [a, b, c]` -/
-@[simp] def concat : list α → α → list α
-| []     a := [a]
-| (b::l) a := b :: concat l a
-
 @[simp] theorem concat_nil (a : α) : concat [] a = [a] := rfl
 
 @[simp] theorem concat_cons (a b : α) (l : list α) : concat (a :: l) b = a :: concat l b := rfl
@@ -517,11 +506,7 @@ theorem last_congr {l₁ l₂ : list α} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ [
   last l₁ h₁ = last l₂ h₂ :=
 by subst l₁
 
-/- head and tail -/
-
-@[simp] def head' : list α → option α
-| []       := none
-| (a :: l) := some a
+/- head(') and tail -/
 
 theorem head_eq_head' [inhabited α] (l : list α) : head l = (head' l).iget :=
 by cases l; refl
@@ -864,33 +849,6 @@ theorem nth_le_reverse_aux2 : ∀ (l r : list α) (i : nat) (h1) (h2),
   nth_le (reverse l) (length l - 1 - i) h1 = nth_le l i h2 :=
 nth_le_reverse_aux2 _ _ _ _ _
 
-/-- Convert a list into an array (whose length is the length of `l`) -/
-def to_array (l : list α) : array l.length α :=
-{data := λ v, l.nth_le v.1 v.2}
-
-/-- "inhabited" `nth` function: returns `default` instead of `none` in the case
-  that the index is out of bounds. -/
-@[simp] def inth [h : inhabited α] (l : list α) (n : nat) : α := (nth l n).iget
-
-/- nth tail operation -/
-
-/-- Apply a function to the nth tail of `l`.
-  `modify_nth_tail f 2 [a, b, c] = [a, b] ++ f [c]`. Returns the input without
-  using `f` if the index is larger than the length of the list. -/
-@[simp] def modify_nth_tail (f : list α → list α) : ℕ → list α → list α
-| 0     l      := f l
-| (n+1) []     := []
-| (n+1) (a::l) := a :: modify_nth_tail n l
-
-/-- Apply `f` to the head of the list, if it exists. -/
-@[simp] def modify_head (f : α → α) : list α → list α
-| []     := []
-| (a::l) := f a :: l
-
-/-- Apply `f` to the nth element of the list, if it exists. -/
-def modify_nth (f : α → α) : ℕ → list α → list α :=
-modify_nth_tail (modify_head f)
-
 lemma modify_nth_tail_modify_nth_tail {f g : list α → list α} (m : ℕ) :
   ∀n (l:list α), (l.modify_nth_tail f n).modify_nth_tail g (m + n) =
     l.modify_nth_tail (λl, (f l).modify_nth_tail g m) n
@@ -981,8 +939,6 @@ by simp only [update_nth_eq_modify_nth, nth_modify_nth_ne _ _ h]
 section insert_nth
 variable {a : α}
 
-def insert_nth (n : ℕ) (a : α) : list α → list α := modify_nth_tail (list.cons a) n
-
 @[simp] lemma insert_nth_nil (a : α) : insert_nth 0 a [] = [a] := rfl
 
 lemma length_insert_nth : ∀n as, n ≤ length as → length (insert_nth n a as) = length as + 1
@@ -1125,10 +1081,6 @@ by cases l; cases n; simp only [update_nth]
 section take'
 variable [inhabited α]
 
-def take' : ∀ n, list α → list α
-| 0     l := []
-| (n+1) l := l.head :: take' n l.tail
-
 @[simp] theorem take'_length : ∀ n l, length (@take' α _ n l) = n
 | 0     l := rfl
 | (n+1) l := congr_arg succ (take'_length _ _)
@@ -1152,15 +1104,7 @@ by rw ← h; apply take'_left
 
 end take'
 
-/- take_while -/
-
-/-- Get the longest initial segment of the list whose members all satisfy `p`.
-  `take_while (λ x, x < 3) [0, 2, 5, 1] = [0, 2]` -/
-def take_while (p : α → Prop) [decidable_pred p] : list α → list α
-| []     := []
-| (a::l) := if p a then a :: take_while l else []
-
-/- foldl, foldr, scanl, scanr -/
+/- foldl, foldr -/
 
 lemma foldl_ext (f g : α → β → α) (a : α)
   {l : list β} (H : ∀ a : α, ∀ b ∈ l, f a b = g a b) :
@@ -1224,20 +1168,7 @@ by rw reverse_reverse l at t; rwa t
 @[simp] theorem reverse_foldl {l : list α} : reverse (foldl (λ t h, h :: t) [] l) = l :=
 by rw ←foldr_reverse; simp
 
-/-- Fold a function `f` over the list from the left, returning the list
-  of partial results. `scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]` -/
-def scanl (f : α → β → α) : α → list β → list α
-| a []     := [a]
-| a (b::l) := a :: scanl (f a b) l
-
-def scanr_aux (f : α → β → β) (b : β) : list α → β × list β
-| []     := (b, [])
-| (a::l) := let (b', l') := scanr_aux l in (f a b', b' :: l')
-
-/-- Fold a function `f` over the list from the right, returning the list
-  of partial results. `scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]` -/
-def scanr (f : α → β → β) (b : β) (l : list α) : list β :=
-let (b', l') := scanr_aux f b l in b' :: l'
+/- scanr -/
 
 @[simp] theorem scanr_nil (f : α → β → β) (b : β) : scanr f b [] = [b] := rfl
 
@@ -1327,9 +1258,7 @@ end mfoldl_mfoldr
 
 /- sum -/
 
-/-- Product of a list. `prod [a, b, c] = ((1 * a) * b) * c` -/
-@[to_additive list.sum]
-def prod [has_mul α] [has_one α] : list α → α := foldl (*) 1
+attribute [to_additive list.sum] list.prod
 attribute [to_additive list.sum.equations._eqn_1] list.prod.equations._eqn_1
 
 section monoid
@@ -1539,7 +1468,7 @@ by simp [any_iff_exists]
 theorem any_of_mem {p : α → bool} {a : α} {l : list α} (h₁ : a ∈ l) (h₂ : p a) : any l p :=
 any_iff_exists.2 ⟨_, h₁, h₂⟩
 
-instance decidable_forall_mem {p : α → Prop} [decidable_pred p] (l : list α) :
+@[priority 500] instance decidable_forall_mem {p : α → Prop} [decidable_pred p] (l : list α) :
   decidable (∀ x ∈ l, p x) :=
 decidable_of_iff _ all_iff_forall_prop
 
@@ -1600,20 +1529,6 @@ by induction l; [refl, simp only [*, pmap, length]]
 section find
 variables {p : α → Prop} [decidable_pred p] {l : list α} {a : α}
 
-/-- `find p l` is the first element of `l` satisfying `p`, or `none` if no such
-  element exists. -/
-def find (p : α → Prop) [decidable_pred p] : list α → option α
-| []     := none
-| (a::l) := if p a then some a else find l
-
-def find_indexes_aux (p : α → Prop) [decidable_pred p] : list α → nat → list nat
-| []     n := []
-| (a::l) n := let t := find_indexes_aux l (succ n) in if p a then n :: t else t
-
-/-- `find_indexes p l` is the list of indexes of elements of `l` that satisfy `p`. -/
-def find_indexes (p : α → Prop) [decidable_pred p] (l : list α) : list nat :=
-find_indexes_aux p l 0
-
 @[simp] theorem find_nil (p : α → Prop) [decidable_pred p] : find p [] = none :=
 rfl
 
@@ -1654,17 +1569,6 @@ end find
 section lookmap
 variables (f : α → option α)
 
-/-- `lookmap` is a combination of `lookup` and `filter_map`.
-  `lookmap f l` will apply `f : α → option α` to each element of the list,
-  replacing `a -> b` at the first value `a` in the list such that `f a = some b`. -/
-def lookmap (f : α → option α) : list α → list α
-| []     := []
-| (a::l) :=
-  match f a with
-  | some b := b :: l
-  | none   := a :: lookmap l
-  end
-
 @[simp] theorem lookmap_nil : [].lookmap f = [] := rfl
 
 @[simp] theorem lookmap_cons_none {a : α} (l : list α) (h : f a = none) :
@@ -1713,10 +1617,6 @@ by rw [← length_map, lookmap_map_eq _ (λ _, ()), length_map]; simp
 
 end lookmap
 
-/-- `indexes_of a l` is the list of all indexes of `a` in `l`.
-  `indexes_of a [a, b, a, a] = [0, 2, 3]` -/
-def indexes_of [decidable_eq α] (a : α) : list α → list nat := find_indexes (eq a)
-
 /- filter_map -/
 
 @[simp] theorem filter_map_nil (f : α → option β) : filter_map f [] = [] := rfl
@@ -1891,11 +1791,6 @@ by rw [← filter_map_eq_map, filter_filter_map, filter_map_filter]; refl
 | (a::l) := if pa : p a then by rw [take_while, drop_while, if_pos pa, if_pos pa, cons_append, take_while_append_drop l]
     else by rw [take_while, drop_while, if_neg pa, if_neg pa, nil_append]
 
-/-- `countp p l` is the number of elements of `l` that satisfy `p`. -/
-def countp (p : α → Prop) [decidable_pred p] : list α → nat
-| []      := 0
-| (x::xs) := if p x then succ (countp xs) else countp xs
-
 @[simp] theorem countp_nil (p : α → Prop) [decidable_pred p] : countp p [] = 0 := rfl
 
 @[simp] theorem countp_cons_of_pos {a : α} (l) (pa : p a) : countp p (a::l) = countp p l + 1 :=
@@ -1929,9 +1824,6 @@ end filter
 section count
 variable [decidable_eq α]
 
-/-- `count a l` is the number of occurrences of `a` in `l`. -/
-def count (a : α) : list α → nat := countp (eq a)
-
 @[simp] theorem count_nil (a : α) : count a [] = 0 := rfl
 
 theorem count_cons (a b : α) (l : list α) :
@@ -1990,22 +1882,6 @@ end count
 
 /- prefix, suffix, infix -/
 
-/-- `is_prefix l₁ l₂`, or `l₁ <+: l₂`, means that `l₁` is a prefix of `l₂`,
-  that is, `l₂` has the form `l₁ ++ t` for some `t`. -/
-def is_prefix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, l₁ ++ t = l₂
-
-/-- `is_suffix l₁ l₂`, or `l₁ <:+ l₂`, means that `l₁` is a suffix of `l₂`,
-  that is, `l₂` has the form `t ++ l₁` for some `t`. -/
-def is_suffix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, t ++ l₁ = l₂
-
-/-- `is_infix l₁ l₂`, or `l₁ <:+: l₂`, means that `l₁` is a contiguous
-  substring of `l₂`, that is, `l₂` has the form `s ++ l₁ ++ t` for some `s, t`. -/
-def is_infix (l₁ : list α) (l₂ : list α) : Prop := ∃ s t, s ++ l₁ ++ t = l₂
-
-infix ` <+: `:50 := is_prefix
-infix ` <:+ `:50 := is_suffix
-infix ` <:+: `:50 := is_infix
-
 @[simp] theorem prefix_append (l₁ l₂ : list α) : l₁ <+: l₁ ++ l₂ := ⟨l₂, rfl⟩
 
 @[simp] theorem suffix_append (l₁ l₂ : list α) : l₂ <:+ l₁ ++ l₂ := ⟨l₁, rfl⟩
@@ -2165,12 +2041,6 @@ instance decidable_suffix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidab
     decidable_of_iff' (l₁ = drop (len2-len1) l₂) suffix_iff_eq_drop
   else is_false $ λ h, hl $ length_le_of_sublist $ sublist_of_suffix h
 
-/-- `inits l` is the list of initial segments of `l`.
-  `inits [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]` -/
-@[simp] def inits : list α → list (list α)
-| []     := [[]]
-| (a::l) := [] :: map (λt, a::t) (inits l)
-
 @[simp] theorem mem_inits : ∀ (s t : list α), s ∈ inits t ↔ s <+: t
 | s []     := suffices s = nil ↔ s <+: nil, by simpa only [inits, mem_singleton],
   ⟨λh, h.symm ▸ prefix_refl [], eq_nil_of_prefix_nil⟩
@@ -2186,12 +2056,6 @@ instance decidable_suffix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidab
     by rw ba; exact ⟨_, (mem_inits _ _).2 ⟨_, st⟩, rfl⟩
   end⟩
 
-/-- `tails l` is the list of terminal segments of `l`.
-  `tails [1, 2, 3] = [[1, 2, 3], [2, 3], [3], []]` -/
-@[simp] def tails : list α → list (list α)
-| []     := [[]]
-| (a::l) := (a::l) :: tails l
-
 @[simp] theorem mem_tails : ∀ (s t : list α), s ∈ tails t ↔ s <:+ t
 | s []     := by simp only [tails, mem_singleton]; exact ⟨λh, by rw h; exact suffix_refl [], eq_nil_of_suffix_nil⟩
 | s (a::t) := by simp only [tails, mem_cons_iff, mem_tails s t]; exact show s = a :: t ∨ s <:+ t ↔ s <:+ a :: t, from
@@ -2213,18 +2077,6 @@ instance decidable_infix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidabl
 
 /- sublists -/
 
-def sublists'_aux : list α → (list α → list β) → list (list β) → list (list β)
-| []     f r := f [] :: r
-| (a::l) f r := sublists'_aux l f (sublists'_aux l (f ∘ cons a) r)
-
-/-- `sublists' l` is the list of all (non-contiguous) sublists of `l`.
-  It differs from `sublists` only in the order of appearance of the sublists;
-  `sublists'` uses the first element of the list as the MSB,
-  `sublists` uses the first element of the list as the LSB.
-  `sublists' [1, 2, 3] = [[], [3], [2], [2, 3], [1], [1, 3], [1, 2], [1, 2, 3]]` -/
-def sublists' (l : list α) : list (list α) :=
-sublists'_aux l id []
-
 @[simp] theorem sublists'_nil : sublists' (@nil α) = [[]] := rfl
 
 @[simp] theorem sublists'_singleton (a : α) : sublists' [a] = [[], [a]] := rfl
@@ -2264,23 +2116,10 @@ end
 | (a::l) := by simp only [sublists'_cons, length_append, length_sublists' l, length_map,
     length, pow_succ, mul_succ, mul_zero, zero_add]
 
-def sublists_aux : list α → (list α → list β → list β) → list β
-| []     f := []
-| (a::l) f := f [a] (sublists_aux l (λys r, f ys (f (a :: ys) r)))
-
-/-- `sublists l` is the list of all (non-contiguous) sublists of `l`.
-  `sublists [1, 2, 3] = [[], [1], [2], [1, 2], [3], [1, 3], [2, 3], [1, 2, 3]]` -/
-def sublists (l : list α) : list (list α) :=
-[] :: sublists_aux l cons
-
 @[simp] theorem sublists_nil : sublists (@nil α) = [[]] := rfl
 
 @[simp] theorem sublists_singleton (a : α) : sublists [a] = [[], [a]] := rfl
 
-def sublists_aux₁ : list α → (list α → list β) → list β
-| []     f := []
-| (a::l) f := f [a] ++ sublists_aux₁ l (λys, f ys ++ f (a :: ys))
-
 theorem sublists_aux₁_eq_sublists_aux : ∀ l (f : list α → list β),
   sublists_aux₁ l f = sublists_aux l (λ ys r, f ys ++ r)
 | []     f := rfl
@@ -2391,19 +2230,6 @@ reverse_rec_on l (nil_sublist _) $
   mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by refl⟩).trans
 ((append_sublist_append_right _).2 IH)
 
-/- transpose -/
-
-def transpose_aux : list α → list (list α) → list (list α)
-| []     ls      := ls
-| (a::i) []      := [a] :: transpose_aux i []
-| (a::i) (l::ls) := (a::l) :: transpose_aux i ls
-
-/-- transpose of a list of lists, treated as a matrix.
-  `transpose [[1, 2], [3, 4], [5, 6]] = [[1, 3, 5], [2, 4, 6]]` -/
-def transpose : list (list α) → list (list α)
-| []      := []
-| (l::ls) := transpose_aux l (transpose ls)
-
 /- forall₂ -/
 
 section forall₂
@@ -2611,13 +2437,6 @@ end forall₂
 
 /- sections -/
 
-/-- List of all sections through a list of lists. A section
-  of `[L₁, L₂, ..., Lₙ]` is a list whose first element comes from
-  `L₁`, whose second element comes from `L₂`, and so on. -/
-def sections : list (list α) → list (list α)
-| []     := [[]]
-| (l::L) := bind (sections L) $ λ s, map (λ a, a::s) l
-
 theorem mem_sections {L : list (list α)} {f} : f ∈ sections L ↔ forall₂ (∈) f L :=
 begin
   refine ⟨λ h, _, λ h, _⟩,
@@ -2642,41 +2461,6 @@ lemma rel_sections {r : α → β → Prop} : (forall₂ (forall₂ r) ⇒ foral
 
 section permutations
 
-def permutations_aux2 (t : α) (ts : list α) (r : list β) : list α → (list α → β) → list α × list β
-| []      f := (ts, r)
-| (y::ys) f := let (us, zs) := permutations_aux2 ys (λx : list α, f (y::x)) in
-               (y :: us, f (t :: y :: us) :: zs)
-
-private def meas : (Σ'_:list α, list α) → ℕ × ℕ | ⟨l, i⟩ := (length l + length i, length l)
-
-local infix ` ≺ `:50 := inv_image (prod.lex (<) (<)) meas
-
-@[elab_as_eliminator] def permutations_aux.rec {C : list α → list α → Sort v}
-  (H0 : ∀ is, C [] is)
-  (H1 : ∀ t ts is, C ts (t::is) → C is [] → C (t::ts) is) : ∀ l₁ l₂, C l₁ l₂
-| []      is := H0 is
-| (t::ts) is :=
-  have h1 : ⟨ts, t :: is⟩ ≺ ⟨t :: ts, is⟩, from
-    show prod.lex _ _ (succ (length ts + length is), length ts) (succ (length ts) + length is, length (t :: ts)),
-    by rw nat.succ_add; exact prod.lex.right _ _ (lt_succ_self _),
-  have h2 : ⟨is, []⟩ ≺ ⟨t :: ts, is⟩, from prod.lex.left _ _ _ (lt_add_of_pos_left _ (succ_pos _)),
-  H1 t ts is (permutations_aux.rec ts (t::is)) (permutations_aux.rec is [])
-using_well_founded {
-  dec_tac := tactic.assumption,
-  rel_tac := λ _ _, `[exact ⟨(≺), @inv_image.wf _ _ _ meas (prod.lex_wf lt_wf lt_wf)⟩] }
-
-def permutations_aux : list α → list α → list (list α) :=
-@@permutations_aux.rec (λ _ _, list (list α)) (λ is, [])
-  (λ t ts is IH1 IH2, foldr (λy r, (permutations_aux2 t ts r y id).2) IH1 (is :: IH2))
-
-/-- List of all permutations of `l`.
-
-     permutations [1, 2, 3] =
-       [[1, 2, 3], [2, 1, 3], [3, 2, 1],
-        [2, 3, 1], [3, 1, 2], [1, 3, 2]] -/
-def permutations (l : list α) : list (list α) :=
-l :: permutations_aux l []
-
 @[simp] theorem permutations_aux_nil (is : list α) : permutations_aux [] is = [] :=
 by rw [permutations_aux, permutations_aux.rec]
 
@@ -2736,10 +2520,6 @@ end insert
 section erasep
 variables {p : α → Prop} [decidable_pred p]
 
-def erasep (p : α → Prop) [decidable_pred p] : list α → list α
-| []     := []
-| (a::l) := if p a then l else a :: erasep l
-
 @[simp] theorem erasep_nil : [].erasep p = [] := rfl
 
 theorem erasep_cons (a : α) (l : list α) : (a :: l).erasep p = if p a then l else a :: l.erasep p := rfl
@@ -2830,11 +2610,6 @@ theorem erasep_map (f : β → α) :
 | []     := rfl
 | (b::l) := by by_cases p (f b); simp [h, erasep_map l]
 
-def extractp (p : α → Prop) [decidable_pred p] : list α → option α × list α
-| []     := (none, [])
-| (a::l) := if p a then (some a, l) else
-  let (a', l') := extractp l in (a', a :: l')
-
 @[simp] theorem extractp_eq_find_erasep :
   ∀ l : list α, extractp p l = (find p l, erasep p l)
 | []     := rfl
@@ -3064,8 +2839,6 @@ theorem unzip_zip {l₁ : list α} {l₂ : list β} (h : length l₁ = length l
 by rw [← @prod.mk.eta _ _ (unzip (zip l₁ l₂)),
   unzip_zip_left (le_of_eq h), unzip_zip_right (ge_of_eq h)]
 
-def revzip (l : list α) : list (α × α) := zip l l.reverse
-
 @[simp] theorem length_revzip (l : list α) : length (revzip l) = length l :=
 by simp only [revzip, length_zip, length_reverse, min_self]
 
@@ -3114,12 +2887,6 @@ by simp only [enum, enum_from_nth, zero_add]; intros; refl
 
 /- product -/
 
-/-- `product l₁ l₂` is the list of pairs `(a, b)` where `a ∈ l₁` and `b ∈ l₂`.
-
-     product [1, 2] [5, 6] = [(1, 5), (1, 6), (2, 5), (2, 6)] -/
-def product (l₁ : list α) (l₂ : list β) : list (α × β) :=
-l₁.bind $ λ a, l₂.map $ prod.mk a
-
 @[simp] theorem nil_product (l : list β) : product (@nil α) l = [] := rfl
 
 @[simp] theorem product_cons (a : α) (l₁ : list α) (l₂ : list β)
@@ -3145,12 +2912,6 @@ by induction l₁ with x l₁ IH; [exact (zero_mul _).symm,
 section
 variable {σ : α → Type*}
 
-/-- `sigma l₁ l₂` is the list of dependent pairs `(a, b)` where `a ∈ l₁` and `b ∈ l₂ a`.
-
-     sigma [1, 2] (λ_, [5, 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)] -/
-protected def sigma (l₁ : list α) (l₂ : Π a, list (σ a)) : list (Σ a, σ a) :=
-l₁.bind $ λ a, (l₂ a).map $ sigma.mk a
-
 @[simp] theorem nil_sigma (l : Π a, list (σ a)) : (@nil α).sigma l = [] := rfl
 
 @[simp] theorem sigma_cons (a : α) (l₁ : list α) (l₂ : Π a, list (σ a))
@@ -3172,12 +2933,6 @@ simp only [map, sigma_cons, length_append, length_map, IH, sum_cons]]
 end
 
 /- of_fn -/
-def of_fn_aux {n} (f : fin n → α) : ∀ m, m ≤ n → list α → list α
-| 0        h l := l
-| (succ m) h l := of_fn_aux m (le_of_lt h) (f ⟨m, h⟩ :: l)
-
-def of_fn {n} (f : fin n → α) : list α :=
-of_fn_aux f n (le_refl _) []
 
 theorem length_of_fn_aux {n} (f : fin n → α) :
   ∀ m h l, length (of_fn_aux f m h l) = length l + m
@@ -3187,9 +2942,6 @@ theorem length_of_fn_aux {n} (f : fin n → α) :
 @[simp] theorem length_of_fn {n} (f : fin n → α) : length (of_fn f) = n :=
 (length_of_fn_aux f _ _ _).trans (zero_add _)
 
-def of_fn_nth_val {n} (f : fin n → α) (i : ℕ) : option α :=
-if h : _ then some (f ⟨i, h⟩) else none
-
 theorem nth_of_fn_aux {n} (f : fin n → α) (i) :
   ∀ m h l,
     (∀ i, nth l i = of_fn_nth_val f (i + m)) →
@@ -3237,9 +2989,6 @@ theorem of_fn_nth_le : ∀ l : list α, of_fn (λ i, nth_le l i.1 i.2) = l
 /- disjoint -/
 section disjoint
 
-/-- `disjoint l₁ l₂` means that `l₁` and `l₂` have no elements in common. -/
-def disjoint (l₁ l₂ : list α) : Prop := ∀ ⦃a⦄, a ∈ l₁ → a ∈ l₂ → false
-
 theorem disjoint.symm {l₁ l₂ : list α} (d : disjoint l₁ l₂) : disjoint l₂ l₁
 | a i₂ i₁ := d i₁ i₂
 
@@ -3447,26 +3196,10 @@ end bag_inter
 /- pairwise relation (generalized no duplicate) -/
 
 section pairwise
-variable (R : α → α → Prop)
-
-/-- `pairwise R l` means that all the elements with earlier indexes are
-  `R`-related to all the elements with later indexes.
-
-     pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3
-
-  For example if `R = (≠)` then it asserts `l` has no duplicates,
-  and if `R = (<)` then it asserts that `l` is (strictly) sorted. -/
-inductive pairwise : list α → Prop
-| nil  : pairwise []
-| cons : ∀ {a : α} {l : list α}, (∀ a' ∈ l, R a a') → pairwise l → pairwise (a::l)
-attribute [simp] pairwise.nil
 
 run_cmd tactic.mk_iff_of_inductive_prop `list.pairwise `list.pairwise_iff
 
-variable {R}
-@[simp] theorem pairwise_cons {a : α} {l : list α} :
-  pairwise R (a::l) ↔ (∀ a' ∈ l, R a a') ∧ pairwise R l :=
-⟨λ p, by cases p with a l n p; exact ⟨n, p⟩, λ ⟨n, p⟩, p.cons n⟩
+variable {R : α → α → Prop}
 
 theorem rel_of_pairwise_cons {a : α} {l : list α}
   (p : pairwise R (a::l)) : ∀ {a'}, a' ∈ l → R a a' :=
@@ -3670,22 +3403,9 @@ theorem pairwise_sublists {R} {l : list α} (H : pairwise R l) :
 by have := pairwise_sublists' (pairwise_reverse.2 H);
    rwa [sublists'_reverse, pairwise_map] at this
 
-variable [decidable_rel R]
-
-instance decidable_pairwise (l : list α) : decidable (pairwise R l) :=
-by induction l with hd tl ih; [exact is_true (pairwise.nil _),
-  exactI decidable_of_iff' _ pairwise_cons]
-
 /- pairwise reduct -/
 
-/-- `pw_filter R l` is a maximal sublist of `l` which is `pairwise R`.
-  `pw_filter (≠)` is the erase duplicates function, and `pw_filter (<)` finds
-  a maximal increasing subsequence in `l`. For example,
-
-     pw_filter (<) [0, 1, 5, 2, 6, 3, 4] = [0, 1, 5, 6] -/
-def pw_filter (R : α → α → Prop) [decidable_rel R] : list α → list α
-| []        := []
-| (x :: xs) := let IH := pw_filter xs in if ∀ y ∈ IH, R x y then x :: IH else IH
+variable [decidable_rel R]
 
 @[simp] theorem pw_filter_nil : pw_filter R [] = [] := rfl
 
@@ -3751,21 +3471,10 @@ end pairwise
 /- chain relation (conjunction of R a b ∧ R b c ∧ R c d ...) -/
 
 section chain
-variable (R : α → α → Prop)
-
-/-- `chain R a l` means that `R` holds between adjacent elements of `a::l`.
-  `chain R a [b, c, d] ↔ R a b ∧ R b c ∧ R c d` -/
-inductive chain : α → list α → Prop
-| nil  (a : α) : chain a []
-| cons : ∀ {a b : α} {l : list α}, R a b → chain b l → chain a (b::l)
-attribute [simp] chain.nil
 
 run_cmd tactic.mk_iff_of_inductive_prop `list.chain `list.chain_iff
 
-variable {R}
-@[simp] theorem chain_cons {a b : α} {l : list α} :
-  chain R a (b::l) ↔ R a b ∧ chain R b l :=
-⟨λ p, by cases p with _ a b l n p; exact ⟨n, p⟩, λ ⟨n, p⟩, p.cons n⟩
+variable {R : α → α → Prop}
 
 theorem rel_of_chain_cons {a b : α} {l : list α}
   (p : chain R a (b::l)) : R a b :=
@@ -3830,17 +3539,10 @@ theorem chain_iff_pairwise (tr : transitive R) {a : α} {l : list α} :
   show ∀ x ∈ l, R b x, from λ x m, (tr r (rel_of_pairwise_cons IH m)),
 end, chain_of_pairwise⟩
 
-instance decidable_chain [decidable_rel R] (a : α) (l : list α) : decidable (chain R a l) :=
-by induction l generalizing a; simp only [chain.nil, chain_cons]; resetI; apply_instance
-
 end chain
 
 /- no duplicates predicate -/
 
-/-- `nodup l` means that `l` has no duplicates, that is, any element appears at most
-  once in the list. It is defined as `pairwise (≠)`. -/
-def nodup : list α → Prop := pairwise (≠)
-
 section nodup
 
 @[simp] theorem forall_mem_ne {a : α} {l : list α} : (∀ (a' : α), a' ∈ l → ¬a = a') ↔ a ∉ l :=
@@ -3963,9 +3665,6 @@ pairwise_filter_of_pairwise p
 @[simp] theorem nodup_reverse {l : list α} : nodup (reverse l) ↔ nodup l :=
 pairwise_reverse.trans $ by simp only [nodup, ne.def, eq_comm]
 
-instance nodup_decidable [decidable_eq α] : ∀ l : list α, decidable (nodup l) :=
-list.decidable_pairwise
-
 theorem nodup_erase_eq_filter [decidable_eq α] (a : α) {l} (d : nodup l) : l.erase a = filter (≠ a) l :=
 begin
   induction d with b l m d IH, {refl},
@@ -4054,11 +3753,6 @@ end nodup
 section erase_dup
 variable [decidable_eq α]
 
-/-- `erase_dup l` removes duplicates from `l` (taking only the first occurrence).
-
-     erase_dup [1, 2, 2, 0, 1] = [1, 2, 0] -/
-def erase_dup : list α → list α := pw_filter (≠)
-
 @[simp] theorem erase_dup_nil : erase_dup [] = ([] : list α) := rfl
 
 theorem erase_dup_cons_of_mem' {a : α} {l : list α} (h : a ∈ erase_dup l) :
@@ -4106,13 +3800,7 @@ end
 
 end erase_dup
 
-/- iota and range -/
-
-/-- `range' s n` is the list of numbers `[s, s+1, ..., s+n-1]`.
-  It is intended mainly for proving properties of `range` and `iota`. -/
-@[simp] def range' : ℕ → ℕ → list ℕ
-| s 0     := []
-| s (n+1) := s :: range' (s+1) n
+/- iota and range(') -/
 
 @[simp] theorem length_range' : ∀ (s n : ℕ), length (range' s n) = n
 | s 0     := rfl
@@ -4244,22 +3932,6 @@ theorem reverse_range' : ∀ s n : ℕ,
   map prod.fst (enum l) = range l.length :=
 by simp only [enum, enum_from_map_fst, range_eq_range']
 
-def reduce_option {α} : list (option α) → list α :=
-list.filter_map id
-
-def map_head {α} (f : α → α) : list α → list α
-| [] := []
-| (x :: xs) := f x :: xs
-
-def map_last {α} (f : α → α) : list α → list α
-| [] := []
-| [x] := [f x]
-| (x :: xs) := x :: map_last xs
-
-@[simp] def last' {α} : α → list α → α
-| a []     := a
-| a (b::l) := last' b l
-
 theorem last'_mem {α} : ∀ a l, @last' α a l ∈ a :: l
 | a []     := or.inl rfl
 | a (b::l) := or.inr (last'_mem b l)
@@ -4286,8 +3958,7 @@ by rw of_fn_eq_pmap; from nodup_pmap
 
 section tfae
 
-/-- tfae: The Following (propositions) Are Equivalent -/
-def tfae (l : list Prop) : Prop := ∀ x ∈ l, ∀ y ∈ l, x ↔ y
+/- tfae: The Following (propositions) Are Equivalent -/
 
 theorem tfae_nil : tfae [] := forall_mem_nil _
 theorem tfae_singleton (p) : tfae [p] := by simp [tfae]
@@ -4313,7 +3984,7 @@ theorem tfae_of_cycle {a b} {l : list Prop} :
   list.chain (→) a (b::l) → (last' b l → a) → tfae (a::b::l) :=
 begin
   induction l with c l IH generalizing a b; simp [tfae_cons_cons, tfae_singleton] at *,
-  { exact iff.intro },
+  { intros a _ b, exact iff.intro a b },
   intros ab bc ch la,
   have := IH bc ch (ab ∘ la),
   exact ⟨⟨ab, la ∘ (this.2 c (or.inl rfl) _ (last'_mem _ _)).1 ∘ bc⟩, this⟩
@@ -4330,18 +4001,6 @@ end tfae
 section choose
 variables (p : α → Prop) [decidable_pred p] (l : list α)
 
-def choose_x : Π l : list α, Π hp : (∃ a, a ∈ l ∧ p a), { a // a ∈ l ∧ p a }
-| [] hp := false.elim (exists.elim hp (assume a h, not_mem_nil a h.left))
-| (l :: ls) hp := if pl : p l then ⟨l, ⟨or.inl rfl, pl⟩⟩ else
-subtype.rec_on (choose_x ls
-  begin
-    rcases hp with ⟨a, rfl | a_mem_ls, pa⟩,
-    { exfalso; apply pl pa },
-    { exact ⟨a, a_mem_ls, pa⟩ }
-  end) (λ a ⟨a_mem_ls, pa⟩, ⟨a, ⟨or.inr a_mem_ls, pa⟩⟩)
-
-def choose (hp : ∃ a, a ∈ l ∧ p a) : α := choose_x p l hp
-
 lemma choose_spec (hp : ∃ a, a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (choose p l hp) :=
 (choose_x p l hp).property
 
diff --git a/data/list/defs.lean b/data/list/defs.lean
new file mode 100644
index 0000000000000..5c8277980f4bb
--- /dev/null
+++ b/data/list/defs.lean
@@ -0,0 +1,374 @@
+import data.option logic.basic tactic.interactive
+
+namespace list
+
+open function nat
+universes u v w x
+variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
+
+/-- Split a list at an index. `split 2 [a, b, c] = ([a, b], [c])` -/
+def split_at : ℕ → list α → list α × list α
+| 0        a         := ([], a)
+| (succ n) []        := ([], [])
+| (succ n) (x :: xs) := let (l, r) := split_at n xs in (x :: l, r)
+
+/-- Concatenate an element at the end of a list. `concat [a, b] c = [a, b, c]` -/
+@[simp] def concat : list α → α → list α
+| []     a := [a]
+| (b::l) a := b :: concat l a
+
+@[simp] def head' : list α → option α
+| []       := none
+| (a :: l) := some a
+
+/-- Convert a list into an array (whose length is the length of `l`) -/
+def to_array (l : list α) : array l.length α :=
+{data := λ v, l.nth_le v.1 v.2}
+
+/-- "inhabited" `nth` function: returns `default` instead of `none` in the case
+  that the index is out of bounds. -/
+@[simp] def inth [h : inhabited α] (l : list α) (n : nat) : α := (nth l n).iget
+
+/-- Apply a function to the nth tail of `l`.
+  `modify_nth_tail f 2 [a, b, c] = [a, b] ++ f [c]`. Returns the input without
+  using `f` if the index is larger than the length of the list. -/
+@[simp] def modify_nth_tail (f : list α → list α) : ℕ → list α → list α
+| 0     l      := f l
+| (n+1) []     := []
+| (n+1) (a::l) := a :: modify_nth_tail n l
+
+/-- Apply `f` to the head of the list, if it exists. -/
+@[simp] def modify_head (f : α → α) : list α → list α
+| []     := []
+| (a::l) := f a :: l
+
+/-- Apply `f` to the nth element of the list, if it exists. -/
+def modify_nth (f : α → α) : ℕ → list α → list α :=
+modify_nth_tail (modify_head f)
+
+def insert_nth (n : ℕ) (a : α) : list α → list α := modify_nth_tail (list.cons a) n
+
+section take'
+variable [inhabited α]
+
+def take' : ∀ n, list α → list α
+| 0     l := []
+| (n+1) l := l.head :: take' n l.tail
+
+end take'
+
+/-- Get the longest initial segment of the list whose members all satisfy `p`.
+  `take_while (λ x, x < 3) [0, 2, 5, 1] = [0, 2]` -/
+def take_while (p : α → Prop) [decidable_pred p] : list α → list α
+| []     := []
+| (a::l) := if p a then a :: take_while l else []
+
+/-- Fold a function `f` over the list from the left, returning the list
+  of partial results. `scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]` -/
+def scanl (f : α → β → α) : α → list β → list α
+| a []     := [a]
+| a (b::l) := a :: scanl (f a b) l
+
+def scanr_aux (f : α → β → β) (b : β) : list α → β × list β
+| []     := (b, [])
+| (a::l) := let (b', l') := scanr_aux l in (f a b', b' :: l')
+
+/-- Fold a function `f` over the list from the right, returning the list
+  of partial results. `scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]` -/
+def scanr (f : α → β → β) (b : β) (l : list α) : list β :=
+let (b', l') := scanr_aux f b l in b' :: l'
+
+/-- Product of a list. `prod [a, b, c] = ((1 * a) * b) * c` -/
+def prod [has_mul α] [has_one α] : list α → α := foldl (*) 1
+
+/-- `find p l` is the first element of `l` satisfying `p`, or `none` if no such
+  element exists. -/
+def find (p : α → Prop) [decidable_pred p] : list α → option α
+| []     := none
+| (a::l) := if p a then some a else find l
+
+def find_indexes_aux (p : α → Prop) [decidable_pred p] : list α → nat → list nat
+| []     n := []
+| (a::l) n := let t := find_indexes_aux l (succ n) in if p a then n :: t else t
+
+/-- `find_indexes p l` is the list of indexes of elements of `l` that satisfy `p`. -/
+def find_indexes (p : α → Prop) [decidable_pred p] (l : list α) : list nat :=
+find_indexes_aux p l 0
+
+/-- `lookmap` is a combination of `lookup` and `filter_map`.
+  `lookmap f l` will apply `f : α → option α` to each element of the list,
+  replacing `a -> b` at the first value `a` in the list such that `f a = some b`. -/
+def lookmap (f : α → option α) : list α → list α
+| []     := []
+| (a::l) :=
+  match f a with
+  | some b := b :: l
+  | none   := a :: lookmap l
+  end
+
+/-- `indexes_of a l` is the list of all indexes of `a` in `l`.
+  `indexes_of a [a, b, a, a] = [0, 2, 3]` -/
+def indexes_of [decidable_eq α] (a : α) : list α → list nat := find_indexes (eq a)
+
+/-- `countp p l` is the number of elements of `l` that satisfy `p`. -/
+def countp (p : α → Prop) [decidable_pred p] : list α → nat
+| []      := 0
+| (x::xs) := if p x then succ (countp xs) else countp xs
+
+/-- `count a l` is the number of occurrences of `a` in `l`. -/
+def count [decidable_eq α] (a : α) : list α → nat := countp (eq a)
+
+/-- `is_prefix l₁ l₂`, or `l₁ <+: l₂`, means that `l₁` is a prefix of `l₂`,
+  that is, `l₂` has the form `l₁ ++ t` for some `t`. -/
+def is_prefix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, l₁ ++ t = l₂
+
+/-- `is_suffix l₁ l₂`, or `l₁ <:+ l₂`, means that `l₁` is a suffix of `l₂`,
+  that is, `l₂` has the form `t ++ l₁` for some `t`. -/
+def is_suffix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, t ++ l₁ = l₂
+
+/-- `is_infix l₁ l₂`, or `l₁ <:+: l₂`, means that `l₁` is a contiguous
+  substring of `l₂`, that is, `l₂` has the form `s ++ l₁ ++ t` for some `s, t`. -/
+def is_infix (l₁ : list α) (l₂ : list α) : Prop := ∃ s t, s ++ l₁ ++ t = l₂
+
+infix ` <+: `:50 := is_prefix
+infix ` <:+ `:50 := is_suffix
+infix ` <:+: `:50 := is_infix
+
+/-- `inits l` is the list of initial segments of `l`.
+  `inits [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]` -/
+@[simp] def inits : list α → list (list α)
+| []     := [[]]
+| (a::l) := [] :: map (λt, a::t) (inits l)
+
+/-- `tails l` is the list of terminal segments of `l`.
+  `tails [1, 2, 3] = [[1, 2, 3], [2, 3], [3], []]` -/
+@[simp] def tails : list α → list (list α)
+| []     := [[]]
+| (a::l) := (a::l) :: tails l
+
+def sublists'_aux : list α → (list α → list β) → list (list β) → list (list β)
+| []     f r := f [] :: r
+| (a::l) f r := sublists'_aux l f (sublists'_aux l (f ∘ cons a) r)
+
+/-- `sublists' l` is the list of all (non-contiguous) sublists of `l`.
+  It differs from `sublists` only in the order of appearance of the sublists;
+  `sublists'` uses the first element of the list as the MSB,
+  `sublists` uses the first element of the list as the LSB.
+  `sublists' [1, 2, 3] = [[], [3], [2], [2, 3], [1], [1, 3], [1, 2], [1, 2, 3]]` -/
+def sublists' (l : list α) : list (list α) :=
+sublists'_aux l id []
+
+def sublists_aux : list α → (list α → list β → list β) → list β
+| []     f := []
+| (a::l) f := f [a] (sublists_aux l (λys r, f ys (f (a :: ys) r)))
+
+/-- `sublists l` is the list of all (non-contiguous) sublists of `l`.
+  `sublists [1, 2, 3] = [[], [1], [2], [1, 2], [3], [1, 3], [2, 3], [1, 2, 3]]` -/
+def sublists (l : list α) : list (list α) :=
+[] :: sublists_aux l cons
+
+def sublists_aux₁ : list α → (list α → list β) → list β
+| []     f := []
+| (a::l) f := f [a] ++ sublists_aux₁ l (λys, f ys ++ f (a :: ys))
+
+def transpose_aux : list α → list (list α) → list (list α)
+| []     ls      := ls
+| (a::i) []      := [a] :: transpose_aux i []
+| (a::i) (l::ls) := (a::l) :: transpose_aux i ls
+
+/-- transpose of a list of lists, treated as a matrix.
+  `transpose [[1, 2], [3, 4], [5, 6]] = [[1, 3, 5], [2, 4, 6]]` -/
+def transpose : list (list α) → list (list α)
+| []      := []
+| (l::ls) := transpose_aux l (transpose ls)
+
+/-- List of all sections through a list of lists. A section
+  of `[L₁, L₂, ..., Lₙ]` is a list whose first element comes from
+  `L₁`, whose second element comes from `L₂`, and so on. -/
+def sections : list (list α) → list (list α)
+| []     := [[]]
+| (l::L) := bind (sections L) $ λ s, map (λ a, a::s) l
+
+section permutations
+
+def permutations_aux2 (t : α) (ts : list α) (r : list β) : list α → (list α → β) → list α × list β
+| []      f := (ts, r)
+| (y::ys) f := let (us, zs) := permutations_aux2 ys (λx : list α, f (y::x)) in
+               (y :: us, f (t :: y :: us) :: zs)
+
+private def meas : (Σ'_:list α, list α) → ℕ × ℕ | ⟨l, i⟩ := (length l + length i, length l)
+
+local infix ` ≺ `:50 := inv_image (prod.lex (<) (<)) meas
+
+@[elab_as_eliminator] def permutations_aux.rec {C : list α → list α → Sort v}
+  (H0 : ∀ is, C [] is)
+  (H1 : ∀ t ts is, C ts (t::is) → C is [] → C (t::ts) is) : ∀ l₁ l₂, C l₁ l₂
+| []      is := H0 is
+| (t::ts) is :=
+  have h1 : ⟨ts, t :: is⟩ ≺ ⟨t :: ts, is⟩, from
+    show prod.lex _ _ (succ (length ts + length is), length ts) (succ (length ts) + length is, length (t :: ts)),
+    by rw nat.succ_add; exact prod.lex.right _ _ (lt_succ_self _),
+  have h2 : ⟨is, []⟩ ≺ ⟨t :: ts, is⟩, from prod.lex.left _ _ _ (lt_add_of_pos_left _ (succ_pos _)),
+  H1 t ts is (permutations_aux.rec ts (t::is)) (permutations_aux.rec is [])
+using_well_founded {
+  dec_tac := tactic.assumption,
+  rel_tac := λ _ _, `[exact ⟨(≺), @inv_image.wf _ _ _ meas (prod.lex_wf lt_wf lt_wf)⟩] }
+
+def permutations_aux : list α → list α → list (list α) :=
+@@permutations_aux.rec (λ _ _, list (list α)) (λ is, [])
+  (λ t ts is IH1 IH2, foldr (λy r, (permutations_aux2 t ts r y id).2) IH1 (is :: IH2))
+
+/-- List of all permutations of `l`.
+
+     permutations [1, 2, 3] =
+       [[1, 2, 3], [2, 1, 3], [3, 2, 1],
+        [2, 3, 1], [3, 1, 2], [1, 3, 2]] -/
+def permutations (l : list α) : list (list α) :=
+l :: permutations_aux l []
+
+end permutations
+
+def erasep (p : α → Prop) [decidable_pred p] : list α → list α
+| []     := []
+| (a::l) := if p a then l else a :: erasep l
+
+def extractp (p : α → Prop) [decidable_pred p] : list α → option α × list α
+| []     := (none, [])
+| (a::l) := if p a then (some a, l) else
+  let (a', l') := extractp l in (a', a :: l')
+
+def revzip (l : list α) : list (α × α) := zip l l.reverse
+
+/-- `product l₁ l₂` is the list of pairs `(a, b)` where `a ∈ l₁` and `b ∈ l₂`.
+
+     product [1, 2] [5, 6] = [(1, 5), (1, 6), (2, 5), (2, 6)] -/
+def product (l₁ : list α) (l₂ : list β) : list (α × β) :=
+l₁.bind $ λ a, l₂.map $ prod.mk a
+
+/-- `sigma l₁ l₂` is the list of dependent pairs `(a, b)` where `a ∈ l₁` and `b ∈ l₂ a`.
+
+     sigma [1, 2] (λ_, [5, 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)] -/
+protected def sigma {σ : α → Type*} (l₁ : list α) (l₂ : Π a, list (σ a)) : list (Σ a, σ a) :=
+l₁.bind $ λ a, (l₂ a).map $ sigma.mk a
+
+def of_fn_aux {n} (f : fin n → α) : ∀ m, m ≤ n → list α → list α
+| 0        h l := l
+| (succ m) h l := of_fn_aux m (le_of_lt h) (f ⟨m, h⟩ :: l)
+
+def of_fn {n} (f : fin n → α) : list α :=
+of_fn_aux f n (le_refl _) []
+
+def of_fn_nth_val {n} (f : fin n → α) (i : ℕ) : option α :=
+if h : _ then some (f ⟨i, h⟩) else none
+
+/-- `disjoint l₁ l₂` means that `l₁` and `l₂` have no elements in common. -/
+def disjoint (l₁ l₂ : list α) : Prop := ∀ ⦃a⦄, a ∈ l₁ → a ∈ l₂ → false
+
+section pairwise
+variables (R : α → α → Prop)
+
+/-- `pairwise R l` means that all the elements with earlier indexes are
+  `R`-related to all the elements with later indexes.
+
+     pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3
+
+  For example if `R = (≠)` then it asserts `l` has no duplicates,
+  and if `R = (<)` then it asserts that `l` is (strictly) sorted. -/
+inductive pairwise : list α → Prop
+| nil  : pairwise []
+| cons : ∀ {a : α} {l : list α}, (∀ a' ∈ l, R a a') → pairwise l → pairwise (a::l)
+
+variables {R}
+@[simp] theorem pairwise_cons {a : α} {l : list α} :
+  pairwise R (a::l) ↔ (∀ a' ∈ l, R a a') ∧ pairwise R l :=
+⟨λ p, by cases p with a l n p; exact ⟨n, p⟩, λ ⟨n, p⟩, p.cons n⟩
+
+instance decidable_pairwise [decidable_rel R] (l : list α) : decidable (pairwise R l) :=
+by induction l with hd tl ih; [exact is_true (pairwise.nil _),
+  exactI decidable_of_iff' _ pairwise_cons]
+
+end pairwise
+
+/-- `pw_filter R l` is a maximal sublist of `l` which is `pairwise R`.
+  `pw_filter (≠)` is the erase duplicates function, and `pw_filter (<)` finds
+  a maximal increasing subsequence in `l`. For example,
+
+     pw_filter (<) [0, 1, 5, 2, 6, 3, 4] = [0, 1, 5, 6] -/
+def pw_filter (R : α → α → Prop) [decidable_rel R] : list α → list α
+| []        := []
+| (x :: xs) := let IH := pw_filter xs in if ∀ y ∈ IH, R x y then x :: IH else IH
+
+section chain
+variable (R : α → α → Prop)
+
+/-- `chain R a l` means that `R` holds between adjacent elements of `a::l`.
+  `chain R a [b, c, d] ↔ R a b ∧ R b c ∧ R c d` -/
+inductive chain : α → list α → Prop
+| nil  (a : α) : chain a []
+| cons : ∀ {a b : α} {l : list α}, R a b → chain b l → chain a (b::l)
+
+variable {R}
+@[simp] theorem chain_cons {a b : α} {l : list α} :
+  chain R a (b::l) ↔ R a b ∧ chain R b l :=
+⟨λ p, by cases p with _ a b l n p; exact ⟨n, p⟩, λ ⟨n, p⟩, p.cons n⟩
+
+instance decidable_chain [decidable_rel R] (a : α) (l : list α) : decidable (chain R a l) :=
+by induction l generalizing a; simp only [chain.nil, chain_cons]; resetI; apply_instance
+
+end chain
+
+/-- `nodup l` means that `l` has no duplicates, that is, any element appears at most
+  once in the list. It is defined as `pairwise (≠)`. -/
+def nodup : list α → Prop := pairwise (≠)
+
+instance nodup_decidable [decidable_eq α] : ∀ l : list α, decidable (nodup l) :=
+list.decidable_pairwise
+
+/-- `erase_dup l` removes duplicates from `l` (taking only the first occurrence).
+
+     erase_dup [1, 2, 2, 0, 1] = [1, 2, 0] -/
+def erase_dup [decidable_eq α] : list α → list α := pw_filter (≠)
+
+/-- `range' s n` is the list of numbers `[s, s+1, ..., s+n-1]`.
+  It is intended mainly for proving properties of `range` and `iota`. -/
+@[simp] def range' : ℕ → ℕ → list ℕ
+| s 0     := []
+| s (n+1) := s :: range' (s+1) n
+
+def reduce_option {α} : list (option α) → list α :=
+list.filter_map id
+
+def map_head {α} (f : α → α) : list α → list α
+| [] := []
+| (x :: xs) := f x :: xs
+
+def map_last {α} (f : α → α) : list α → list α
+| [] := []
+| [x] := [f x]
+| (x :: xs) := x :: map_last xs
+
+@[simp] def last' {α} : α → list α → α
+| a []     := a
+| a (b::l) := last' b l
+
+/- tfae: The Following (propositions) Are Equivalent -/
+def tfae (l : list Prop) : Prop := ∀ x ∈ l, ∀ y ∈ l, x ↔ y
+
+section choose
+variables (p : α → Prop) [decidable_pred p] (l : list α)
+
+def choose_x : Π l : list α, Π hp : (∃ a, a ∈ l ∧ p a), { a // a ∈ l ∧ p a }
+| [] hp := false.elim (exists.elim hp (assume a h, not_mem_nil a h.left))
+| (l :: ls) hp := if pl : p l then ⟨l, ⟨or.inl rfl, pl⟩⟩ else
+subtype.rec_on (choose_x ls
+  begin
+    rcases hp with ⟨a, rfl | a_mem_ls, pa⟩,
+    { exfalso; apply pl pa },
+    { exact ⟨a, a_mem_ls, pa⟩ }
+  end) (λ a ⟨a_mem_ls, pa⟩, ⟨a, ⟨or.inr a_mem_ls, pa⟩⟩)
+
+def choose (hp : ∃ a, a ∈ l ∧ p a) : α := choose_x p l hp
+
+end choose
+
+end list