chore(data/list): move some sections to separate files (#2341)

* move list.func namespace to its own file

* move erase_dup to its own file

* move rotate to its own file

* move tfae to its own file

* move bag_inter and intervals

* move range out

* move nodup

* move chain and pairwise

* move zip

* move forall2

* move of_fn

* add copyright headers

* remove unnecessary sections, move defns to func.set and tfae

* fixes

* oops, forgot to add file

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/category/traversable/instances.lean

@@ -7,7 +7,7 @@ Instances of `traversable` for types from the core library
 -/
 
 import category.traversable.basic category.basic category.functor category.applicative
-import data.list.basic data.set.lattice
+import data.list.forall2 data.set.lattice
 
 universes u v
 

src/data/int/basic.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad
 
 The integers, with addition, multiplication, and subtraction.
 -/
-import data.nat.basic algebra.char_zero algebra.order_functions
+import data.nat.basic algebra.char_zero algebra.order_functions data.list.range
 open nat
 
 

src/data/list/antidiagonal.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2019 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+import data.list.range
+
+open list function nat
+
+namespace list
+namespace nat
+
+/-- The antidiagonal of a natural number `n` is the list of pairs `(i,j)` such that `i+j = n`. -/
+def antidiagonal (n : ℕ) : list (ℕ × ℕ) :=
+(range (n+1)).map (λ i, (i, n - i))
+
+/-- A pair (i,j) is contained in the antidiagonal of `n` if and only if `i+j=n`. -/
+@[simp] lemma mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} :
+  x ∈ antidiagonal n ↔ x.1 + x.2 = n :=
+begin
+  rw [antidiagonal, mem_map], split,
+  { rintros ⟨i, hi, rfl⟩, rw [mem_range, lt_succ_iff] at hi, exact add_sub_of_le hi },
+  { rintro rfl, refine ⟨x.fst, _, _⟩,
+    { rw [mem_range, add_assoc, lt_add_iff_pos_right], exact zero_lt_succ _ },
+    { exact prod.ext rfl (nat.add_sub_cancel_left _ _) } }
+end
+
+/-- The length of the antidiagonal of `n` is `n+1`. -/
+@[simp] lemma length_antidiagonal (n : ℕ) : (antidiagonal n).length = n+1 :=
+by rw [antidiagonal, length_map, length_range]
+
+/-- The antidiagonal of `0` is the list `[(0,0)]` -/
+@[simp] lemma antidiagonal_zero : antidiagonal 0 = [(0, 0)] :=
+ext_le (length_antidiagonal 0) $ λ n h₁ h₂,
+begin
+  rw [length_antidiagonal, lt_succ_iff, le_zero_iff] at h₁,
+  subst n, simp [antidiagonal]
+end
+
+/-- The antidiagonal of `n` does not contain duplicate entries. -/
+lemma nodup_antidiagonal (n : ℕ) : nodup (antidiagonal n) :=
+nodup_map (@injective_of_left_inverse ℕ (ℕ × ℕ) prod.fst (λ i, (i, n-i)) $ λ i, rfl) (nodup_range _)
+
+end nat
+end list

src/data/list/bag_inter.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Scott Morrison
+-/
+import data.list.basic
+
+namespace list
+
+open nat
+
+/- bag_inter -/
+universe u
+
+variables {α : Type u} [decidable_eq α]
+
+@[simp] theorem nil_bag_inter (l : list α) : [].bag_inter l = [] :=
+by cases l; refl
+
+@[simp] theorem bag_inter_nil (l : list α) : l.bag_inter [] = [] :=
+by cases l; refl
+
+@[simp] theorem cons_bag_inter_of_pos {a} (l₁ : list α) {l₂} (h : a ∈ l₂) :
+  (a :: l₁).bag_inter l₂ = a :: l₁.bag_inter (l₂.erase a) :=
+by cases l₂; exact if_pos h
+
+@[simp] theorem cons_bag_inter_of_neg {a} (l₁ : list α) {l₂} (h : a ∉ l₂) :
+  (a :: l₁).bag_inter l₂ = l₁.bag_inter l₂ :=
+begin
+  cases l₂, {simp only [bag_inter_nil]},
+  simp only [erase_of_not_mem h, list.bag_inter, if_neg h]
+end
+
+@[simp] theorem mem_bag_inter {a : α} : ∀ {l₁ l₂ : list α}, a ∈ l₁.bag_inter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
+| []      l₂ := by simp only [nil_bag_inter, not_mem_nil, false_and]
+| (b::l₁) l₂ := begin
+    by_cases b ∈ l₂,
+    { rw [cons_bag_inter_of_pos _ h, mem_cons_iff, mem_cons_iff, mem_bag_inter],
+      by_cases ba : a = b,
+      { simp only [ba, h, eq_self_iff_true, true_or, true_and] },
+      { simp only [mem_erase_of_ne ba, ba, false_or] } },
+    { rw [cons_bag_inter_of_neg _ h, mem_bag_inter, mem_cons_iff, or_and_distrib_right],
+      symmetry, apply or_iff_right_of_imp,
+      rintro ⟨rfl, h'⟩, exact h.elim h' }
+  end
+
+@[simp] theorem count_bag_inter {a : α} :
+  ∀ {l₁ l₂ : list α}, count a (l₁.bag_inter l₂) = min (count a l₁) (count a l₂)
+| []         l₂ := by simp
+| l₁         [] := by simp
+| (h₁ :: l₁) (h₂ :: l₂) :=
+begin
+  simp only [list.bag_inter, list.mem_cons_iff],
+  by_cases p₁ : h₂ = h₁; by_cases p₂ : h₁ = a,
+  { simp only [p₁, p₂, count_bag_inter, min_succ_succ, erase_cons_head, if_true, mem_cons_iff,
+               count_cons_self, true_or, eq_self_iff_true] },
+  { simp only [p₁, ne.symm p₂, count_bag_inter, count_cons, erase_cons_head, if_true, mem_cons_iff,
+               true_or, eq_self_iff_true, if_false] },
+  { rw p₂ at p₁,
+    by_cases p₃ : a ∈ l₂,
+    { simp only [p₁, ne.symm p₁, p₂, p₃, erase_cons, count_bag_inter, eq.symm (min_succ_succ _ _),
+                 succ_pred_eq_of_pos (count_pos.2 p₃), if_true, mem_cons_iff, false_or,
+                 count_cons_self, eq_self_iff_true, if_false, ne.def, not_false_iff,
+                 count_erase_self, list.count_cons_of_ne] },
+    { simp [ne.symm p₁, p₂, p₃] } },
+  { by_cases p₄ : h₁ ∈ l₂; simp only [ne.symm p₁, ne.symm p₂, p₄, count_bag_inter, if_true, if_false,
+      mem_cons_iff, false_or, eq_self_iff_true, ne.def, not_false_iff,count_erase_of_ne, count_cons_of_ne] }
+end
+
+theorem bag_inter_sublist_left : ∀ l₁ l₂ : list α, l₁.bag_inter l₂ <+ l₁
+| []      l₂ := by simp [nil_sublist]
+| (b::l₁) l₂ := begin
+  by_cases b ∈ l₂; simp [h],
+  { apply cons_sublist_cons, apply bag_inter_sublist_left },
+  { apply sublist_cons_of_sublist, apply bag_inter_sublist_left }
+end
+
+theorem bag_inter_nil_iff_inter_nil : ∀ l₁ l₂ : list α, l₁.bag_inter l₂ = [] ↔ l₁ ∩ l₂ = []
+| []      l₂ := by simp
+| (b::l₁) l₂ :=
+begin
+  by_cases h : b ∈ l₂; simp [h],
+  exact bag_inter_nil_iff_inter_nil l₁ l₂
+end
+
+
+end list