move(data/bool/*): Move bool files in one folder (#10718)

* renames `data.bool` to `data.bool.basic`
* renames `data.set.bool` to `data.bool.set`
* splits `data.bool.all_any` off `data.list.basic`

src/data/bool/all_any.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import data.list.basic
+
+/-!
+# Boolean quantifiers
+
+This proves a few properties about `list.all` and `list.any`, which are the `bool` universal and
+existential quantifiers. Their definitions are in core Lean.
+-/
+
+variables {α : Type*} {p : α → Prop} [decidable_pred p] {l : list α} {a : α}
+
+namespace list
+
+@[simp] theorem all_nil (p : α → bool) : all [] p = tt := rfl
+
+@[simp] theorem all_cons (p : α → bool) (a : α) (l : list α) : all (a::l) p = (p a && all l p) :=
+rfl
+
+theorem all_iff_forall {p : α → bool} : all l p ↔ ∀ a ∈ l, p a :=
+begin
+  induction l with a l ih,
+  { exact iff_of_true rfl (forall_mem_nil _) },
+  simp only [all_cons, band_coe_iff, ih, forall_mem_cons]
+end
+
+theorem all_iff_forall_prop : all l (λ a, p a) ↔ ∀ a ∈ l, p a :=
+by simp only [all_iff_forall, bool.of_to_bool_iff]
+
+@[simp] theorem any_nil (p : α → bool) : any [] p = ff := rfl
+
+@[simp] theorem any_cons (p : α → bool) (a : α) (l : list α) : any (a :: l) p = (p a || any l p) :=
+rfl
+
+theorem any_iff_exists {p : α → bool} : any l p ↔ ∃ a ∈ l, p a :=
+begin
+  induction l with a l ih,
+  { exact iff_of_false bool.not_ff (not_exists_mem_nil _) },
+  simp only [any_cons, bor_coe_iff, ih, exists_mem_cons_iff]
+end
+
+theorem any_iff_exists_prop : any l (λ a, p a) ↔ ∃ a ∈ l, p a := by simp [any_iff_exists]
+
+theorem any_of_mem {p : α → bool} (h₁ : a ∈ l) (h₂ : p a) : any l p := any_iff_exists.2 ⟨_, h₁, h₂⟩
+
+@[priority 500] instance decidable_forall_mem (l : list α) : decidable (∀ x ∈ l, p x) :=
+decidable_of_iff _ all_iff_forall_prop
+
+instance decidable_exists_mem (l : list α) : decidable (∃ x ∈ l, p x) :=
+decidable_of_iff _ any_iff_exists_prop
+
+end list

src/data/bool.lean → src/data/bool/basic.lean

@@ -65,7 +65,7 @@ by by_cases p; by_cases q; simp *
   to_bool p = to_bool q ↔ (p ↔ q) :=
 ⟨λ h, (coe_to_bool p).symm.trans $ by simp [h], to_bool_congr⟩
 
-lemma not_ff : ¬ ff := by simp
+lemma not_ff : ¬ ff := ff_ne_tt
 
 @[simp] theorem default_bool : default bool = ff := rfl
 

src/data/set/bool.lean → src/data/bool/set.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
+import data.bool.basic
 import data.set.basic
-import data.bool
 
 /-!
 # Booleans and set operations

src/data/list/basic.lean

@@ -2450,51 +2450,6 @@ begin
   split_ifs; simp [zip_with, join, *],
 end
 
-/-! ### all & any -/
-
-@[simp] theorem all_nil (p : α → bool) : all [] p = tt := rfl
-
-@[simp] theorem all_cons (p : α → bool) (a : α) (l : list α) :
-  all (a::l) p = (p a && all l p) := rfl
-
-theorem all_iff_forall {p : α → bool} {l : list α} : all l p ↔ ∀ a ∈ l, p a :=
-begin
-  induction l with a l ih,
-  { exact iff_of_true rfl (forall_mem_nil _) },
-  simp only [all_cons, band_coe_iff, ih, forall_mem_cons]
-end
-
-theorem all_iff_forall_prop {p : α → Prop} [decidable_pred p]
-  {l : list α} : all l (λ a, p a) ↔ ∀ a ∈ l, p a :=
-by simp only [all_iff_forall, bool.of_to_bool_iff]
-
-@[simp] theorem any_nil (p : α → bool) : any [] p = ff := rfl
-
-@[simp] theorem any_cons (p : α → bool) (a : α) (l : list α) :
-  any (a::l) p = (p a || any l p) := rfl
-
-theorem any_iff_exists {p : α → bool} {l : list α} : any l p ↔ ∃ a ∈ l, p a :=
-begin
-  induction l with a l ih,
-  { exact iff_of_false bool.not_ff (not_exists_mem_nil _) },
-  simp only [any_cons, bor_coe_iff, ih, exists_mem_cons_iff]
-end
-
-theorem any_iff_exists_prop {p : α → Prop} [decidable_pred p]
-  {l : list α} : any l (λ a, p a) ↔ ∃ a ∈ l, p a :=
-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₂⟩
-
-@[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
-
-instance decidable_exists_mem {p : α → Prop} [decidable_pred p] (l : list α) :
-  decidable (∃ x ∈ l, p x) :=
-decidable_of_iff _ any_iff_exists_prop
-
 /-! ### map for partial functions -/
 
 /-- Partial map. If `f : Π a, p a → β` is a partial function defined on

src/data/multiset/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import data.bool.all_any
 import data.list.perm
 import data.list.prod_monoid
 

src/order/complete_lattice.lean

@@ -3,9 +3,9 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import order.bounds
-import data.set.bool
+import data.bool.set
 import data.nat.basic
+import order.bounds
 
 /-!
 # Theory of complete lattices

src/tactic/clear.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-import data.bool
+import data.bool.basic
 import tactic.core
 
 /-!

src/tactic/find_unused.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
-import data.bool
+import data.bool.basic
 import meta.rb_map
 import tactic.core
 

src/tactic/lint/misc.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Robert Y. Lewis
 -/
-import data.bool
+import data.bool.basic
 import meta.rb_map
 import tactic.lint.basic
 

src/tactic/lint/type_classes.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
 -/
-import data.bool
+import data.bool.basic
 import meta.rb_map
 import tactic.lint.basic
 

src/tactic/suggest.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Lucas Allen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lucas Allen, Scott Morrison
 -/
-import data.bool
+import data.bool.basic
 import data.mllist
 import tactic.solve_by_elim