feat: lemmas for BitVec (leanprover-community#558)

Co-authored-by: Joe Hendrix <[email protected]>

Std/Data/BitVec/Basic.lean

@@ -334,7 +334,13 @@ As a numeric operation, this is equivalent to `a / 2^s`, rounding down.
 
 SMT-Lib name: `bvlshr` except this operator uses a `Nat` shift value.
 -/
-def ushiftRight (a : BitVec n) (s : Nat) : BitVec n := .ofNat n (a.toNat >>> s)
+def ushiftRight (a : BitVec n) (s : Nat) : BitVec n :=
+  ⟨a.toNat >>> s, by
+  let ⟨a, lt⟩ := a
+  simp only [BitVec.toNat, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul (Nat.pow_two_pos s)]
+  rw [←Nat.mul_one a]
+  exact Nat.mul_lt_mul_of_lt_of_le' lt (Nat.pow_two_pos s) (Nat.le_refl 1)⟩
+
 instance : HShiftRight (BitVec w) Nat (BitVec w) := ⟨.ushiftRight⟩
 
 /--

Std/Data/BitVec/Lemmas.lean

@@ -1,27 +1,47 @@
 import Std.Data.Bool
 import Std.Data.BitVec.Basic
+import Std.Data.Fin.Lemmas
 import Std.Data.Nat.Lemmas
 
+import Std.Tactic.Ext
 import Std.Tactic.Simpa
+import Std.Tactic.Omega
 
 namespace Std.BitVec
 
 /-- Prove equality of bitvectors in terms of nat operations. -/
 theorem eq_of_toNat_eq {n} : ∀ {i j : BitVec n}, i.toNat = j.toNat → i = j
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
+theorem zero_is_unique (x : BitVec 0) : x = 0#0 := by
+  let ⟨i, lt⟩ := x
+  have p : i < 1 := lt
+  have q : i = 0 := by omega
+  simp [q]
+  rfl
+
+@[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
+
 theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat :=
   Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq
 
+theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.toFin.2
+
 theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
 
+@[simp] theorem getLsb_ofFin (x : Fin (2^n)) (i : Nat) :
+  getLsb (BitVec.ofFin x) i = x.val.testBit i := rfl
+
 @[simp] theorem getLsb_ge (x : BitVec w) (i : Nat) (ge : i ≥ w) : getLsb x i = false := by
   let ⟨x, x_lt⟩ := x
+  simp
   apply Nat.testBit_lt_two
-  apply Nat.lt_of_lt_of_le x_lt
-  apply Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) ge
+  have p : 2^w ≤ 2^i := Nat.pow_le_pow_of_le_right (by omega) ge
+  omega
 
-theorem eq_of_getLsb_eq {x y : BitVec w}
+-- We choose `eq_of_getLsb_eq` as the `@[ext]` theorem for `BitVec`
+-- somewhat arbitrarily over `eq_of_getMsg_eq`.
+@[ext] theorem eq_of_getLsb_eq {x y : BitVec w}
     (pred : ∀(i : Fin w), x.getLsb i.val = y.getLsb i.val) : x = y := by
   apply eq_of_toNat_eq
   apply Nat.eq_of_testBit_eq
@@ -56,15 +76,22 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
 
 @[simp] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
 
-theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w := by
+@[simp] theorem toNat_ofNat (x w : Nat) : (x#w).toNat = x % 2^w := by
   simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
 
-@[simp] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
+@[simp] 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] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
+  Nat.mod_eq_of_lt x.isLt
 
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
   Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
 
-@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : (BitVec.ofNat m x.toNat) = truncate m x := by
+@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : x.toNat#m = truncate m x := by
   let ⟨x, lt_n⟩ := x
   unfold truncate
   unfold zeroExtend
@@ -75,31 +102,13 @@ private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) :
   else
     simp [h]
 
-theorem toNat_append (x : BitVec m) (y : BitVec n) : (x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
-  rfl
+/-! ### cast -/
 
 @[simp] theorem toNat_cast (e : m = n) (x : BitVec m) : (cast e x).toNat = x.toNat := rfl
 
-theorem toNat_cons (b : Bool) (x : BitVec w) : (cons b x).toNat = (b.toNat <<< w) ||| x.toNat := by
-  let ⟨x, _⟩ := x
-  simp [cons, toNat_append, toNat_ofBool]
-
-/-! ### cons -/
-
-theorem getLsb_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
-    getLsb (cons b x) i = if i = n then b else getLsb x i := by
-  simp only [getLsb, toNat_cons, Nat.testBit_or]
-  rw [Nat.testBit_shiftLeft]
-  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
-  · have i_ge_n := Nat.not_le_of_gt i_lt_n
-    have not_eq := Nat.ne_of_lt i_lt_n
-    simp [i_ge_n, not_eq]
-  · simp [i_eq_n, testBit_toNat]
-    cases b <;> trivial
-  · have i_ge_n : n ≤ i := Nat.le_of_lt n_lt_i
-    have not_eq := Nat.ne_of_gt n_lt_i
-    have neq_zero : i - n ≠ 0 := Nat.sub_ne_zero_of_lt n_lt_i
-    simp [i_ge_n, not_eq, Nat.testBit_bool_to_nat, neq_zero]
+@[simp] theorem getLsb_cast : (cast h v).getLsb i = v.getLsb i := by
+  cases h
+  simp
 
 /-! ### zeroExtend and truncate -/
 
@@ -132,18 +141,131 @@ theorem toNat_zeroExtend (i : Nat) (x : BitVec n) :
 @[simp] theorem toNat_truncate (x : BitVec n) : (truncate i x).toNat = x.toNat % 2^i :=
   toNat_zeroExtend i x
 
-theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+@[simp] theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend' ge x) i = getLsb x i := by
   simp [getLsb, toNat_zeroExtend']
 
-theorem getLsb_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
+@[simp] theorem getLsb_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend m x) i = (decide (i < m) && getLsb x i) := by
   simp [getLsb, toNat_zeroExtend, Nat.testBit_mod_two_pow]
 
-theorem getLsb_truncate (m : Nat) (x : BitVec n) (i : Nat) :
+@[simp] theorem getLsb_truncate (m : Nat) (x : BitVec n) (i : Nat) :
     getLsb (truncate m x) i = (decide (i < m) && getLsb x i) :=
   getLsb_zeroExtend m x i
 
+/-! ## extractLsb -/
+
+@[simp]
+protected theorem extractLsb_ofFin {n} (x : Fin (2^n)) (hi lo : Nat) :
+  extractLsb hi lo (@BitVec.ofFin n x) = .ofNat (hi-lo+1) (x.val >>> lo) := rfl
+
+@[simp]
+protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
+  extractLsb hi lo x#n = .ofNat (hi - lo + 1) ((x % 2^n) >>> lo) := by
+  apply eq_of_getLsb_eq
+  intro ⟨i, _lt⟩
+  simp [BitVec.ofNat]
+
+@[simp] theorem extractLsb'_toNat (s m : Nat) (x : BitVec n) :
+  (extractLsb' s m x).toNat = (x.toNat >>> s) % 2^m := rfl
+
+@[simp] theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) :
+  (extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl
+
+@[simp] theorem getLsb_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
+    getLsb (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsb x (lo+i)) := by
+  unfold getLsb
+  simp [Nat.lt_succ]
+
+/-! ### or -/
+
+@[simp] theorem toNat_or {x y : BitVec v} :
+    BitVec.toNat (x ||| y) = BitVec.toNat x ||| BitVec.toNat y := rfl
+
+@[simp] theorem getLsb_or {x y : BitVec v} : (x ||| y).getLsb i = (x.getLsb i || y.getLsb i) := by
+  rw [← testBit_toNat, getLsb, getLsb]
+  simp
+
+/-! ### shiftLeft -/
+
+@[simp] theorem toNat_shiftLeft {x : BitVec v} :
+    BitVec.toNat (x <<< n) = BitVec.toNat x <<< n % 2^v :=
+  BitVec.toNat_ofNat _ _
+
+@[simp] theorem getLsb_shiftLeft (x : BitVec m) (n) :
+    getLsb (x <<< n) i = (decide (i < m) && !decide (i < n) && getLsb x (i - n)) := by
+  rw [← testBit_toNat, getLsb]
+  simp only [toNat_shiftLeft, Nat.testBit_mod_two_pow, Nat.testBit_shiftLeft, ge_iff_le]
+  -- This step could be a case bashing tactic.
+  cases h₁ : decide (i < m) <;> cases h₂ : decide (n ≤ i) <;> cases h₃ : decide (i < n)
+  all_goals { simp_all <;> omega }
+
+theorem shiftLeftZeroExtend_eq {x : BitVec w} :
+    shiftLeftZeroExtend x n = zeroExtend (w+n) x <<< n := by
+  apply eq_of_toNat_eq
+  rw [shiftLeftZeroExtend, zeroExtend]
+  split
+  · simp
+    rw [Nat.mod_eq_of_lt]
+    rw [Nat.shiftLeft_eq, Nat.pow_add]
+    exact Nat.mul_lt_mul_of_pos_right (BitVec.toNat_lt x) (Nat.pow_two_pos _)
+  · omega
+
+@[simp] theorem getLsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
+    getLsb (shiftLeftZeroExtend x n) i = ((! decide (i < n)) && getLsb x (i - n)) := by
+  rw [shiftLeftZeroExtend_eq]
+  simp only [getLsb_shiftLeft, getLsb_zeroExtend]
+  cases h₁ : decide (i < n) <;> cases h₂ : decide (i - n < m + n) <;> cases h₃ : decide (i < m + n)
+    <;> simp_all
+    <;> (rw [getLsb_ge]; omega)
+
+/-! ### ushiftRight -/
+
+@[simp] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
+    (x >>> i).toNat = x.toNat >>> i := rfl
+
+@[simp] theorem getLsb_ushiftRight (x : BitVec n) (i j : Nat) :
+    getLsb (x >>> i) j = getLsb x (i+j) := by
+  unfold getLsb ; simp
+
+/-! ### append -/
+
+theorem append_def (x : BitVec v) (y : BitVec w) :
+    x ++ y = (shiftLeftZeroExtend x w ||| zeroExtend' (Nat.le_add_left w v) y) := rfl
+
+@[simp] theorem toNat_append (x : BitVec m) (y : BitVec n) :
+    (x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
+  rfl
+
+@[simp] theorem getLsb_append {v : BitVec n} {w : BitVec m} :
+    getLsb (v ++ w) i = bif i < m then getLsb w i else getLsb v (i - m) := by
+  simp [append_def]
+  by_cases h : i < m
+  · simp [h]
+  · simp [h]; simp_all
+
+/-! ### cons -/
+
+@[simp] theorem toNat_cons (b : Bool) (x : BitVec w) :
+    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat := by
+  let ⟨x, _⟩ := x
+  simp [cons, toNat_append, toNat_ofBool]
+
+@[simp] theorem getLsb_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
+    getLsb (cons b x) i = if i = n then b else getLsb x i := by
+  simp only [getLsb, toNat_cons, Nat.testBit_or]
+  rw [Nat.testBit_shiftLeft]
+  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
+  · have p1 : ¬(n ≤ i) := by omega
+    have p2 : i ≠ n := by omega
+    simp [p1, p2]
+  · simp [i_eq_n, testBit_toNat]
+    cases b <;> trivial
+  · have p1 : n ≤ i := by omega
+    have p2 : i ≠ n := by omega
+    have p3 : i - n ≠ 0 := by omega
+    simp [p1, p2, p3, Nat.testBit_bool_to_nat]
+
 theorem truncate_succ (x : BitVec w) :
     truncate (i+1) x = cons (getLsb x i) (truncate i x) := by
   apply eq_of_getLsb_eq
@@ -157,11 +279,87 @@ theorem truncate_succ (x : BitVec w) :
 
 /-! ### add -/
 
+theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl
+
 /--
 Definition of bitvector addition as a nat.
 -/
-theorem toNat_add (x y : BitVec w) : (x + y).toNat = (x.toNat + y.toNat) % 2^w := by rfl
+@[simp] theorem toNat_add (x y : BitVec w) : (x + y).toNat = (x.toNat + y.toNat) % 2^w := rfl
+@[simp] theorem ofFin_add (x : Fin (2^n)) (y : BitVec n) :
+  .ofFin x + y = .ofFin (x + y.toFin) := rfl
+@[simp] theorem add_ofFin (x : BitVec n) (y : Fin (2^n)) :
+  x + .ofFin y = .ofFin (x.toFin + y) := rfl
+@[simp] theorem ofNat_add_ofNat {n} (x y : Nat) : x#n + y#n = (x + y)#n := by
+  apply eq_of_toNat_eq ; simp [BitVec.ofNat]
+
+protected theorem add_assoc (x y z : BitVec n) : x + y + z = x + (y + z) := by
+  apply eq_of_toNat_eq ; simp [Nat.add_assoc]
+
+protected theorem add_comm (x y : BitVec n) : x + y = y + x := by
+  simp [add_def, Nat.add_comm]
+
+@[simp] protected theorem add_zero (x : BitVec n) : x + 0#n = x := by simp [add_def]
+
+@[simp] protected theorem zero_add (x : BitVec n) : 0#n + x = x := by simp [add_def]
+
+
+/-! ### sub/neg -/
+
+theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n (x.toNat + (2^n - y.toNat)) := by rfl
+
+@[simp] theorem sub_toNat {n} (x y : BitVec n) :
+  (x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := rfl
+
+@[simp] theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
+  rfl
+@[simp] theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) :=
+  rfl
+@[simp] theorem ofNat_sub_ofNat {n} (x y : Nat) : x#n - y#n = .ofNat n (x + (2^n - y % 2^n)) := by
+  apply eq_of_toNat_eq ; simp [BitVec.ofNat]
+
+@[simp] protected theorem sub_zero (x : BitVec n) : x - (0#n) = x := by apply eq_of_toNat_eq ; simp
+
+@[simp] protected theorem sub_self (x : BitVec n) : x - x = 0#n := by
+  apply eq_of_toNat_eq
+  simp only [sub_toNat]
+  rw [Nat.add_sub_of_le]
+  · simp
+  · exact Nat.le_of_lt x.isLt
+
+@[simp] theorem neg_toNat (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
+  simp [Neg.neg, BitVec.neg]
 
-@[simp] theorem add_zero (x : BitVec n) : x + (0#n) = x := by
+theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
   apply eq_of_toNat_eq
-  simp [toNat_add, isLt, Nat.mod_eq_of_lt]
+  simp
+
+@[simp] theorem neg_zero (n:Nat) : -0#n = 0#n := by apply eq_of_toNat_eq ; simp
+
+/-! ### le and lt -/
+
+theorem le_def (x y : BitVec n) :
+  x ≤ y ↔ x.toNat ≤ y.toNat := Iff.rfl
+
+@[simp] theorem le_ofFin (x : BitVec n) (y : Fin (2^n)) :
+  x ≤ BitVec.ofFin y ↔ x.toFin ≤ y := Iff.rfl
+@[simp] theorem ofFin_le (x : Fin (2^n)) (y : BitVec n) :
+  BitVec.ofFin x ≤ y ↔ x ≤ y.toFin := Iff.rfl
+@[simp] theorem ofNat_le_ofNat {n} (x y : Nat) : (x#n) ≤ (y#n) ↔ x % 2^n ≤ y % 2^n := by
+  simp [le_def]
+
+theorem lt_def (x y : BitVec n) :
+  x < y ↔ x.toNat < y.toNat := Iff.rfl
+
+@[simp] theorem lt_ofFin (x : BitVec n) (y : Fin (2^n)) :
+  x < BitVec.ofFin y ↔ x.toFin < y := Iff.rfl
+@[simp] theorem ofFin_lt (x : Fin (2^n)) (y : BitVec n) :
+  BitVec.ofFin x < y ↔ x < y.toFin := Iff.rfl
+@[simp] theorem ofNat_lt_ofNat {n} (x y : Nat) : (x#n) < (y#n) ↔ x % 2^n < y % 2^n := by
+  simp [lt_def]
+
+protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x < y := by
+  revert h1 h2
+  let ⟨x, lt⟩ := x
+  let ⟨y, lt⟩ := y
+  simp
+  exact Nat.lt_of_le_of_ne