feat: deprecate _root_.or/and/not/xor

src/Init/Data/BitVec/Lemmas.lean

@@ -729,17 +729,17 @@ instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_co
   exact (Nat.mod_eq_of_lt <| Nat.xor_lt_two_pow x.isLt y.isLt).symm
 
 @[simp] theorem getLsbD_xor {x y : BitVec v} :
-    (x ^^^ y).getLsbD i = (xor (x.getLsbD i) (y.getLsbD i)) := by
+    (x ^^^ y).getLsbD i = (Bool.xor (x.getLsbD i) (y.getLsbD i)) := by
   rw [← testBit_toNat, getLsbD, getLsbD]
   simp
 
 @[simp] theorem getMsbD_xor {x y : BitVec w} :
-    (x ^^^ y).getMsbD i = (xor (x.getMsbD i) (y.getMsbD i)) := by
+    (x ^^^ y).getMsbD i = (Bool.xor (x.getMsbD i) (y.getMsbD i)) := by
   simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
 @[simp] theorem msb_xor {x y : BitVec w} :
-    (x ^^^ y).msb = (xor x.msb y.msb) := by
+    (x ^^^ y).msb = (Bool.xor x.msb y.msb) := by
   simp [BitVec.msb]
 
 @[simp] theorem truncate_xor {x y : BitVec w} :
@@ -1379,7 +1379,7 @@ theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)
   ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
 
 @[simp] theorem cons_xor_cons (x y : BitVec w) (a b : Bool) :
-    (cons a x) ^^^ (cons b y) = cons (xor a b) (x ^^^ y) := by
+    (cons a x) ^^^ (cons b y) = cons (Bool.xor a b) (x ^^^ y) := by
   ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
 
 /-! ### concat -/
@@ -1418,7 +1418,7 @@ theorem getLsbD_concat (x : BitVec w) (b : Bool) (i : Nat) :
   ext i; cases i using Fin.succRecOn <;> simp
 
 @[simp] theorem concat_xor_concat (x y : BitVec w) (a b : Bool) :
-    (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (xor a b) := by
+    (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (Bool.xor a b) := by
   ext i; cases i using Fin.succRecOn <;> simp
 
 /-! ### add -/

src/Init/Data/Bool.lean

@@ -6,16 +6,14 @@ Authors: F. G. Dorais
 prelude
 import Init.NotationExtra
 
-/-- 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
+/-- Boolean exclusive or -/
+abbrev xor : Bool → Bool → Bool := bne
+
+/-- Deprecated alias for `Bool.xor` in the root namespace. -/
+@[deprecated Bool.xor (since := "2024-09-13")] abbrev _root_.xor := Bool.xor
 
 instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
   match inst true, inst false with

src/Init/Data/Nat/Bitwise/Basic.lean

@@ -31,9 +31,9 @@ def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat :=
 decreasing_by apply bitwise_rec_lemma; assumption
 
 @[extern "lean_nat_land"]
-def land : @& Nat → @& Nat → Nat := bitwise and
+def land : @& Nat → @& Nat → Nat := bitwise Bool.and
 @[extern "lean_nat_lor"]
-def lor  : @& Nat → @& Nat → Nat := bitwise or
+def lor  : @& Nat → @& Nat → Nat := bitwise Bool.or
 @[extern "lean_nat_lxor"]
 def xor  : @& Nat → @& Nat → Nat := bitwise bne
 @[extern "lean_nat_shiftl"]

src/Init/Notation.lean

@@ -10,6 +10,16 @@ import Init.Prelude
 import Init.Coe
 set_option linter.missingDocs true -- keep it documented
 
+
+/-- Deprecated copy of `Bool.or` in the root namespace. -/
+abbrev or := Bool.or
+
+/-- Deprecated copy of `Bool.and` in the root namespace. -/
+abbrev and := Bool.and
+
+/-- Deprecated copy of `Bool.not` in the root namespace. -/
+abbrev not := Bool.not
+
 namespace Lean
 
 /--
@@ -332,9 +342,9 @@ macro_rules | `($x == $y) => `(binrel_no_prop% BEq.beq $x $y)
 @[inherit_doc] infixr:30 " ∨  "  => Or
 @[inherit_doc] notation:max "¬" p:40 => Not p
 
-@[inherit_doc] infixl:35 " && " => and
-@[inherit_doc] infixl:30 " || " => or
-@[inherit_doc] notation:max "!" b:40 => not b
+@[inherit_doc] infixl:35 " && " => Bool.and
+@[inherit_doc] infixl:30 " || " => Bool.or
+@[inherit_doc] notation:max "!" b:40 => Bool.not b
 
 @[inherit_doc] notation:50 a:50 " ∈ " b:50 => Membership.mem b a
 /-- `a ∉ b` is negated elementhood. It is notation for `¬ (a ∈ b)`. -/
@@ -761,3 +771,7 @@ macro_rules
   | `(unseal $fs:ident*) => `(attribute [local semireducible] $fs:ident*)
 
 end Parser
+
+attribute [deprecated] or
+attribute [deprecated] and
+attribute [deprecated] not

src/Init/Prelude.lean

@@ -1014,7 +1014,7 @@ with `Or : Prop → Prop → Prop`, which is the propositional connective).
 It is `@[macro_inline]` because it has C-like short-circuiting behavior:
 if `x` is true then `y` is not evaluated.
 -/
-@[macro_inline] def or (x y : Bool) : Bool :=
+@[macro_inline] def Bool.or (x y : Bool) : Bool :=
   match x with
   | true  => true
   | false => y
@@ -1025,7 +1025,7 @@ with `And : Prop → Prop → Prop`, which is the propositional connective).
 It is `@[macro_inline]` because it has C-like short-circuiting behavior:
 if `x` is false then `y` is not evaluated.
 -/
-@[macro_inline] def and (x y : Bool) : Bool :=
+@[macro_inline] def Bool.and (x y : Bool) : Bool :=
   match x with
   | false => false
   | true  => y
@@ -1034,10 +1034,11 @@ if `x` is false then `y` is not evaluated.
 `not x`, or `!x`, is the boolean "not" operation (not to be confused
 with `Not : Prop → Prop`, which is the propositional connective).
 -/
-@[inline] def not : Bool → Bool
+@[inline] def Bool.not : Bool → Bool
   | true  => false
   | false => true
 
+
 /--
 The type of natural numbers, starting at zero. It is defined as an
 inductive type freely generated by "zero is a natural number" and
@@ -3577,8 +3578,8 @@ abbrev mkSimple (s : String) : Name :=
 @[extern "lean_name_eq"]
 protected def beq : (@& Name) → (@& Name) → Bool
   | anonymous, anonymous => true
-  | str p₁ s₁, str p₂ s₂ => and (BEq.beq s₁ s₂) (Name.beq p₁ p₂)
-  | num p₁ n₁, num p₂ n₂ => and (BEq.beq n₁ n₂) (Name.beq p₁ p₂)
+  | str p₁ s₁, str p₂ s₂ => .and (BEq.beq s₁ s₂) (Name.beq p₁ p₂)
+  | num p₁ n₁, num p₂ n₂ => .and (BEq.beq n₁ n₂) (Name.beq p₁ p₂)
   | _,         _         => false
 
 instance : BEq Name where
@@ -3903,7 +3904,7 @@ if it parsed something and `none` otherwise.
 -/
 def getOptional? (stx : Syntax) : Option Syntax :=
   match stx with
-  | Syntax.node _ k args => match and (beq k nullKind) (beq args.size 1) with
+  | Syntax.node _ k args => match .and (beq k nullKind) (beq args.size 1) with
     | true  => some (args.get! 0)
     | false => none
   | _                    => none
@@ -3915,7 +3916,7 @@ def isMissing : Syntax → Bool
 
 /-- Is this syntax a `node` with kind `k`? -/
 def isNodeOf (stx : Syntax) (k : SyntaxNodeKind) (n : Nat) : Bool :=
-  and (stx.isOfKind k) (beq stx.getNumArgs n)
+  .and (stx.isOfKind k) (beq stx.getNumArgs n)
 
 /-- `stx.isIdent` is `true` iff `stx` is an identifier. -/
 def isIdent : Syntax → Bool
@@ -4403,12 +4404,12 @@ def matchesNull (stx : Syntax) (n : Nat) : Bool :=
   identifiers that "look" the same match. This is particularly useful when dealing with identifiers that
   do not actually refer to Lean bindings, e.g. in the `stx` pattern `` `(many($p)) ``. -/
 def matchesIdent (stx : Syntax) (id : Name) : Bool :=
-  and stx.isIdent (beq stx.getId.eraseMacroScopes id.eraseMacroScopes)
+  .and stx.isIdent (beq stx.getId.eraseMacroScopes id.eraseMacroScopes)
 
 /-- Is this syntax a node kind `k` wrapping an `atom _ val`? -/
 def matchesLit (stx : Syntax) (k : SyntaxNodeKind) (val : String) : Bool :=
   match stx with
-  | Syntax.node _ k' args => and (beq k k') (match args.getD 0 Syntax.missing with
+  | Syntax.node _ k' args => .and (beq k k') (match args.getD 0 Syntax.missing with
     | Syntax.atom _ val' => beq val val'
     | _                  => false)
   | _                     => false

src/Lean/Elab/Quotation.lean

@@ -381,7 +381,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
             else uncovered
           | _ => undecided,
         doMatch := fun yes no => do
-          let cond ← ks.foldlM (fun cond k => `(or $cond (Syntax.isOfKind __discr $(quote k)))) (← `(false))
+          let cond ← ks.foldlM (fun cond k => `(Bool.or $cond (Syntax.isOfKind __discr $(quote k)))) (← `(false))
           `(cond $cond $(← yes []) $(← no)),
       }
     else if isAntiquotSuffixSplice quoted then throwErrorAt quoted "unexpected antiquotation splice"

src/Std/Sat/AIG/Basic.lean

@@ -379,7 +379,7 @@ where
       have := h2 h1 h3
       let lval := go lhs decls assign (by omega) h2
       let rval := go rhs decls assign (by omega) h2
-      xor lval linv && xor rval rinv
+      Bool.xor lval linv && Bool.xor rval rinv
 
 /--
 Denotation of an `AIG` at a specific `Entrypoint`.

src/Std/Sat/AIG/CNF.lean

@@ -67,7 +67,7 @@ theorem atomToCNF_eval :
 theorem gateToCNF_eval :
     (gateToCNF output lhs rhs linv rinv).eval assign
       =
-    (assign output == ((xor (assign lhs) linv) && (xor (assign rhs) rinv))) := by
+    (assign output == ((Bool.xor (assign lhs) linv) && (Bool.xor (assign rhs) rinv))) := by
   simp only [CNF.eval, gateToCNF, CNF.Clause.eval, List.all_cons, List.any_cons, beq_false,
     List.any_nil, Bool.or_false, beq_true, List.all_nil, Bool.and_true]
   cases assign output

src/Std/Sat/AIG/CachedGatesLemmas.lean

@@ -32,7 +32,7 @@ private theorem or_as_aig : ∀ (a b : Bool), (!(!a && !b)) = (a || b) := by
 /--
 Encoding of XOR as boolean expression in AIG form.
 -/
-private theorem xor_as_aig : ∀ (a b : Bool), (!(a && b) && !(!a && !b)) = (xor a b) := by
+private theorem xor_as_aig : ∀ (a b : Bool), (!(a && b) && !(!a && !b)) = (Bool.xor a b) := by
   decide
 
 /--
@@ -175,7 +175,7 @@ instance : LawfulOperator α BinaryInput mkXorCached where
 theorem denote_mkXorCached {aig : AIG α} {input : BinaryInput aig} :
     ⟦aig.mkXorCached input, assign⟧
       =
-    xor
+    Bool.xor
       ⟦aig, input.lhs, assign⟧
       ⟦aig, input.rhs, assign⟧
     := by

src/Std/Sat/AIG/Lemmas.lean

@@ -93,9 +93,9 @@ theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
     ⟦aig.mkGate input, assign⟧
       =
     (
-      (xor ⟦aig, input.lhs.ref, assign⟧ input.lhs.inv)
+      (Bool.xor ⟦aig, input.lhs.ref, assign⟧ input.lhs.inv)
         &&
-      (xor ⟦aig, input.rhs.ref, assign⟧ input.rhs.inv)
+      (Bool.xor ⟦aig, input.rhs.ref, assign⟧ input.rhs.inv)
     ) := by
   conv =>
     lhs
@@ -224,9 +224,9 @@ theorem denote_idx_gate {aig : AIG α} {hstart} (h : aig.decls[start] = .gate lh
     ⟦aig, ⟨start, hstart⟩, assign⟧
       =
     (
-      (xor ⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ linv)
+      (Bool.xor ⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ linv)
         &&
-      (xor ⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ rinv)
+      (Bool.xor ⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ rinv)
     ) := by
   unfold denote
   conv =>

src/Std/Sat/CNF/Literal.lean

@@ -21,7 +21,7 @@ namespace Literal
 /--
 Flip the polarity of `l`.
 -/
-def negate (l : Literal α) : Literal α := (l.1, not l.2)
+def negate (l : Literal α) : Literal α := (l.1, !l.2)
 
 end Literal
 

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean

@@ -27,7 +27,7 @@ namespace blastAdd
 theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
     ⟦mkFullAdderOut aig input, assign⟧
       =
-    xor (xor ⟦aig, input.lhs, assign⟧ ⟦aig, input.rhs, assign⟧) ⟦aig, input.cin, assign⟧
+    Bool.xor (Bool.xor ⟦aig, input.lhs, assign⟧ ⟦aig, input.rhs, assign⟧) ⟦aig, input.cin, assign⟧
     := by
   simp only [mkFullAdderOut, Ref.cast_eq, denote_mkXorCached, denote_projected_entry, Bool.bne_assoc,
     Bool.bne_left_inj]
@@ -39,7 +39,7 @@ theorem denote_mkFullAdderCarry (assign : α → Bool) (aig : AIG α) (input : F
       =
     or
       (and
-        (xor
+        (Bool.xor
           ⟦aig, input.lhs, assign⟧
           ⟦aig, input.rhs, assign⟧)
         ⟦aig, input.cin, assign⟧)
@@ -137,7 +137,7 @@ theorem go_get (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig)
 theorem atLeastTwo_eq_halfAdder (lhsBit rhsBit carry : Bool) :
     Bool.atLeastTwo lhsBit rhsBit carry
       =
-    (((xor lhsBit rhsBit) && carry) || (lhsBit && rhsBit)) := by
+    (((Bool.xor lhsBit rhsBit) && carry) || (lhsBit && rhsBit)) := by
   revert lhsBit rhsBit carry
   decide
 

src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean

@@ -33,7 +33,7 @@ def toString : Gate → String
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
   | or => (· || ·)
-  | xor => _root_.xor
+  | xor => Bool.xor
   | beq => (· == ·)
   | imp => (!· || ·)
 

src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean

@@ -21,12 +21,11 @@ theorem sat_negate_iff_not_sat {p : α → Bool} {l : Literal α} : p ⊨ Litera
   simp only [Literal.negate, sat_iff]
   constructor
   · intro h pl
-    rw [sat_iff, h, not.eq_def] at pl
-    split at pl <;> simp_all
+    rw [sat_iff, h] at pl
+    simp at pl
   · intro h
     rw [sat_iff] at h
-    rw [not.eq_def]
-    split <;> simp_all
+    cases h : p l.fst <;> simp_all
 
 theorem unsat_of_limplies_complement [Entails α t] (x : t) (l : Literal α) :
     Limplies α x l → Limplies α x (Literal.negate l) → Unsatisfiable α x := by

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -508,7 +508,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               simp only [← heq, not] at l_ne_b
-              split at l_ne_b <;> simp at l_ne_b
+              simp at l_ne_b
             · next id_ne_idx => simp [id_ne_idx]
           · exact hf
         · exact Or.inr hf

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean

@@ -58,7 +58,7 @@ theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c
     · split
       · next heq =>
         simp only [heq, Literal.negate, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
-        split at negl_ne_v <;> simp_all
+        simp_all
       · next hne =>
         exact pv
   · exists v
@@ -68,7 +68,7 @@ theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c
     · split
       · next heq =>
         simp only [heq, Literal.negate, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
-        split at negl_ne_v <;> simp_all
+        simp_all
       · next hne =>
         exact pv
 

src/Std/Tactic/BVDecide/Normalize/Bool.lean

@@ -46,7 +46,7 @@ attribute [bv_normalize] Bool.and_self_left
 attribute [bv_normalize] Bool.and_self_right
 
 @[bv_normalize]
-theorem Bool.not_xor : ∀ (a b : Bool), !(xor a b) = (a == b) := by decide
+theorem Bool.not_xor : ∀ (a b : Bool), !(Bool.xor a b) = (a == b) := by decide
 
 end Normalize
 end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Reflect.lean

@@ -126,7 +126,7 @@ theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
   simp[*]
 
 theorem xor_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (xor lhs' rhs') = (xor lhs rhs) := by
+    (Bool.xor lhs' rhs') = (Bool.xor lhs rhs) := by
   simp[*]
 
 theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :