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.truncate_eq_zeroExtend {w n : Nat} (x : BitVec w) : BitVec.truncate n x = BitVec.zeroExtend n x

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.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.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 : Nat} (a b c : BitVec w) : a + (b + c) = a + b + c

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

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

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_right' {w : Nat} (a b c : BitVec w) : a + b + c = b + 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.ushiftRight_zero' {w w' : Nat} (n : BitVec w) : n >>> 0#w' = n

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.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.exctractLsb'_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