From 062ecb5eaed79e29ec22951a7ab5eefc8b2e99bc Mon Sep 17 00:00:00 2001 From: Siddharth Date: Thu, 26 Sep 2024 18:45:31 -0500 Subject: [PATCH] feat: add udiv/umod bitblasting for bv_decide (#5281) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds the theorems ``` @[simp] theorem divRec_zero (qr : DivModState w) : divRec w w 0 n d qr = qr @[simp] theorem divRec_succ' (wn : Nat) (qr : DivModState w) : divRec w wr (wn + 1) n d qr = let r' := shiftConcat qr.r (n.getLsbD wn) let input : DivModState w := if r' < d then ⟨qr.q.shiftConcat false, r'⟩ else ⟨qr.q.shiftConcat true, r' - d⟩ divRec w (wr + 1) wn n d input ``` The final statements may need some masasging to interoperate with `bv_decide`. We prove the recurrence for unsigned division by building a shift-subtract circuit, and then showing that this circuit obeys the division algorithm's invariant. --- A `DivModState` is lawful if the remainder width `wr` plus the dividend width `wn` equals `w`, and the bitvectors `r` and `n` have values in the bounds given by bitwidths `wr`, resp. `wn`. This is a proof engineering choice: An alternative world could have `r : BitVec wr` and `n : BitVec wn`, but this required much more dependent typing coercions. Instead, we choose to declare all involved bitvectors as length `w`, and then prove that the values are within their respective bounds. --------- Co-authored-by: Tobias Grosser Co-authored-by: Alex Keizer Co-authored-by: Kim Morrison Co-authored-by: Tobias Grosser --- src/Init/Data/BitVec/Basic.lean | 7 + src/Init/Data/BitVec/Bitblast.lean | 380 +++++++++++++++++++++++++++++ src/Init/Data/BitVec/Lemmas.lean | 67 +++++ src/Init/Data/Bool.lean | 5 +- src/Init/Data/Nat/Lemmas.lean | 5 + 5 files changed, 462 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 37ae83c0e1..dacdc0f69d 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -676,6 +676,13 @@ result of appending a single bit to the front in the naive implementation). That is, the new bit is the least significant bit. -/ def concat {n} (msbs : BitVec n) (lsb : Bool) : BitVec (n+1) := msbs ++ (ofBool lsb) +/-- +`x.shiftConcat b` shifts all bits of `x` to the left by `1` and sets the least significant bit to `b`. +It is a non-dependent version of `concat` that does not change the total bitwidth. +-/ +def shiftConcat (x : BitVec n) (b : Bool) : BitVec n := + (x.concat b).truncate n + /-- Prepend a single bit to the front of a bitvector, using big endian order (see `append`). That is, the new bit is the most significant bit. -/ def cons {n} (msb : Bool) (lsbs : BitVec n) : BitVec (n+1) := diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index a8ce5b31dd..431b6237bd 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -438,6 +438,386 @@ theorem shiftLeft_eq_shiftLeftRec (x : BitVec w₁) (y : BitVec w₂) : · simp [of_length_zero] · simp [shiftLeftRec_eq] +/-! # udiv/urem recurrence for bitblasting + +In order to prove the correctness of the division algorithm on the integers, +one shows that `n.div d = q` and `n.mod d = r` iff `n = d * q + r` and `0 ≤ r < d`. +Mnemonic: `n` is the numerator, `d` is the denominator, `q` is the quotient, and `r` the remainder. + +This *uniqueness of decomposition* is not true for bitvectors. +For `n = 0, d = 3, w = 3`, we can write: +- `0 = 0 * 3 + 0` (`q = 0`, `r = 0 < 3`.) +- `0 = 2 * 3 + 2 = 6 + 2 ≃ 0 (mod 8)` (`q = 2`, `r = 2 < 3`). + +Such examples can be created by choosing different `(q, r)` for a fixed `(d, n)` +such that `(d * q + r)` overflows and wraps around to equal `n`. + +This tells us that the division algorithm must have more restrictions than just the ones +we have for integers. These restrictions are captured in `DivModState.Lawful`. +The key idea is to state the relationship in terms of the toNat values of {n, d, q, r}. +If the division equation `d.toNat * q.toNat + r.toNat = n.toNat` holds, +then `n.udiv d = q` and `n.umod d = r`. + +Following this, we implement the division algorithm by repeated shift-subtract. + +References: +- Fast 32-bit Division on the DSP56800E: Minimized nonrestoring division algorithm by David Baca +- Bitwuzla sources for bitblasting.h +-/ + +private theorem Nat.div_add_eq_left_of_lt {x y z : Nat} (hx : z ∣ x) (hy : y < z) (hz : 0 < z) : + (x + y) / z = x / z := by + refine Nat.div_eq_of_lt_le ?lo ?hi + · apply Nat.le_trans + · exact div_mul_le_self x z + · omega + · simp only [succ_eq_add_one, Nat.add_mul, Nat.one_mul] + apply Nat.add_lt_add_of_le_of_lt + · apply Nat.le_of_eq + exact (Nat.div_eq_iff_eq_mul_left hz hx).mp rfl + · exact hy + +/-- If the division equation `d.toNat * q.toNat + r.toNat = n.toNat` holds, +then `n.udiv d = q`. -/ +theorem udiv_eq_of_mul_add_toNat {d n q r : BitVec w} (hd : 0 < d) + (hrd : r < d) + (hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) : + n.udiv d = q := by + apply BitVec.eq_of_toNat_eq + rw [toNat_udiv] + replace hdqnr : (d.toNat * q.toNat + r.toNat) / d.toNat = n.toNat / d.toNat := by + simp [hdqnr] + rw [Nat.div_add_eq_left_of_lt] at hdqnr + · rw [← hdqnr] + exact mul_div_right q.toNat hd + · exact Nat.dvd_mul_right d.toNat q.toNat + · exact hrd + · exact hd + +/-- If the division equation `d.toNat * q.toNat + r.toNat = n.toNat` holds, +then `n.umod d = r`. -/ +theorem umod_eq_of_mul_add_toNat {d n q r : BitVec w} (hrd : r < d) + (hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) : + n.umod d = r := by + apply BitVec.eq_of_toNat_eq + rw [toNat_umod] + replace hdqnr : (d.toNat * q.toNat + r.toNat) % d.toNat = n.toNat % d.toNat := by + simp [hdqnr] + rw [Nat.add_mod, Nat.mul_mod_right] at hdqnr + simp only [Nat.zero_add, mod_mod] at hdqnr + replace hrd : r.toNat < d.toNat := by + simpa [BitVec.lt_def] using hrd + rw [Nat.mod_eq_of_lt hrd] at hdqnr + simp [hdqnr] + +/-! ### DivModState -/ + +/-- `DivModState` is a structure that maintains the state of recursive `divrem` calls. -/ +structure DivModState (w : Nat) : Type where + /-- The number of bits in the numerator that are not yet processed -/ + wn : Nat + /-- The number of bits in the remainder (and quotient) -/ + wr : Nat + /-- The current quotient. -/ + q : BitVec w + /-- The current remainder. -/ + r : BitVec w + + +/-- `DivModArgs` contains the arguments to a `divrem` call which remain constant throughout +execution. -/ +structure DivModArgs (w : Nat) where + /-- the numerator (aka, dividend) -/ + n : BitVec w + /-- the denumerator (aka, divisor)-/ + d : BitVec w + +/-- A `DivModState` is lawful if the remainder width `wr` plus the numerator width `wn` equals `w`, +and the bitvectors `r` and `n` have values in the bounds given by bitwidths `wr`, resp. `wn`. + +This is a proof engineering choice: an alternative world could have been +`r : BitVec wr` and `n : BitVec wn`, but this required much more dependent typing coercions. + +Instead, we choose to declare all involved bitvectors as length `w`, and then prove that +the values are within their respective bounds. + +We start with `wn = w` and `wr = 0`, and then in each step, we decrement `wn` and increment `wr`. +In this way, we grow a legal remainder in each loop iteration. +-/ +structure DivModState.Lawful {w : Nat} (args : DivModArgs w) (qr : DivModState w) : Prop where + /-- The sum of widths of the dividend and remainder is `w`. -/ + hwrn : qr.wr + qr.wn = w + /-- The denominator is positive. -/ + hdPos : 0 < args.d + /-- The remainder is strictly less than the denominator. -/ + hrLtDivisor : qr.r.toNat < args.d.toNat + /-- The remainder is morally a `Bitvec wr`, and so has value less than `2^wr`. -/ + hrWidth : qr.r.toNat < 2^qr.wr + /-- The quotient is morally a `Bitvec wr`, and so has value less than `2^wr`. -/ + hqWidth : qr.q.toNat < 2^qr.wr + /-- The low `(w - wn)` bits of `n` obey the invariant for division. -/ + hdiv : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat + +/-- A lawful DivModState implies `w > 0`. -/ +def DivModState.Lawful.hw {args : DivModArgs w} {qr : DivModState w} + {h : DivModState.Lawful args qr} : 0 < w := by + have hd := h.hdPos + rcases w with rfl | w + · have hcontra : args.d = 0#0 := by apply Subsingleton.elim + rw [hcontra] at hd + simp at hd + · omega + +/-- An initial value with both `q, r = 0`. -/ +def DivModState.init (w : Nat) : DivModState w := { + wn := w + wr := 0 + q := 0#w + r := 0#w +} + +/-- The initial state is lawful. -/ +def DivModState.lawful_init {w : Nat} (args : DivModArgs w) (hd : 0#w < args.d) : + DivModState.Lawful args (DivModState.init w) := by + simp only [BitVec.DivModState.init] + exact { + hwrn := by simp only; omega, + hdPos := by assumption + hrLtDivisor := by simp [BitVec.lt_def] at hd ⊢; assumption + hrWidth := by simp [DivModState.init], + hqWidth := by simp [DivModState.init], + hdiv := by + simp only [DivModState.init, toNat_ofNat, zero_mod, Nat.mul_zero, Nat.add_zero]; + rw [Nat.shiftRight_eq_div_pow] + apply Nat.div_eq_of_lt args.n.isLt + } + +/-- +A lawful DivModState with a fully consumed dividend (`wn = 0`) witnesses that the +quotient has been correctly computed. +-/ +theorem DivModState.udiv_eq_of_lawful {n d : BitVec w} {qr : DivModState w} + (h_lawful : DivModState.Lawful {n, d} qr) + (h_final : qr.wn = 0) : + n.udiv d = qr.q := by + apply udiv_eq_of_mul_add_toNat h_lawful.hdPos h_lawful.hrLtDivisor + have hdiv := h_lawful.hdiv + simp only [h_final] at * + omega + +/-- +A lawful DivModState with a fully consumed dividend (`wn = 0`) witnesses that the +remainder has been correctly computed. +-/ +theorem DivModState.umod_eq_of_lawful {qr : DivModState w} + (h : DivModState.Lawful {n, d} qr) + (h_final : qr.wn = 0) : + n.umod d = qr.r := by + apply umod_eq_of_mul_add_toNat h.hrLtDivisor + have hdiv := h.hdiv + simp only [shiftRight_zero] at hdiv + simp only [h_final] at * + exact hdiv.symm + +/-! ### DivModState.Poised -/ + +/-- +A `Poised` DivModState is a state which is `Lawful` and furthermore, has at least +one numerator bit left to process `(0 < wn)` + +The input to the shift subtractor is a legal input to `divrem`, and we also need to have an +input bit to perform shift subtraction on, and thus we need `0 < wn`. +-/ +structure DivModState.Poised {w : Nat} (args : DivModArgs w) (qr : DivModState w) + extends DivModState.Lawful args qr : Type where + /-- Only perform a round of shift-subtract if we have dividend bits. -/ + hwn_lt : 0 < qr.wn + +/-- +In the shift subtract input, the dividend is at least one bit long (`wn > 0`), so +the remainder has bits to be computed (`wr < w`). +-/ +def DivModState.wr_lt_w {qr : DivModState w} (h : qr.Poised args) : qr.wr < w := by + have hwrn := h.hwrn + have hwn_lt := h.hwn_lt + omega + +/-! ### Division shift subtractor -/ + +/-- +One round of the division algorithm, that tries to perform a subtract shift. +Note that this should only be called when `r.msb = false`, so we will not overflow. +-/ +def divSubtractShift (args : DivModArgs w) (qr : DivModState w) : DivModState w := + let {n, d} := args + let wn := qr.wn - 1 + let wr := qr.wr + 1 + let r' := shiftConcat qr.r (n.getLsbD wn) + if r' < d then { + q := qr.q.shiftConcat false, -- If `r' < d`, then we do not have a quotient bit. + r := r' + wn, wr + } else { + q := qr.q.shiftConcat true, -- Otherwise, `r' ≥ d`, and we have a quotient bit. + r := r' - d -- we subtract to maintain the invariant that `r < d`. + wn, wr + } + +/-- The value of shifting right by `wn - 1` equals shifting by `wn` and grabbing the lsb at `(wn - 1)`. -/ +theorem DivModState.toNat_shiftRight_sub_one_eq + {args : DivModArgs w} {qr : DivModState w} (h : qr.Poised args) : + args.n.toNat >>> (qr.wn - 1) + = (args.n.toNat >>> qr.wn) * 2 + (args.n.getLsbD (qr.wn - 1)).toNat := by + show BitVec.toNat (args.n >>> (qr.wn - 1)) = _ + have {..} := h -- break the structure down for `omega` + rw [shiftRight_sub_one_eq_shiftConcat args.n h.hwn_lt] + rw [toNat_shiftConcat_eq_of_lt (k := w - qr.wn)] + · simp + · omega + · apply BitVec.toNat_ushiftRight_lt + omega + +/-- +This is used when proving the correctness of the divison algorithm, +where we know that `r < d`. +We then want to show that `((r.shiftConcat b) - d) < d` as the loop invariant. +In arithmetic, this is the same as showing that +`r * 2 + 1 - d < d`, which this theorem establishes. +-/ +private theorem two_mul_add_sub_lt_of_lt_of_lt_two (h : a < x) (hy : y < 2) : + 2 * a + y - x < x := by omega + +/-- We show that the output of `divSubtractShift` is lawful, which tells us that it +obeys the division equation. -/ +theorem lawful_divSubtractShift (qr : DivModState w) (h : qr.Poised args) : + DivModState.Lawful args (divSubtractShift args qr) := by + rcases args with ⟨n, d⟩ + simp only [divSubtractShift, decide_eq_true_eq] + -- We add these hypotheses for `omega` to find them later. + have ⟨⟨hrwn, hd, hrd, hr, hn, hrnd⟩, hwn_lt⟩ := h + have : d.toNat * (qr.q.toNat * 2) = d.toNat * qr.q.toNat * 2 := by rw [Nat.mul_assoc] + by_cases rltd : shiftConcat qr.r (n.getLsbD (qr.wn - 1)) < d + · simp only [rltd, ↓reduceIte] + constructor <;> try bv_omega + case pos.hrWidth => apply toNat_shiftConcat_lt_of_lt <;> omega + case pos.hqWidth => apply toNat_shiftConcat_lt_of_lt <;> omega + case pos.hdiv => + simp [qr.toNat_shiftRight_sub_one_eq h, h.hdiv, this, + toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hrWidth, + toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hqWidth] + omega + · simp only [rltd, ↓reduceIte] + constructor <;> try bv_omega + case neg.hrLtDivisor => + simp only [lt_def, Nat.not_lt] at rltd + rw [BitVec.toNat_sub_of_le rltd, + toNat_shiftConcat_eq_of_lt (hk := qr.wr_lt_w h) (hx := h.hrWidth), + Nat.mul_comm] + apply two_mul_add_sub_lt_of_lt_of_lt_two <;> bv_omega + case neg.hrWidth => + simp only + have hdr' : d ≤ (qr.r.shiftConcat (n.getLsbD (qr.wn - 1))) := + BitVec.not_lt_iff_le.mp rltd + have hr' : ((qr.r.shiftConcat (n.getLsbD (qr.wn - 1)))).toNat < 2 ^ (qr.wr + 1) := by + apply toNat_shiftConcat_lt_of_lt <;> bv_omega + rw [BitVec.toNat_sub_of_le hdr'] + omega + case neg.hqWidth => + apply toNat_shiftConcat_lt_of_lt <;> omega + case neg.hdiv => + have rltd' := (BitVec.not_lt_iff_le.mp rltd) + simp only [qr.toNat_shiftRight_sub_one_eq h, + BitVec.toNat_sub_of_le rltd', + toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hrWidth] + simp only [BitVec.le_def, + toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hrWidth] at rltd' + simp only [toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hqWidth, h.hdiv, Nat.mul_add] + bv_omega + +/-! ### Core division algorithm circuit -/ + +/-- A recursive definition of division for bitblasting, in terms of a shift-subtraction circuit. -/ +def divRec {w : Nat} (m : Nat) (args : DivModArgs w) (qr : DivModState w) : + DivModState w := + match m with + | 0 => qr + | m + 1 => divRec m args <| divSubtractShift args qr + +@[simp] +theorem divRec_zero (qr : DivModState w) : + divRec 0 args qr = qr := rfl + +@[simp] +theorem divRec_succ (m : Nat) (args : DivModArgs w) (qr : DivModState w) : + divRec (m + 1) args qr = + divRec m args (divSubtractShift args qr) := rfl + +/-- The output of `divRec` is a lawful state -/ +theorem lawful_divRec {args : DivModArgs w} {qr : DivModState w} + (h : DivModState.Lawful args qr) : + DivModState.Lawful args (divRec qr.wn args qr) := by + generalize hm : qr.wn = m + induction m generalizing qr + case zero => + exact h + case succ wn' ih => + simp only [divRec_succ] + apply ih + · apply lawful_divSubtractShift + constructor + · assumption + · omega + · simp only [divSubtractShift, hm] + split <;> rfl + +/-- The output of `divRec` has no more bits left to process (i.e., `wn = 0`) -/ +@[simp] +theorem wn_divRec (args : DivModArgs w) (qr : DivModState w) : + (divRec qr.wn args qr).wn = 0 := by + generalize hm : qr.wn = m + induction m generalizing qr + case zero => + assumption + case succ wn' ih => + apply ih + simp only [divSubtractShift, hm] + split <;> rfl + +/-- The result of `udiv` agrees with the result of the division recurrence. -/ +theorem udiv_eq_divRec (hd : 0#w < d) : + let out := divRec w {n, d} (DivModState.init w) + n.udiv d = out.q := by + have := DivModState.lawful_init {n, d} hd + have := lawful_divRec this + apply DivModState.udiv_eq_of_lawful this (wn_divRec ..) + +/-- The result of `umod` agrees with the result of the division recurrence. -/ +theorem umod_eq_divRec (hd : 0#w < d) : + let out := divRec w {n, d} (DivModState.init w) + n.umod d = out.r := by + have := DivModState.lawful_init {n, d} hd + have := lawful_divRec this + apply DivModState.umod_eq_of_lawful this (wn_divRec ..) + +@[simp] +theorem divRec_succ' (m : Nat) (args : DivModArgs w) (qr : DivModState w) : + divRec (m+1) args qr = + let wn := qr.wn - 1 + let wr := qr.wr + 1 + let r' := shiftConcat qr.r (args.n.getLsbD wn) + let input : DivModState _ := + if r' < args.d then { + q := qr.q.shiftConcat false, + r := r' + wn, wr + } else { + q := qr.q.shiftConcat true, + r := r' - args.d + wn, wr + } + divRec m args input := by + simp [divRec_succ, divSubtractShift] + /- ### Arithmetic shift right (sshiftRight) recurrence -/ /-- diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index dedf3c5a34..84b672b2a9 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1149,6 +1149,17 @@ theorem ushiftRight_or_distrib (x y : BitVec w) (n : Nat) : theorem ushiftRight_zero_eq (x : BitVec w) : x >>> 0 = x := by simp [bv_toNat] +/-- +Shifting right by `n < w` yields a bitvector whose value is less than `2 ^ (w - n)`. +-/ +theorem toNat_ushiftRight_lt (x : BitVec w) (n : Nat) (hn : n ≤ w) : + (x >>> n).toNat < 2 ^ (w - n) := by + rw [toNat_ushiftRight, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul] + · rw [Nat.pow_sub_mul_pow] + · apply x.isLt + · apply hn + · apply Nat.pow_pos (by decide) + /-! ### ushiftRight reductions from BitVec to Nat -/ @[simp] @@ -1698,6 +1709,51 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) : (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by ext i; cases i using Fin.succRecOn <;> simp +/-! ### shiftConcat -/ + +theorem getLsbD_shiftConcat (x : BitVec w) (b : Bool) (i : Nat) : + (shiftConcat x b).getLsbD i + = (decide (i < w) && (if (i = 0) then b else x.getLsbD (i - 1))) := by + simp only [shiftConcat, getLsbD_setWidth, getLsbD_concat] + +theorem getLsbD_shiftConcat_eq_decide (x : BitVec w) (b : Bool) (i : Nat) : + (shiftConcat x b).getLsbD i + = (decide (i < w) && ((decide (i = 0) && b) || (decide (0 < i) && x.getLsbD (i - 1)))) := by + simp only [getLsbD_shiftConcat] + split <;> simp [*, show ((0 < i) ↔ ¬(i = 0)) by omega] + +theorem shiftRight_sub_one_eq_shiftConcat (n : BitVec w) (hwn : 0 < wn) : + n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1)) := by + ext i + simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, Fin.is_lt, decide_True, Bool.true_and] + split + · simp [*] + · congr 1; omega + +@[simp, bv_toNat] +theorem toNat_shiftConcat {x : BitVec w} {b : Bool} : + (x.shiftConcat b).toNat + = (x.toNat <<< 1 + b.toNat) % 2 ^ w := by + simp [shiftConcat, Nat.shiftLeft_eq] + +/-- `x.shiftConcat b` does not overflow if `x < 2^k` for `k < w`, and so +`x.shiftConcat b |>.toNat = x.toNat * 2 + b.toNat`. -/ +theorem toNat_shiftConcat_eq_of_lt {x : BitVec w} {b : Bool} {k : Nat} + (hk : k < w) (hx : x.toNat < 2 ^ k) : + (x.shiftConcat b).toNat = x.toNat * 2 + b.toNat := by + simp only [toNat_shiftConcat, Nat.shiftLeft_eq, Nat.pow_one] + have : 2 ^ k < 2 ^ w := Nat.pow_lt_pow_of_lt (by omega) (by omega) + have : 2 ^ k * 2 ≤ 2 ^ w := (Nat.pow_lt_pow_iff_pow_mul_le_pow (by omega)).mp this + rw [Nat.mod_eq_of_lt (by cases b <;> simp [bv_toNat] <;> omega)] + +theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat} + (hk : k < w) (hx : x.toNat < 2 ^ k) : + (x.shiftConcat b).toNat < 2 ^ (k + 1) := by + rw [toNat_shiftConcat_eq_of_lt hk hx] + have : 2 ^ (k + 1) ≤ 2 ^ w := Nat.pow_le_pow_of_le_right (by decide) (by assumption) + have := Bool.toNat_lt b + omega + @[simp] theorem zero_concat_false : concat 0#w false = 0#(w + 1) := by ext simp [getLsbD_concat] @@ -1992,6 +2048,10 @@ protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x.umod y < y simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod, umod, toNat_ofNatLt] apply Nat.mod_lt +theorem not_lt_iff_le {x y : BitVec w} : (¬ x < y) ↔ y ≤ x := by + constructor <;> + (intro h; simp only [lt_def, Nat.not_lt, le_def] at h ⊢; omega) + /-! ### ofBoolList -/ @[simp] theorem getMsbD_ofBoolListBE : (ofBoolListBE bs).getMsbD i = bs.getD i false := by @@ -2237,6 +2297,13 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by rw [← twoPow_zero, getLsbD_twoPow] +theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) : + x <<< n = x * (BitVec.twoPow w n) := by + ext i + simp [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, mul_twoPow_eq_shiftLeft] + +/- ### cons -/ + @[simp] theorem true_cons_zero : cons true 0#w = twoPow (w + 1) w := by ext simp [getLsbD_cons] diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index b4017cba83..edfff1ac73 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -368,13 +368,14 @@ theorem and_or_inj_left_iff : /-- convert a `Bool` to a `Nat`, `false -> 0`, `true -> 1` -/ def toNat (b : Bool) : Nat := cond b 1 0 -@[simp] theorem toNat_false : false.toNat = 0 := rfl +@[simp, bv_toNat] theorem toNat_false : false.toNat = 0 := rfl -@[simp] theorem toNat_true : true.toNat = 1 := rfl +@[simp, bv_toNat] theorem toNat_true : true.toNat = 1 := rfl theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by cases c <;> trivial +@[bv_toNat] theorem toNat_lt (b : Bool) : b.toNat < 2 := Nat.lt_succ_of_le (toNat_le _) diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 85f9db8d64..ca5b7065c4 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -770,6 +770,11 @@ protected theorem two_pow_pred_mod_two_pow (h : 0 < w) : rw [mod_eq_of_lt] apply Nat.pow_pred_lt_pow (by omega) h +protected theorem pow_lt_pow_iff_pow_mul_le_pow {a n m : Nat} (h : 1 < a) : + a ^ n < a ^ m ↔ a ^ n * a ≤ a ^ m := by + rw [←Nat.pow_add_one, Nat.pow_le_pow_iff_right (by omega), Nat.pow_lt_pow_iff_right (by omega)] + omega + @[simp] theorem two_pow_pred_mul_two (h : 0 < w) : 2 ^ (w - 1) * 2 = 2 ^ w := by