chore: cleanup after export Bool.and/or/not/xor

src/Init/Control/Basic.lean

@@ -28,7 +28,7 @@ Important instances include
 * `Option`, where `failure := none` and `<|>` returns the left-most `some`.
 * Parser combinators typically provide an `Applicative` instance for error-handling and
   backtracking.
-  
+
 Error recovery and state can interact subtly. For example, the implementation of `Alternative` for `OptionT (StateT σ Id)` keeps modifications made to the state while recovering from failure, while `StateT σ (OptionT Id)` discards them.
 -/
 -- NB: List instance is in mathlib. Once upstreamed, add

src/Init/Data/Bool.lean

@@ -6,16 +6,11 @@ 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
 
 instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
   match inst true, inst false with
@@ -597,7 +592,7 @@ theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidab
 
 end Bool
 
-export Bool (cond_eq_if)
+export Bool (cond_eq_if xor and or not)
 
 /-! ### decide -/
 

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

@@ -226,12 +226,12 @@ private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
     simp [Nat.mod_eq (x+2) 2, p, hyp]
     cases Nat.mod_two_eq_zero_or_one x with | _ p => simp [p]
 
-private theorem testBit_succ_zero : testBit (x + 1) 0 = not (testBit x 0) := by
+private theorem testBit_succ_zero : testBit (x + 1) 0 = !(testBit x 0) := by
   simp [testBit_to_div_mod, succ_mod_two]
   cases Nat.mod_two_eq_zero_or_one x with | _ p =>
     simp [p]
 
-theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = not (testBit x i) := by
+theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = !(testBit x i) := by
   simp [testBit_to_div_mod, add_div_left, Nat.two_pow_pos, succ_mod_two]
   cases mod_two_eq_zero_or_one (x / 2 ^ i) with
   | _ p => simp [p]

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,12 @@ 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
 
+export Bool (or and not)
+
 /--
 The type of natural numbers, starting at zero. It is defined as an
 inductive type freely generated by "zero is a natural number" and

src/Lean/Compiler/IR/RC.lean

@@ -91,7 +91,7 @@ private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Na
     | Arg.var y      => x == y && !consumeParamPred i
 
 private def isBorrowParam (x : VarId) (ys : Array Arg) (ps : Array Param) : Bool :=
-  isBorrowParamAux x ys fun i => not ps[i]!.borrow
+  isBorrowParamAux x ys fun i => ! ps[i]!.borrow
 
 /--
 Return `n`, the number of times `x` is consumed.
@@ -124,7 +124,7 @@ private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred :
         addInc ctx x b numIncs
 
 private def addIncBefore (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=
-  addIncBeforeAux ctx xs (fun i => not ps[i]!.borrow) b liveVarsAfter
+  addIncBeforeAux ctx xs (fun i => ! ps[i]!.borrow) b liveVarsAfter
 
 /-- See `addIncBeforeAux`/`addIncBefore` for the procedure that inserts `inc` operations before an application.  -/
 private def addDecAfterFullApp (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody :=

src/Lean/Data/PersistentArray.lean

@@ -317,8 +317,8 @@ variable {m : Type → Type w} [Monad m]
   anyMAux p t.root <||> t.tail.anyM p
 
 @[inline] def allM (a : PersistentArray α) (p : α → m Bool) : m Bool := do
-  let b ← anyM a (fun v => do let b ← p v; pure (not b))
-  pure (not b)
+  let b ← anyM a (fun v => do let b ← p v; pure (!b))
+  pure (!b)
 
 end
 

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -599,7 +599,7 @@ partial def solve {m} {α} [Monad m] (measures : Array α)
             all_le := false
             break
       -- No progress here? Try the next measure
-      if not (has_lt && all_le) then continue
+      if !(has_lt && all_le) then continue
       -- We found a suitable measure, remove it from the list (mild optimization)
       let measures' := measures.eraseIdx measureIdx
       return ← go measures' todo (acc.push measure)

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean

@@ -56,7 +56,7 @@ partial def of (t : Expr) : M (Option ReifiedBVLogical) := do
     let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.false)
     let proof := return mkRefl (mkConst ``Bool.false)
     return some ⟨boolExpr, proof, expr⟩
-  | not subExpr =>
+  | Bool.not subExpr =>
     let some sub ← of subExpr | return none
     let boolExpr := .not sub.bvExpr
     let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
@@ -65,9 +65,9 @@ partial def of (t : Expr) : M (Option ReifiedBVLogical) := do
       let subProof ← sub.evalsAtAtoms
       return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
     return some ⟨boolExpr, proof, expr⟩
-  | or lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.Bool.or_congr
-  | and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
-  | xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
+  | Bool.or lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.Bool.or_congr
+  | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
+  | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
   | BEq.beq α _ lhsExpr rhsExpr =>
     match_expr α with
     | Bool => gateReflection lhsExpr rhsExpr .beq ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr

src/Lean/Elab/Term.lean

@@ -1439,7 +1439,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
     let localDecl? := lctx.decls.findSomeRev? fun localDecl? => do
       let localDecl ← localDecl?
       if localDecl.isAuxDecl then
-        guard (not skipAuxDecl)
+        guard (!skipAuxDecl)
         if let some fullDeclName := auxDeclToFullName.find? localDecl.fvarId then
           matchAuxRecDecl? localDecl fullDeclName givenNameView
         else
@@ -1497,7 +1497,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
       foo := 10
     ```
     -/
-    match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && not projs.isEmpty) with
+    match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && !projs.isEmpty) with
     | some decl => return some (decl.toExpr, projs)
     | none => match n with
       | .str pre s => loop pre (s::projs) globalDeclFoundNext

src/Lean/Meta/Check.lean

@@ -82,7 +82,7 @@ where
         return (a, b)
       else if a.getAppNumArgs != b.getAppNumArgs then
         return (a, b)
-      else if not (← isDefEq a.getAppFn b.getAppFn) then
+      else if !(← isDefEq a.getAppFn b.getAppFn) then
         return (a, b)
       else
         let fType ← inferType a.getAppFn

src/Lean/Meta/DiscrTree.lean

@@ -211,7 +211,7 @@ private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Boo
     if info.isInstImplicit then
       return true
     else if info.isImplicit || info.isStrictImplicit then
-      return not (← isType a)
+      return !(← isType a)
     else
       isProof a
   else

src/Lean/Meta/ExprDefEq.lean

@@ -418,7 +418,7 @@ This method assumes that for any `xs[i]` and `xs[j]` where `i < j`, we have that
 where the index is the position in the local context.
 -/
 private partial def mkLambdaFVarsWithLetDeps (xs : Array Expr) (v : Expr) : MetaM (Option Expr) := do
-  if not (← hasLetDeclsInBetween) then
+  if !(← hasLetDeclsInBetween) then
     mkLambdaFVars xs v (etaReduce := true)
   else
     let ys ← addLetDeps

src/Lean/Meta/LazyDiscrTree.lean

@@ -77,7 +77,7 @@ private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Boo
     if info.isInstImplicit then
       return true
     else if info.isImplicit || info.isStrictImplicit then
-      return not (← isType a)
+      return !(← isType a)
     else
       isProof a
   else

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -137,7 +137,7 @@ def isNonConstFun (motive : Expr) : MetaM Bool := do
   | _ => return motive.hasLooseBVars
 
 def isSimpleHOFun (motive : Expr) : MetaM Bool :=
-  return not (← returnsPi motive) && not (← isNonConstFun motive)
+  return !(← returnsPi motive) && !(← isNonConstFun motive)
 
 def isType2Type (motive : Expr) : MetaM Bool := do
   match ← inferType motive with
@@ -278,7 +278,7 @@ where
   inspectAux (fType mType : Expr) (i : Nat) (args mvars : Array Expr) := do
     let fType ← whnf fType
     let mType ← whnf mType
-    if not (i < args.size) then return ()
+    if !(i < args.size) then return ()
     match fType, mType with
     | Expr.forallE _ fd fb _, Expr.forallE _ _  mb _ => do
       -- TODO: do I need to check (← okBottomUp? args[i] mvars[i] fuel).isSafe here?
@@ -324,7 +324,7 @@ def withKnowing (knowsType knowsLevel : Bool) (x : AnalyzeM α) : AnalyzeM α :=
 builtin_initialize analyzeFailureId : InternalExceptionId ← registerInternalExceptionId `analyzeFailure
 
 def checkKnowsType : AnalyzeM Unit := do
-  if not (← read).knowsType then
+  if !(← read).knowsType then
     throw $ Exception.internal analyzeFailureId
 
 def annotateBoolAt (n : Name) (pos : Pos) : AnalyzeM Unit := do
@@ -425,7 +425,7 @@ mutual
         funBinders   := mkArray args.size false
       }
 
-      if not rest.isEmpty then
+      if !rest.isEmpty then
         -- Note: this shouldn't happen for type-correct terms
         if !args.isEmpty then
           analyzeAppStaged (mkAppN f args) rest
@@ -501,11 +501,11 @@ mutual
     collectHigherOrders := do
       let { args, mvars, bInfos, ..} ← read
       for i in [:args.size] do
-        if not (bInfos[i]! == BinderInfo.implicit || bInfos[i]! == BinderInfo.strictImplicit) then continue
-        if not (← isHigherOrder (← inferType args[i]!)) then continue
+        if !(bInfos[i]! == BinderInfo.implicit || bInfos[i]! == BinderInfo.strictImplicit) then continue
+        if !(← isHigherOrder (← inferType args[i]!)) then continue
         if getPPAnalyzeTrustId (← getOptions) && isIdLike args[i]! then continue
 
-        if getPPAnalyzeTrustKnownFOType2TypeHOFuns (← getOptions) && not (← valUnknown mvars[i]!)
+        if getPPAnalyzeTrustKnownFOType2TypeHOFuns (← getOptions) && !(← valUnknown mvars[i]!)
           && (← isType2Type (args[i]!)) && (← isFOLike (args[i]!)) then continue
 
         tryUnify args[i]! mvars[i]!
@@ -602,7 +602,7 @@ mutual
               | _                 => annotateNamedArg (← mvarName mvars[i]!)
             else annotateBool `pp.analysis.skip; provided := false
             modify fun s => { s with provideds := s.provideds.set! i provided }
-          if (← get).provideds[i]! then withKnowing (not (← typeUnknown mvars[i]!)) true analyze
+          if (← get).provideds[i]! then withKnowing (!(← typeUnknown mvars[i]!)) true analyze
           tryUnify mvars[i]! args[i]!
 
     maybeSetExplicit := do

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

@@ -37,15 +37,11 @@ theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : Ful
 theorem denote_mkFullAdderCarry (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
     ⟦mkFullAdderCarry aig input, assign⟧
       =
-    or
-      (and
-        (xor
+      ((xor
           ⟦aig, input.lhs, assign⟧
-          ⟦aig, input.rhs, assign⟧)
-        ⟦aig, input.cin, assign⟧)
-      (and
-        ⟦aig, input.lhs, assign⟧
-        ⟦aig, input.rhs, assign⟧)
+          ⟦aig, input.rhs, assign⟧) &&
+        ⟦aig, input.cin, assign⟧ ||
+       ⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧)
     := by
   simp only [mkFullAdderCarry, Ref.cast_eq, Int.reduceNeg, denote_mkOrCached,
     LawfulOperator.denote_input_entry, denote_mkAndCached, denote_projected_entry',

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/Clause.lean

@@ -168,7 +168,7 @@ Attempts to add the literal `(idx, b)` to clause `c`. Returns none if doing so w
 tautology.
 -/
 def insert (c : DefaultClause n) (l : Literal (PosFin n)) : Option (DefaultClause n) :=
-  if heq1 : c.clause.contains (l.1, not l.2) then
+  if heq1 : c.clause.contains (l.1, !l.2) then
     none -- Adding l would make c a tautology
   else if heq2 : c.clause.contains l then
     some c
@@ -353,7 +353,7 @@ def reduce_fold_fn (assignments : Array Assignment) (acc : ReduceResult (PosFin
         else
           .reducedToEmpty
       | .neg =>
-        if not l.2 then
+        if !l.2 then
           .reducedToUnit l
         else
           .reducedToEmpty
@@ -367,7 +367,7 @@ def reduce_fold_fn (assignments : Array Assignment) (acc : ReduceResult (PosFin
         else
           .reducedToUnit l'
       | .neg =>
-        if not l.2 then
+        if !l.2 then
           .reducedToNonunit -- Assignment fails to refute both l and l'
         else
           .reducedToUnit l'

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

@@ -219,7 +219,7 @@ def performRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHin
     let (f, derivedLits, derivedEmpty, encounteredError) := performRupCheck f rupHints
     if encounteredError then
       (f, false)
-    else if not derivedEmpty then
+    else if !derivedEmpty then
       (f, false)
     else -- derivedEmpty is true and encounteredError is false
       let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
@@ -284,7 +284,7 @@ def performRatCheck {n : Nat} (f : DefaultFormula n) (negPivot : Literal (PosFin
           -- assignments should now be the same as it was before the performRupCheck call
           let f := clearRatUnits ⟨clauses, rupUnits, ratUnits, assignments⟩
           -- f should now be the same as it was before insertRatUnits
-          if encounteredError || not derivedEmpty then (f, false)
+          if encounteredError || !derivedEmpty then (f, false)
           else (f, true)
     | none => (⟨clauses, rupUnits, ratUnits, assignments⟩, false)
 
@@ -309,7 +309,7 @@ def performRatAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClause n)
           if allChecksPassed then performRatCheck f (Literal.negate pivot) ratHint
           else (f, false)
         let (f, allChecksPassed) := ratHints.foldl fold_fn (f, true)
-        if not allChecksPassed then (f, false)
+        if !allChecksPassed then (f, false)
         else
           match f with
           | ⟨clauses, rupUnits, ratUnits, assignments⟩ =>

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

@@ -507,8 +507,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
                 Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
               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 only [← heq] 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

@@ -57,8 +57,8 @@ theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c
     · simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
     · 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 only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
+        simp_all
       · next hne =>
         exact pv
   · exists v
@@ -67,8 +67,8 @@ theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c
     · simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
     · 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 only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
+        simp_all
       · next hne =>
         exact pv
 

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') = (xor lhs rhs) := by
   simp[*]
 
 theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :