chore: cleanup in BitVec/Bitblast

src/Init/Data/BitVec/Bitblast.lean

@@ -29,6 +29,20 @@ https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.
 
 open Nat Bool
 
+namespace Bool
+
+/-- At least two out of three booleans are true. -/
+abbrev atLeastTwo (a b c : Bool) : Bool := a && b || a && c || b && c
+
+@[simp] theorem atLeastTwo_false_left  : atLeastTwo false b c = (b && c) := by simp [atLeastTwo]
+@[simp] theorem atLeastTwo_false_mid   : atLeastTwo a false c = (a && c) := by simp [atLeastTwo]
+@[simp] theorem atLeastTwo_false_right : atLeastTwo a b false = (a && b) := by simp [atLeastTwo]
+@[simp] theorem atLeastTwo_true_left   : atLeastTwo true b c  = (b || c) := by cases b <;> cases c <;> simp [atLeastTwo]
+@[simp] theorem atLeastTwo_true_mid    : atLeastTwo a true c  = (a || c) := by cases a <;> cases c <;> simp [atLeastTwo]
+@[simp] theorem atLeastTwo_true_right  : atLeastTwo a b true  = (a || b) := by cases a <;> cases b <;> simp [atLeastTwo]
+
+end Bool
+
 /-! ### Preliminaries -/
 
 namespace Std.BitVec
@@ -75,7 +89,11 @@ private theorem mod_two_pow_succ (x i : Nat) :
     have not_j_ge_i : ¬(j ≥ i) := Nat.not_le_of_lt j_lt_i
     simp [j_lt_i, j_le_i, not_j_ge_i, j_le_i_succ]
 
-private theorem mod_two_pow_lt (x i : Nat) : x % 2 ^ i < 2^i := Nat.mod_lt _ (Nat.two_pow_pos _)
+private theorem mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ
+     (x y i : Nat) (c : Bool) : x % 2^i + (y % 2^i + c.toNat) < 2^(i+1) := by
+  have : c.toNat ≤ 1 := Bool.toNat_le_one c
+  rw [Nat.pow_succ]
+  omega
 
 /-! ### Addition -/
 
@@ -86,8 +104,14 @@ def carry (i : Nat) (x y : BitVec w) (c : Bool) : Bool :=
 @[simp] theorem carry_zero : carry 0 x y c = c := by
   cases c <;> simp [carry, mod_one]
 
-/-- At least two out of three booleans are true. -/
-abbrev atLeastTwo (a b c : Bool) : Bool := a && b || a && c || b && c
+theorem carry_succ (i : Nat) (x y : BitVec w) (c : Bool) :
+    carry (i+1) x y c = atLeastTwo (x.getLsb i) (y.getLsb i) (carry i x y c) := by
+  simp only [carry, mod_two_pow_succ, atLeastTwo, getLsb]
+  simp only [Nat.pow_succ']
+  have sum_bnd : x.toNat%2^i + (y.toNat%2^i + c.toNat) < 2*2^i := by
+    simp only [← Nat.pow_succ']
+    exact mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ ..
+  cases x.toNat.testBit i <;> cases y.toNat.testBit i <;> (simp; omega)
 
 /-- Carry function for bitwise addition. -/
 def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xor y c))
@@ -96,20 +120,6 @@ def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xo
 def adc (x y : BitVec w) : Bool → Bool × BitVec w :=
   iunfoldr fun (i : Fin w) c => adcb (x.getLsb i) (y.getLsb i) c
 
-theorem adc_overflow_limit (x y i : Nat) (c : Bool) : x % 2^i + (y % 2^i + c.toNat) < 2^(i+1) := by
-  have : c.toNat ≤ 1 := Bool.toNat_le_one c
-  rw [Nat.pow_succ]
-  omega
-
-theorem carry_succ (i : Nat) (x y : BitVec w) (c : Bool) :
-    carry (i+1) x y c = atLeastTwo (x.getLsb i) (y.getLsb i) (carry i x y c) := by
-  simp only [carry, mod_two_pow_succ, atLeastTwo, getLsb]
-  simp only [Nat.pow_succ']
-  have sum_bnd : x.toNat%2^i + (y.toNat%2^i + c.toNat) < 2*2^i := by
-    simp only [← Nat.pow_succ']
-    exact adc_overflow_limit ..
-  cases x.toNat.testBit i <;> cases y.toNat.testBit i <;> (simp; omega)
-
 theorem getLsb_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
     getLsb (x + y + zeroExtend w (ofBool c)) i =
       Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x y c)) := by
@@ -127,7 +137,7 @@ theorem getLsb_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool)
       Bool.true_and,
       Nat.add_assoc,
       Nat.add_left_comm (_%_) (_ * _) _,
-      testBit_limit (adc_overflow_limit x y i c)
+      testBit_limit (mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ x y i c)
     ]
   simp [testBit_to_div_mod, carry, Nat.add_assoc]
 

src/Init/Data/BitVec/Lemmas.lean

@@ -81,6 +81,8 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
     have q := pred ⟨w - 1 - i, q_lt⟩
     simpa [q_lt, Nat.sub_sub_self, r] using q
 
+@[simp] theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
+
 theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
@@ -110,7 +112,9 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
   getLsb (x#n) i = (i < n && x.testBit i) := by
   simp [getLsb, BitVec.ofNat, Fin.val_ofNat']
 
-@[deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
+@[simp, deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
+
+@[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb]
 
 @[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
   Nat.mod_eq_of_lt x.isLt
@@ -120,6 +124,8 @@ private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) :
 
 /-! ### msb -/
 
+@[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsb]
+
 theorem msb_eq_getLsb_last (x : BitVec w) :
     x.msb = x.getLsb (w - 1) := by
   simp [BitVec.msb, getMsb, getLsb]
@@ -127,7 +133,7 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
   · simp [BitVec.eq_nil x]
   · simp
 
-@[simp] theorem getLsb_last (x : BitVec (w + 1)) :
+@[bv_toNat] theorem getLsb_last (x : BitVec (w + 1)) :
     x.getLsb w = decide (2 ^ w ≤ x.toNat) := by
   simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
     Nat.sub_zero, Nat.and_one_is_mod, Bool.true_and, Nat.shiftRight_eq_div_pow]
@@ -139,9 +145,8 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
     · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
       omega
 
-@[simp]
-theorem msb_eq_decide (x : BitVec (w + 1)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by
-  simp [msb_eq_getLsb_last]
+@[bv_toNat] theorem msb_eq_decide (x : BitVec (w + 1)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by
+  simp [msb_eq_getLsb_last, getLsb_last]
 
 /-! ### cast -/
 
@@ -205,6 +210,23 @@ theorem msb_eq_decide (x : BitVec (w + 1)) : BitVec.msb x = decide (2 ^ w ≤ x.
     getLsb (truncate m x) i = (decide (i < m) && getLsb x i) :=
   getLsb_zeroExtend m x i
 
+@[simp] theorem zeroExtend_zeroExtend_of_le (x : BitVec w) (h : k ≤ l) :
+    (x.zeroExtend l).zeroExtend k = x.zeroExtend k := by
+  ext i
+  simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and]
+  have p := lt_of_getLsb x i
+  revert p
+  cases getLsb x i <;> simp; omega
+
+@[simp] theorem truncate_truncate_of_le (x : BitVec w) (h : k ≤ l) :
+    (x.truncate l).truncate k = x.truncate k :=
+  zeroExtend_zeroExtend_of_le x h
+
+theorem msb_zeroExtend (x : BitVec w) : (x.zeroExtend v).msb = (decide (0 < v) && x.getLsb (v - 1)) := by
+  rw [msb_eq_getLsb_last]
+  simp only [getLsb_zeroExtend]
+  cases getLsb x (v - 1) <;> simp; omega
+
 /-! ## extractLsb -/
 
 @[simp]