fix: Std.BitVec occurrences at OmegaM.lean

Motivation: `Nat`, `Int`, `Fin`, `UInt??` are already in the top level
namespace. We will eventually define `UInt??` and `Int??` using `BitVec`.

src/Init/Data/BitVec/Basic.lean

@@ -8,8 +8,6 @@ import Init.Data.Fin.Basic
 import Init.Data.Nat.Bitwise.Lemmas
 import Init.Data.Nat.Power2
 
-namespace Std
-
 /-!
 We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
 (Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
@@ -35,6 +33,8 @@ structure BitVec (w : Nat) where
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
 
+@[deprecated] abbrev Std.BitVec := _root_.BitVec
+
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
 -- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
@@ -166,7 +166,7 @@ protected def toHex {n : Nat} (x : BitVec n) : String :=
   let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
   t ++ s
 
-instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Format) ++ "#" ++ repr n
+instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
 instance : ToString (BitVec n) where toString a := toString (repr a)
 
 end repr_toString
@@ -606,3 +606,5 @@ section normalization_eqs
 @[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
 @[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
 end normalization_eqs
+
+end BitVec

src/Init/Data/BitVec/Bitblast.lean

@@ -45,7 +45,7 @@ end Bool
 
 /-! ### Preliminaries -/
 
-namespace Std.BitVec
+namespace BitVec
 
 private theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
     testBit x i = decide (x ≥ 2^i) := by
@@ -173,3 +173,5 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
 /-- Subtracting `x` from the all ones bitvector is equivalent to taking its complement -/
 theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
   rw [← add_not_self x, BitVec.add_comm, add_sub_cancel]
+
+end BitVec

src/Init/Data/BitVec/Folds.lean

@@ -8,7 +8,7 @@ import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Fin.Iterate
 
-namespace Std.BitVec
+namespace BitVec
 
 /--
 iunfoldr is an iterative operation that applies a function `f` repeatedly.
@@ -57,3 +57,5 @@ theorem iunfoldr_replace
     (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
     iunfoldr f a = (state w, value) := by
   simp [iunfoldr.eq_test state value a init step]
+
+end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -9,7 +9,7 @@ import Init.Data.BitVec.Basic
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
 
-namespace Std.BitVec
+namespace BitVec
 
 /--
 This normalized a bitvec using `ofFin` to `ofNat`.
@@ -598,3 +598,5 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   let ⟨y, lt⟩ := y
   simp
   exact Nat.lt_of_le_of_ne
+
+end BitVec

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -7,6 +7,7 @@ prelude
 import Init.Omega.LinearCombo
 import Init.Omega.Int
 import Init.Omega.Logic
+import Init.Data.BitVec
 import Lean.Meta.AppBuilder
 
 /-!
@@ -173,8 +174,8 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
         r := r.insert (mkApp (.const ``Int.neg_le_natAbs []) x)
       | _, (``Fin.val, #[n, i]) =>
         r := r.insert (mkApp2 (.const ``Fin.isLt []) n i)
-      | _, (`Std.BitVec.toNat, #[n, x]) =>
-        r := r.insert (mkApp2 (.const `Std.BitVec.toNat_lt []) n x)
+      | _, (``BitVec.toNat, #[n, x]) =>
+        r := r.insert (mkApp2 (.const ``BitVec.toNat_lt []) n x)
       | _, _ => pure ()
     return r
   | (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -8,7 +8,7 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Init.Data.BitVec.Basic
 
-namespace Std.BitVec
+namespace BitVec
 open Lean Meta Simp
 
 /-- A bit-vector literal -/
@@ -30,16 +30,16 @@ private def fromOfNatExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
   return { n, value := BitVec.ofNat n v }
 
 /--
-Try to convert an `Std.BitVec.ofNat`-application into a bitvector literal.
+Try to convert an `BitVec.ofNat`-application into a bitvector literal.
 -/
 private def fromBitVecExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
-  guard (e.isAppOfArity ``Std.BitVec.ofNat 2)
+  guard (e.isAppOfArity ``BitVec.ofNat 2)
   let n ← Nat.fromExpr? e.appFn!.appArg!
   let v ← Nat.fromExpr? e.appArg!
   return { n, value := BitVec.ofNat n v }
 
 /--
-Try to convert `OfNat.ofNat`/`Std.BitVec.OfNat` application into a
+Try to convert `OfNat.ofNat`/`BitVec.OfNat` application into a
 bitvector literal.
 -/
 def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
@@ -48,9 +48,9 @@ def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
 /--
 Convert a bitvector literal into an expression.
 -/
--- Using `Std.BitVec.ofNat` because it is being used in `simp` theorems
+-- Using `BitVec.ofNat` because it is being used in `simp` theorems
 def Literal.toExpr (lit : Literal) : Expr :=
-  mkApp2 (mkConst ``Std.BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
+  mkApp2 (mkConst ``BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
 
 /--
 Helper function for reducing homogenous unary bitvector operators.
@@ -305,4 +305,4 @@ builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
   let lit : Literal := { n, value := allOnes n }
   return .done { expr := lit.toExpr }
 
-end Std.BitVec
+end BitVec

tests/lean/binop_at_pattern_issue.lean

@@ -1,5 +1,5 @@
-open Std BitVec
-def f4 (v : Std.BitVec 32) : Nat :=
+open BitVec
+def f4 (v : BitVec 32) : Nat :=
   match v with
   | 10#20 ++ 0#12  => 0 -- Should be rejected since `++` does not have `[match_pattern]`
   | _ => 1

tests/lean/run/bitvec_fin_literal_norm.lean

@@ -1,4 +1,4 @@
-open Std BitVec
+open BitVec
 
 example : (5 : Fin 4) = x := by
   simp

tests/lean/run/bitvec_simproc.lean

@@ -3,45 +3,45 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-open Std BitVec
+open BitVec
 
-example (h : x = (6 : Std.BitVec 3)) : x = -2 := by
+example (h : x = (6 : BitVec 3)) : x = -2 := by
   simp; guard_target =ₛ x = 6#3; assumption
-example (h : x = (5 : Std.BitVec 3)) : x = ~~~2 := by
+example (h : x = (5 : BitVec 3)) : x = ~~~2 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = BitVec.abs (-1#32) := by
+example (h : x = (1 : BitVec 32)) : x = BitVec.abs (-1#32) := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (5 : Std.BitVec 3)) : x = 2 + 3 := by
+example (h : x = (5 : BitVec 3)) : x = 2 + 3 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (1 : Std.BitVec 3)) : x = 5 &&& 3 := by
+example (h : x = (1 : BitVec 3)) : x = 5 &&& 3 := by
   simp; guard_target =ₛ x = 1#3; assumption
-example (h : x = (7 : Std.BitVec 3)) : x = 5 ||| 3 := by
+example (h : x = (7 : BitVec 3)) : x = 5 ||| 3 := by
   simp; guard_target =ₛ x = 7#3; assumption
-example (h : x = (6 : Std.BitVec 3)) : x = 5 ^^^ 3 := by
+example (h : x = (6 : BitVec 3)) : x = 5 ^^^ 3 := by
   simp; guard_target =ₛ x = 6#3; assumption
-example (h : x = (3 : Std.BitVec 32)) : x = 5 - 2 := by
+example (h : x = (3 : BitVec 32)) : x = 5 - 2 := by
   simp; guard_target =ₛ x = 3#32; assumption
-example (h : x = (10 : Std.BitVec 32)) : x = 5 * 2 := by
+example (h : x = (10 : BitVec 32)) : x = 5 * 2 := by
   simp; guard_target =ₛ x = 10#32; assumption
-example (h : x = (4 : Std.BitVec 32)) : x = 9 / 2 := by
+example (h : x = (4 : BitVec 32)) : x = 9 / 2 := by
   simp; guard_target =ₛ x = 4#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = 9 % 2 := by
+example (h : x = (1 : BitVec 32)) : x = 9 % 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (4 : Std.BitVec 32)) : x = udiv 9 2 := by
+example (h : x = (4 : BitVec 32)) : x = udiv 9 2 := by
   simp; guard_target =ₛ x = 4#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = umod 9 2 := by
+example (h : x = (1 : BitVec 32)) : x = umod 9 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (4 : Std.BitVec 32)) : x = sdiv (-9) (-2) := by
+example (h : x = (4 : BitVec 32)) : x = sdiv (-9) (-2) := by
   simp; guard_target =ₛ x = 4#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = smod (-9) 2 := by
+example (h : x = (1 : BitVec 32)) : x = smod (-9) 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = - smtUDiv 9 0 := by
+example (h : x = (1 : BitVec 32)) : x = - smtUDiv 9 0 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = - srem (-9) 2 := by
+example (h : x = (1 : BitVec 32)) : x = - srem (-9) 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = - smtSDiv 9 0 := by
+example (h : x = (1 : BitVec 32)) : x = - smtSDiv 9 0 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = smtSDiv (-9) 0 := by
+example (h : x = (1 : BitVec 32)) : x = smtSDiv (-9) 0 := by
   simp; guard_target =ₛ x = 1#32; assumption
 example (h : x = false) : x = (4#3).getLsb 0:= by
   simp; guard_target =ₛ x = false; assumption
@@ -51,29 +51,29 @@ example (h : x = true) : x = (4#3).getMsb 0:= by
   simp; guard_target =ₛ x = true; assumption
 example (h : x = false) : x = (4#3).getMsb 2:= by
   simp; guard_target =ₛ x = false; assumption
-example (h : x = (24 : Std.BitVec 32)) : x = 6#32 <<< 2 := by
+example (h : x = (24 : BitVec 32)) : x = 6#32 <<< 2 := by
   simp; guard_target =ₛ x = 24#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = 6#32 >>> 2 := by
+example (h : x = (1 : BitVec 32)) : x = 6#32 >>> 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (24 : Std.BitVec 32)) : x = BitVec.shiftLeft 6#32 2 := by
+example (h : x = (24 : BitVec 32)) : x = BitVec.shiftLeft 6#32 2 := by
   simp; guard_target =ₛ x = 24#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = BitVec.ushiftRight 6#32 2 := by
+example (h : x = (1 : BitVec 32)) : x = BitVec.ushiftRight 6#32 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (2 : Std.BitVec 32)) : x = - BitVec.sshiftRight (- 6#32) 2 := by
+example (h : x = (2 : BitVec 32)) : x = - BitVec.sshiftRight (- 6#32) 2 := by
   simp; guard_target =ₛ x = 2#32; assumption
-example (h : x = (5 : Std.BitVec 3)) : x = BitVec.rotateLeft (6#3) 1 := by
+example (h : x = (5 : BitVec 3)) : x = BitVec.rotateLeft (6#3) 1 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (3 : Std.BitVec 3)) : x = BitVec.rotateRight (6#3) 1 := by
+example (h : x = (3 : BitVec 3)) : x = BitVec.rotateRight (6#3) 1 := by
   simp; guard_target =ₛ x = 3#3; assumption
-example (h : x = (7 : Std.BitVec 5)) : x = 1#3 ++ 3#2 := by
+example (h : x = (7 : BitVec 5)) : x = 1#3 ++ 3#2 := by
   simp; guard_target =ₛ x = 7#5; assumption
-example (h : x = (1 : Std.BitVec 3)) : x = BitVec.cast (by decide : 3=2+1) 1#3 := by
+example (h : x = (1 : BitVec 3)) : x = BitVec.cast (by decide : 3=2+1) 1#3 := by
   simp; guard_target =ₛ x = 1#3; assumption
 example (h : x = 5) : x = (2#3 + 3#3).toNat := by
   simp; guard_target =ₛ x = 5; assumption
 example (h : x = -1) : x = (2#3 - 3#3).toInt := by
   simp; guard_target =ₛ x = -1; assumption
-example (h : x = (1 : Std.BitVec 3)) : x = -BitVec.ofInt 3 (-1) := by
+example (h : x = (1 : BitVec 3)) : x = -BitVec.ofInt 3 (-1) := by
   simp; guard_target =ₛ x = 1#3; assumption
 example (h : x) : x = (1#3 < 3#3) := by
   simp; guard_target =ₛ x; assumption
@@ -99,15 +99,15 @@ example (h : x) : x = (3#3 ≥ 1#3) := by
   simp; guard_target =ₛ x; assumption
 example (h : ¬x) : x = (3#3 ≥ 4#3) := by
   simp; guard_target =ₛ ¬x; assumption
-example (h : x = (5 : Std.BitVec 7)) : x = (5#3).zeroExtend' (by decide) := by
+example (h : x = (5 : BitVec 7)) : x = (5#3).zeroExtend' (by decide) := by
   simp; guard_target =ₛ x = 5#7; assumption
-example (h : x = (80 : Std.BitVec 7)) : x = (5#3).shiftLeftZeroExtend 4 := by
+example (h : x = (80 : BitVec 7)) : x = (5#3).shiftLeftZeroExtend 4 := by
   simp; guard_target =ₛ x = 80#7; assumption
-example (h : x = (5: Std.BitVec 3)) : x = (10#5).extractLsb' 1 3 := by
+example (h : x = (5: BitVec 3)) : x = (10#5).extractLsb' 1 3 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (9: Std.BitVec 6)) : x = (1#3).replicate 2 := by
+example (h : x = (9: BitVec 6)) : x = (1#3).replicate 2 := by
   simp; guard_target =ₛ x = 9#6; assumption
-example (h : x = (5 : Std.BitVec 7)) : x = (5#3).zeroExtend 7 := by
+example (h : x = (5 : BitVec 7)) : x = (5#3).zeroExtend 7 := by
   simp; guard_target =ₛ x = 5#7; assumption
 example (h : -5#10 = x) : signExtend 10 (-5#8) = x := by
   simp; guard_target =ₛ1019#10 = x; assumption

tests/lean/run/omega.lean

@@ -1,4 +1,3 @@
-
 example : True := by
   fail_if_success omega
   trivial
@@ -428,7 +427,7 @@ example : 2^7 < 165 := by omega
 example (_ : x % 2^7 < 3) : x % 128 < 5 := by omega
 
 /-! ### BitVec -/
-open Std BitVec
+open BitVec
 
 example (x y : BitVec 8) (_ : x < y) : x ≠ y := by
   bv_omega