From 65544c31ecad27941286b736c513889d4267cc05 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Fri, 27 Oct 2023 00:02:30 -0400
Subject: [PATCH] feat: `Bool` lemmas (#183)

This migrates a large selection of Mathlib theorems on Booleans to std.
---
 Std.lean                  |   1 +
 Std/Data/Bool.lean        | 256 ++++++++++++++++++++++++++++++++++++++
 Std/Data/List/Lemmas.lean |  32 ++++-
 3 files changed, 286 insertions(+), 3 deletions(-)
 create mode 100644 Std/Data/Bool.lean

diff --git a/Std.lean b/Std.lean
index 9d20895529..a21a629e7b 100644
--- a/Std.lean
+++ b/Std.lean
@@ -25,6 +25,7 @@ import Std.Data.BinomialHeap.Basic
 import Std.Data.BinomialHeap.Lemmas
 import Std.Data.BitVec
 import Std.Data.BitVec.Basic
+import Std.Data.Bool
 import Std.Data.Char
 import Std.Data.DList
 import Std.Data.Fin.Basic
diff --git a/Std/Data/Bool.lean b/Std/Data/Bool.lean
new file mode 100644
index 0000000000..018fdf2471
--- /dev/null
+++ b/Std/Data/Bool.lean
@@ -0,0 +1,256 @@
+/-
+Copyright (c) 2023 F. G. Dorais. No rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: F. G. Dorais
+-/
+
+import Std.Tactic.Alias
+
+/-- Boolean exclusive or -/
+abbrev xor : Bool → Bool → Bool := bne
+
+namespace Bool
+
+/- Namespaced versions that can be used instead of prefixing `_root_` -/
+@[inherit_doc not] protected abbrev not := not
+@[inherit_doc or]  protected abbrev or  := or
+@[inherit_doc and] protected abbrev and := and
+@[inherit_doc xor] protected abbrev xor := xor
+
+instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
+  match inst true, inst false with
+  | isFalse ht, _ => isFalse fun h => absurd (h _) ht
+  | _, isFalse hf => isFalse fun h => absurd (h _) hf
+  | isTrue ht, isTrue hf => isTrue fun | true => ht | false => hf
+
+instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∃ x, p x) :=
+  match inst true, inst false with
+  | isTrue ht, _ => isTrue ⟨_, ht⟩
+  | _, isTrue hf => isTrue ⟨_, hf⟩
+  | isFalse ht, isFalse hf => isFalse fun | ⟨true, h⟩ => absurd h ht | ⟨false, h⟩ => absurd h hf
+
+instance : LE Bool := leOfOrd
+instance : LT Bool := ltOfOrd
+instance : Max Bool := maxOfLe
+instance : Min Bool := minOfLe
+
+/-! ### and -/
+
+@[simp] theorem and_not_self_left : ∀ (x : Bool), (!x && x) = false := by
+  decide
+
+@[simp] theorem and_not_self_right : ∀ (x : Bool), (x && !x) = false := by
+  decide
+
+theorem and_comm : ∀ (x y : Bool), (x && y) = (y && x) := by
+  decide
+
+theorem and_left_comm : ∀ (x y z : Bool), (x && (y && z)) = (y && (x && z)) := by
+  decide
+
+theorem and_right_comm : ∀ (x y z : Bool), ((x && y) && z) = ((x && z) && y) := by
+  decide
+
+theorem and_or_distrib_left : ∀ (x y z : Bool), (x && (y || z)) = ((x && y) || (x && z)) := by
+  decide
+
+theorem and_or_distrib_right : ∀ (x y z : Bool), ((x || y) && z) = ((x && z) || (y && z)) := by
+  decide
+
+theorem and_xor_distrib_left : ∀ (x y z : Bool), (x && xor y z) = xor (x && y) (x && z) := by
+  decide
+
+theorem and_xor_distrib_right : ∀ (x y z : Bool), (xor x y && z) = xor (x && z) (y && z) := by
+  decide
+
+theorem and_deMorgan : ∀ (x y : Bool), (!(x && y)) = (!x || !y) := by
+  decide
+
+theorem and_eq_true_iff : ∀ (x y : Bool), (x && y) = true ↔ x = true ∧ y = true := by
+  decide
+
+theorem and_eq_false_iff : ∀ (x y : Bool), (x && y) = false ↔ x = false ∨ y = false := by
+  decide
+
+alias and_false_left := Bool.false_and
+alias and_false_right := Bool.and_false
+alias and_true_left := Bool.true_and
+alias and_true_right := Bool.and_true
+alias not_and := Bool.and_deMorgan
+
+/-! ### or -/
+
+@[simp] theorem or_not_self_left : ∀ (x : Bool), (!x || x) = true := by
+  decide
+
+@[simp] theorem or_not_self_right : ∀ (x : Bool), (x || !x) = true := by
+  decide
+
+theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by
+  decide
+
+theorem or_left_comm : ∀ (x y z : Bool), (x || (y || z)) = (y || (x || z)) := by
+  decide
+
+theorem or_right_comm : ∀ (x y z : Bool), ((x || y) || z) = ((x || z) || y) := by
+  decide
+
+theorem or_and_distrib_left : ∀ (x y z : Bool), (x || (y && z)) = ((x || y) && (x || z)) := by
+  decide
+
+theorem or_and_distrib_right : ∀ (x y z : Bool), ((x && y) || z) = ((x || z) && (y || z)) := by
+  decide
+
+theorem or_deMorgan : ∀ (x y : Bool), (!(x || y)) = (!x && !y) := by
+  decide
+
+theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by
+  decide
+
+theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by
+  decide
+
+alias or_false_left := Bool.false_or
+alias or_false_right := Bool.or_false
+alias or_true_left := Bool.true_or
+alias or_true_right := Bool.or_true
+alias not_or := Bool.or_deMorgan
+
+/-! ### xor -/
+
+@[simp] theorem xor_false_left : ∀ (x : Bool), xor false x = x := by
+  decide
+
+@[simp] theorem xor_false_right : ∀ (x : Bool), xor x false = x := by
+  decide
+
+@[simp] theorem xor_true_left : ∀ (x : Bool), xor true x = !x := by
+  decide
+
+@[simp] theorem xor_true_right : ∀ (x : Bool), xor x true = !x := by
+  decide
+
+@[simp] theorem xor_not_self_left : ∀ (x : Bool), xor (!x) x = true := by
+  decide
+
+@[simp] theorem xor_not_self_right : ∀ (x : Bool), xor x (!x) = true := by
+  decide
+
+@[simp] theorem xor_not_left : ∀ (x y : Bool), xor (!x) y = !(xor x y) := by
+  decide
+
+@[simp] theorem xor_not_right : ∀ (x y : Bool), xor x (!y) = !(xor x y) := by
+  decide
+
+theorem xor_not_not : ∀ (x y : Bool), xor (!x) (!y) = (xor x y) := by
+  decide
+
+theorem xor_self : ∀ (x : Bool), xor x x = false := by
+  decide
+
+theorem xor_comm : ∀ (x y : Bool), xor x y = xor y x := by
+  decide
+
+theorem xor_left_comm : ∀ (x y z : Bool), xor x (xor y z) = xor y (xor x z) := by
+  decide
+
+theorem xor_right_comm : ∀ (x y z : Bool), xor (xor x y) z = xor (xor x z) y := by
+  decide
+
+theorem xor_assoc : ∀ (x y z : Bool), xor (xor x y) z = xor x (xor y z) := by
+  decide
+
+/-! ### le/lt -/
+
+@[simp] protected theorem le_true : ∀ (x : Bool), x ≤ true := by
+  decide
+
+@[simp] protected theorem false_le : ∀ (x : Bool), false ≤ x := by
+  decide
+
+@[simp] protected theorem le_refl : ∀ (x : Bool), x ≤ x := by
+  decide
+
+@[simp] protected theorem lt_irrefl : ∀ (x : Bool), ¬ x < x := by
+  decide
+
+protected theorem le_trans : ∀ {x y z : Bool}, x ≤ y → y ≤ z → x ≤ z := by
+  decide
+
+protected theorem le_antisymm : ∀ {x y : Bool}, x ≤ y → y ≤ x → x = y := by
+  decide
+
+protected theorem le_total : ∀ (x y : Bool), x ≤ y ∨ y ≤ x := by
+  decide
+
+protected theorem lt_asymm : ∀ {x y : Bool}, x < y → ¬ y < x := by
+  decide
+
+protected theorem lt_trans : ∀ {x y z : Bool}, x < y → y < z → x < z := by
+  decide
+
+protected theorem lt_iff_le_not_le : ∀ {x y : Bool}, x < y ↔ x ≤ y ∧ ¬ y ≤ x := by
+  decide
+
+protected theorem lt_of_le_of_lt : ∀ {x y z : Bool}, x ≤ y → y < z → x < z := by
+  decide
+
+protected theorem lt_of_lt_of_le : ∀ {x y z : Bool}, x < y → y ≤ z → x < z := by
+  decide
+
+protected theorem le_of_lt : ∀ {x y : Bool}, x < y → x ≤ y := by
+  decide
+
+protected theorem le_of_eq : ∀ {x y : Bool}, x = y → x ≤ y := by
+  decide
+
+protected theorem ne_of_lt : ∀ {x y : Bool}, x < y → x ≠ y := by
+  decide
+
+protected theorem lt_of_le_of_ne : ∀ {x y : Bool}, x ≤ y → x ≠ y → x < y := by
+  decide
+
+protected theorem le_of_lt_or_eq : ∀ {x y : Bool}, x < y ∨ x = y → x ≤ y := by
+  decide
+
+protected theorem eq_true_of_true_le : ∀ {x : Bool}, true ≤ x → x = true := by
+  decide
+
+protected theorem eq_false_of_le_false : ∀ {x : Bool}, x ≤ false → x = false := by
+  decide
+
+/-! ### min/max -/
+
+protected theorem max_eq_or : ∀ (x y : Bool), max x y = (x || y) := by
+  decide
+
+protected theorem min_eq_and : ∀ (x y : Bool), min x y = (x && y) := by
+  decide
+
+/-! ### injectivity lemmas -/
+
+theorem not_inj : ∀ {x y : Bool}, (!x) = (!y) → x = y := by
+  decide
+
+theorem not_inj_iff : ∀ {x y : Bool}, (!x) = (!y) ↔ x = y := by
+  decide
+
+theorem and_or_inj_right : ∀ {m x y : Bool}, (x && m) = (y && m) → (x || m) = (y || m) → x = y := by
+  decide
+
+theorem and_or_inj_right_iff :
+    ∀ {m x y : Bool}, (x && m) = (y && m) ∧ (x || m) = (y || m) ↔ x = y := by
+  decide
+
+theorem and_or_inj_left : ∀ {m x y : Bool}, (m && x) = (m && y) → (m || x) = (m || y) → x = y := by
+  decide
+
+theorem and_or_inj_left_iff :
+    ∀ {m x y : Bool}, (m && x) = (m && y) ∧ (m || x) = (m || y) ↔ x = y := by
+  decide
+
+/-! ### deprecated -/
+
+@[deprecated] alias not_inj' := not_inj_iff
+@[deprecated] alias and_or_inj_left' := and_or_inj_left_iff
+@[deprecated] alias and_or_inj_right' := and_or_inj_right_iff
diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 84fea50598..54ad1e6ce0 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -4,6 +4,7 @@ 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
 -/
 import Std.Control.ForInStep.Lemmas
+import Std.Data.Bool
 import Std.Data.Nat.Lemmas
 import Std.Data.List.Basic
 import Std.Data.Option.Lemmas
@@ -987,9 +988,6 @@ theorem length_removeNth : ∀ {l i}, i < length l → length (@removeNth α l i
 
 @[simp] theorem any_eq_true {l : List α} : l.any p ↔ ∃ x ∈ l, p x := by induction l <;> simp [*]
 
-theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (fun c => !p c) := by
-  rw [Bool.eq_iff_iff]; simp; rw [← Bool.not_eq_true, List.any_eq_true]; simp
-
 @[simp] theorem contains_nil [BEq α] : ([] : List α).contains a = false := rfl
 
 @[simp] theorem contains_cons [BEq α] :
@@ -1000,6 +998,34 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (f
 theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by
   induction l with simp | cons b l => cases a == b <;> simp [*]
 
+theorem not_all_eq_any_not (l : List α) (p : α → Bool) : (!l.all p) = l.any fun a => !p a := by
+  induction l with simp | cons _ _ ih => rw [Bool.not_and, ih]
+
+theorem not_any_eq_all_not (l : List α) (p : α → Bool) : (!l.any p) = l.all fun a => !p a := by
+  induction l with simp | cons _ _ ih => rw [Bool.not_or, ih]
+
+theorem or_all_distrib_left (l : List α) (p : α → Bool) (q : Bool) :
+    (q || l.all p) = l.all fun a => q || p a := by
+  induction l with simp | cons _ _ ih => rw [Bool.or_and_distrib_left, ih]
+
+theorem or_all_distrib_right (l : List α) (p : α → Bool) (q : Bool) :
+    (l.all p || q) = l.all fun a => p a || q := by
+  induction l with simp | cons _ _ ih => rw [Bool.or_and_distrib_right, ih]
+
+theorem and_any_distrib_left (l : List α) (p : α → Bool) (q : Bool) :
+    (q && l.any p) = l.any fun a => q && p a := by
+  induction l with simp | cons _ _ ih => rw [Bool.and_or_distrib_left, ih]
+
+theorem and_any_distrib_right (l : List α) (p : α → Bool) (q : Bool) :
+    (l.any p && q) = l.any fun a => p a && q := by
+  induction l with simp | cons _ _ ih => rw [Bool.and_or_distrib_right, ih]
+
+theorem any_eq_not_all_not (l : List α) (p : α → Bool) : l.any p = !l.all (!p .) := by
+  simp only [not_all_eq_any_not, Bool.not_not]
+
+theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!p .) := by
+  simp only [not_any_eq_all_not, Bool.not_not]
+
 /-! ### reverse -/
 
 @[simp] theorem mem_reverseAux {x : α} : ∀ {as bs}, x ∈ reverseAux as bs ↔ x ∈ as ∨ x ∈ bs