This module contains the BitVec simplifying part of the bv_normalize simp set.

theorem Std.Tactic.BVDecide.Normalize.BitVec.le_ult {w : Nat} (x y : BitVec w) : x ≤ y ↔ (!y.ult x) = true

theorem Std.Tactic.BVDecide.Normalize.BitVec.gt_ult {w : Nat} (x y : BitVec w) : x > y ↔ y.ult x = true

theorem Std.Tactic.BVDecide.Normalize.BitVec.ge_ule {w : Nat} (x y : BitVec w) : x ≥ y ↔ (!x.ult y) = true

theorem Std.Tactic.BVDecide.Normalize.BitVec.slt_eq_ult {w : Nat} (x y : BitVec w) : x.slt y = (!x.getLsbD (w - 1) == y.getLsbD (w - 1) ^^ x.ult y)

theorem Std.Tactic.BVDecide.Normalize.BitVec.sle_eq_ult {w : Nat} (x y : BitVec w) : x.sle y = !(!x.getLsbD (w - 1) == y.getLsbD (w - 1) ^^ y.ult x)

theorem Std.Tactic.BVDecide.Normalize.BitVec.ofNatLT_reduce {w : Nat} (n : Nat) (h : n < 2 ^ w) : n#'h = BitVec.ofNat w n

theorem Std.Tactic.BVDecide.Normalize.BitVec.ofNat_toNat' (w : Nat) (b : Bool) : BitVec.ofNat w b.toNat = BitVec.zeroExtend w (BitVec.ofBool b)

theorem Std.Tactic.BVDecide.Normalize.BitVec.ofBool_eq_ite (b : Bool) : BitVec.ofBool b = bif b then 1#1 else 0#1

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.ofBool_eq_ite (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.BitVec.ofBool_eq_if (b : Bool) : BitVec.ofBool b = bif b then 1#1 else 0#1

theorem Std.Tactic.BVDecide.Normalize.BitVec.sdiv_udiv {w : Nat} (x y : BitVec w) : x.sdiv y = bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -x / -y else -(-x / y) else bif y.getLsbD (w - 1) then -(x / -y) else x / y

theorem Std.Tactic.BVDecide.Normalize.BitVec.smod_umod {w : Nat} (x y : BitVec w) : x.smod y = bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -(-x % -y) else bif -x % y == 0#w then -x % y else y - -x % y else bif y.getLsbD (w - 1) then bif x % -y == 0#w then x % -y else x % -y + y else x.umod y

theorem Std.Tactic.BVDecide.Normalize.BitVec.smtSDiv_smtUDiv {w : Nat} (x y : BitVec w) : x.smtSDiv y = bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then (-x).smtUDiv (-y) else -(-x).smtUDiv y else bif y.getLsbD (w - 1) then -x.smtUDiv (-y) else x.smtUDiv y

theorem Std.Tactic.BVDecide.Normalize.BitVec.srem_umod {w : Nat} (x y : BitVec w) : x.srem y = bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -(-x % -y) else -(-x % y) else bif y.getLsbD (w - 1) then x % -y else x % y

theorem Std.Tactic.BVDecide.Normalize.BitVec.abs_eq {w : Nat} (x : BitVec w) : x.abs = bif x.getLsbD (w - 1) then -x else x

theorem Std.Tactic.BVDecide.Normalize.BitVec.carry_eq_ite_le_lt {w : Nat} (i : Nat) (x y : BitVec w) (c : Bool) : BitVec.carry i x y c = bif c then (~~~BitVec.setWidth i x).ule (BitVec.setWidth i y) else (~~~BitVec.setWidth i x).ult (BitVec.setWidth i y)

theorem Std.Tactic.BVDecide.Normalize.BitVec.getElem_eq_getLsbD {w : Nat} (a : BitVec w) (i : Nat) (h : i < w) : a[i] = a.getLsbD i

theorem Std.Tactic.BVDecide.Normalize.BitVec.ones_and {w : Nat} (a : BitVec w) : -1#w &&& a = a

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_ones {w : Nat} (a : BitVec w) : a &&& -1#w = a

theorem Std.Tactic.BVDecide.Normalize.BitVec.one_plus_not_eq_not_plus_one {w : Nat} (x : BitVec w) : 1#w + ~~~x = ~~~x + 1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_contra {w : Nat} (a : BitVec w) : a &&& ~~~a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_contra' {w : Nat} (a : BitVec w) : ~~~a &&& a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_not {w : Nat} (a : BitVec w) : a + ~~~a = -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_add {w : Nat} (a : BitVec w) : ~~~a + a = -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg {w : Nat} (a : BitVec w) : a + (~~~a + 1#w) = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.neg_add {w : Nat} (a : BitVec w) : ~~~a + 1#w + a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg {w : Nat} (x : BitVec w) : ~~~(~~~x + 1#w) = x + -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg' {w : Nat} (x : BitVec w) : ~~~(x + 1#w) = ~~~x + -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg'' {w : Nat} (x : BitVec w) : ~~~(1#w + x) = ~~~x + -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_same {w : Nat} (a : BitVec w) : a + a = a * 2#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_left {w a b : Nat} {c : BitVec w} : BitVec.ofNat w a + (BitVec.ofNat w b + c) = BitVec.ofNat w a + BitVec.ofNat w b + c

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_right {w a : Nat} {b : BitVec w} {c : Nat} : BitVec.ofNat w a + (b + BitVec.ofNat w c) = BitVec.ofNat w a + BitVec.ofNat w c + b

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_left' {w a : Nat} {b : BitVec w} {c : Nat} : BitVec.ofNat w a + b + BitVec.ofNat w c = BitVec.ofNat w a + BitVec.ofNat w c + b

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_right' {w b c : Nat} {a : BitVec w} : a + BitVec.ofNat w b + BitVec.ofNat w c = BitVec.ofNat w b + BitVec.ofNat w c + a

theorem Std.Tactic.BVDecide.Normalize.BitVec.neg_mul {w : Nat} (x y : BitVec w) : (~~~x + 1#w) * y = ~~~(x * y) + 1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_neg {w : Nat} (x y : BitVec w) : x * (~~~y + 1#w) = ~~~(x * y) + 1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.shiftLeft_zero' {w w' : Nat} (n : BitVec w) : n <<< 0#w' = n

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_shiftLeft' {w w' : Nat} (n : BitVec w) : 0#w' <<< n = 0#w'

theorem Std.Tactic.BVDecide.Normalize.BitVec.shiftLeft_neg {w₁ w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} : (~~~x + 1#w₁) <<< y = ~~~(x <<< y) + 1

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_sshiftRight' {w w' : Nat} (n : BitVec w) : (0#w').sshiftRight' n = 0#w'

theorem Std.Tactic.BVDecide.Normalize.BitVec.ushiftRight_zero' {w w' : Nat} (n : BitVec w) : n >>> 0#w' = n

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_ushiftRight' {w w' : Nat} (n : BitVec w) : 0#w' >>> n = 0#w'

theorem Std.Tactic.BVDecide.Normalize.BitVec.ushiftRight_self {w : Nat} (n : BitVec w) : n >>> n = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_lt_iff_zero_neq {w : Nat} (a : BitVec w) : 0#w < a ↔ a ≠ 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_ult' {w : Nat} (a : BitVec w) : (0#w).ult a = !a == 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.lt_irrefl {n : Nat} (a : BitVec n) : a.ult a = false

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_lt_zero {n : Nat} (a : BitVec n) : a.ult 0#n = false

theorem Std.Tactic.BVDecide.Normalize.BitVec.lt_one_iff {n : Nat} (a : BitVec n) (h : 0 < n) : a.ult 1#n = (a == 0#n)

theorem Std.Tactic.BVDecide.Normalize.BitVec.max_ult' {w : Nat} (a : BitVec w) : (-1#w).ult a = false

theorem Std.Tactic.BVDecide.Normalize.BitVec.ult_max' {w : Nat} (a : BitVec w) : a.ult (-1#w) = !a == -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n k : Nat) (hk : 2 ^ k = n) (hlt : k < w) : x / BitVec.ofNat w n = x >>> k

x / (BitVec.ofNat n) where n = 2^k is the same as shifting x right by k.

theorem Std.Tactic.BVDecide.Normalize.BitVec.extractLsb'_ite {w : Nat} {c : Bool} {x y : BitVec w} (s l : Nat) : BitVec.extractLsb' s l (bif c then x else y) = bif c then BitVec.extractLsb' s l x else BitVec.extractLsb' s l y

theorem Std.Tactic.BVDecide.Normalize.BitVec.extractLsb'_eq_setWidth_ushiftRight {w : Nat} (x : BitVec w) (s l : Nat) : BitVec.extractLsb' s l x = BitVec.setWidth l (x >>> s)

Used in the extractLsb' simproc to reduce extraction at a symbolic offset to a shift.

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.extractLsb'_ite (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.BitVec.extractLsb'_if {w : Nat} {c : Bool} {x y : BitVec w} (s l : Nat) : BitVec.extractLsb' s l (bif c then x else y) = bif c then BitVec.extractLsb' s l x else BitVec.extractLsb' s l y

theorem Std.Tactic.BVDecide.Normalize.BitVec.ones_mul {w : Nat} (a : BitVec w) : -1#w * a = -a

theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_ones {w : Nat} (a : BitVec w) : a * -1#w = -a

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_beq_const {w b c : Nat} {a : BitVec w} : (a + BitVec.ofNat w b == BitVec.ofNat w c) = (a == BitVec.ofNat w c - BitVec.ofNat w b)

theorem Std.Tactic.BVDecide.Normalize.BitVec.const_add_beq_const {w b : Nat} {a : BitVec w} {c : Nat} : (BitVec.ofNat w b + a == BitVec.ofNat w c) = (a == BitVec.ofNat w c - BitVec.ofNat w b)

theorem Std.Tactic.BVDecide.Normalize.BitVec.const_beq_add_const_beq {w c : Nat} {a : BitVec w} {b : Nat} : (BitVec.ofNat w c == a + BitVec.ofNat w b) = (a == BitVec.ofNat w c - BitVec.ofNat w b)

theorem Std.Tactic.BVDecide.Normalize.BitVec.const_beq_const_add_beq {w c b : Nat} {a : BitVec w} : (BitVec.ofNat w c == BitVec.ofNat w b + a) = (a == BitVec.ofNat w c - BitVec.ofNat w b)

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_const_left {w a b : Nat} {c : BitVec w} : BitVec.ofNat w a &&& (BitVec.ofNat w b &&& c) = BitVec.ofNat w a &&& BitVec.ofNat w b &&& c

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_const_right {w a : Nat} {b : BitVec w} {c : Nat} : BitVec.ofNat w a &&& (b &&& BitVec.ofNat w c) = BitVec.ofNat w a &&& BitVec.ofNat w c &&& b

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_const_left' {w a : Nat} {b : BitVec w} {c : Nat} : BitVec.ofNat w a &&& b &&& BitVec.ofNat w c = BitVec.ofNat w a &&& BitVec.ofNat w c &&& b

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_const_right' {w b c : Nat} {a : BitVec w} : a &&& BitVec.ofNat w b &&& BitVec.ofNat w c = BitVec.ofNat w b &&& BitVec.ofNat w c &&& a

theorem Std.Tactic.BVDecide.Normalize.BitVec.append_const_left {w3 w1 a w2 b : Nat} {c : BitVec w3} : BitVec.ofNat w1 a ++ (BitVec.ofNat w2 b ++ c) = BitVec.cast ⋯ (BitVec.ofNat w1 a ++ BitVec.ofNat w2 b ++ c)

theorem Std.Tactic.BVDecide.Normalize.BitVec.append_const_right {w1 w2 b w3 c : Nat} {a : BitVec w1} : a ++ BitVec.ofNat w2 b ++ BitVec.ofNat w3 c = BitVec.cast ⋯ (a ++ (BitVec.ofNat w2 b ++ BitVec.ofNat w3 c))

theorem Std.Tactic.BVDecide.Normalize.BitVec.signExtend_elim {v : Nat} {x : BitVec v} {w : Nat} (h : v ≤ w) : BitVec.signExtend w x = BitVec.cast ⋯ ((bif x.msb then -1#(w - v) else 0#(w - v)) ++ x)

theorem Std.Tactic.BVDecide.Normalize.BitVec.signExtend_elim' {v : Nat} {x : BitVec v} {w : Nat} (h : w ≤ v) : BitVec.signExtend w x = BitVec.extractLsb' 0 w x

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul {w : Nat} {x y : BitVec w} : ~~~(x + x * y) + 1#w = x * ~~~y

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul' {w : Nat} {x y : BitVec w} : ~~~(x + y * x) + 1#w = ~~~y * x

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul'' {w : Nat} {x y : BitVec w} : ~~~(x * y + x) + 1#w = x * ~~~y

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul''' {w : Nat} {x y : BitVec w} : ~~~(y * x + x) + 1#w = ~~~y * x

theorem Std.Tactic.BVDecide.Normalize.BitVec.norm_bv_add_mul {w : Nat} {x y : BitVec w} : ~~~(x * ~~~y) + 1#w = x + x * y

theorem Std.Tactic.BVDecide.Normalize.BitVec.norm_bv_add_mul' {w : Nat} {x y : BitVec w} : ~~~(~~~y * x) + 1#w = x + y * x

theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_beq_mul_short_circuit_left {w : Nat} {x₁ x₂ y : BitVec w} : (x₁ * y == x₂ * y) = !(!x₁ == x₂ && !x₁ * y == x₂ * y)

theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_beq_mul_short_circuit_right {w : Nat} {x y₁ y₂ : BitVec w} : (x * y₁ == x * y₂) = !(!y₁ == y₂ && !x * y₁ == x * y₂)

theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_self_eq_true {w : Nat} (a : BitVec w) : (a == a) = true

theorem Std.Tactic.BVDecide.Normalize.UInt8.toBitVec_cond {c : Bool} {t e : UInt8} : (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.UInt16.toBitVec_cond {c : Bool} {t e : UInt16} : (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.UInt32.toBitVec_cond {c : Bool} {t e : UInt32} : (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.UInt64.toBitVec_cond {c : Bool} {t e : UInt64} : (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.USize.toBitVec_cond {c : Bool} {t e : USize} : (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.Int8.toBitVec_cond {c : Bool} {t e : Int8} : (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.Int16.toBitVec_cond {c : Bool} {t e : Int16} : (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.Int32.toBitVec_cond {c : Bool} {t e : Int32} : (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.Int64.toBitVec_cond {c : Bool} {t e : Int64} : (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.ISize.toBitVec_cond {c : Bool} {t e : ISize} : (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.UInt8.toBitVec_ite {c : Prop} {t e : UInt8} [Decidable c] : (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.UInt16.toBitVec_ite {c : Prop} {t e : UInt16} [Decidable c] : (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.UInt32.toBitVec_ite {c : Prop} {t e : UInt32} [Decidable c] : (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.UInt64.toBitVec_ite {c : Prop} {t e : UInt64} [Decidable c] : (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.USize.toBitVec_ite {c : Prop} {t e : USize} [Decidable c] : (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.Int8.toBitVec_ite {c : Prop} {t e : Int8} [Decidable c] : (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.Int16.toBitVec_ite {c : Prop} {t e : Int16} [Decidable c] : (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.Int32.toBitVec_ite {c : Prop} {t e : Int32} [Decidable c] : (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.Int64.toBitVec_ite {c : Prop} {t e : Int64} [Decidable c] : (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.ISize.toBitVec_ite {c : Prop} {t e : ISize} [Decidable c] : (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec

theorem Std.Tactic.BVDecide.Normalize.UInt8.beq_eq_decide_eq {a b : UInt8} : (a == b) = decide (a = b)

theorem Std.Tactic.BVDecide.Normalize.UInt16.beq_eq_decide_eq {a b : UInt16} : (a == b) = decide (a = b)

theorem Std.Tactic.BVDecide.Normalize.UInt32.beq_eq_decide_eq {a b : UInt32} : (a == b) = decide (a = b)

theorem Std.Tactic.BVDecide.Normalize.UInt64.beq_eq_decide_eq {a b : UInt64} : (a == b) = decide (a = b)

theorem Std.Tactic.BVDecide.Normalize.USize.beq_eq_decide_eq {a b : USize} : (a == b) = decide (a = b)

theorem Std.Tactic.BVDecide.Normalize.Int8.beq_eq_decide_eq {a b : Int8} : (a == b) = decide (a = b)

theorem Std.Tactic.BVDecide.Normalize.Int16.beq_eq_decide_eq {a b : Int16} : (a == b) = decide (a = b)

theorem Std.Tactic.BVDecide.Normalize.Int32.beq_eq_decide_eq {a b : Int32} : (a == b) = decide (a = b)

theorem Std.Tactic.BVDecide.Normalize.Int64.beq_eq_decide_eq {a b : Int64} : (a == b) = decide (a = b)

theorem Std.Tactic.BVDecide.Normalize.ISize.beq_eq_decide_eq {a b : ISize} : (a == b) = decide (a = b)