feat: add BitVec.toInt_sdiv plus corresponding BitVec theory (#7565)
This PR adds `BitVec.toInt_sdiv` plus a lot of related bitvector theory around divisions. Coauthored-by: Markus Himmel <markus@lean-fro.org>
This commit is contained in:
Tobias Grosser
GitHub
parent
b2da85971d
commit
149b6423f8
4 changed files with 363 additions and 4 deletions
|
|
@ -1371,6 +1371,261 @@ theorem eq_iff_eq_of_inv (f : α → BitVec w) (g : BitVec w → α) (h : ∀ x,
|
|||
have := congrArg g h'
|
||||
simpa [h] using this
|
||||
|
||||
@[simp]
|
||||
theorem ne_intMin_of_lt_of_msb_false {x : BitVec w} (hw : 0 < w) (hx : x.msb = false) :
|
||||
x ≠ intMin w := by
|
||||
have := toNat_lt_of_msb_false hx
|
||||
simp [toNat_eq, Nat.two_pow_pred_mod_two_pow hw]
|
||||
omega
|
||||
|
||||
@[simp]
|
||||
theorem ne_zero_of_msb_true {x : BitVec w} (hx : x.msb = true) :
|
||||
x ≠ 0#w := by
|
||||
have := Nat.two_pow_pos (w-1)
|
||||
have := le_toNat_of_msb_true hx
|
||||
simp [toNat_eq]
|
||||
omega
|
||||
|
||||
@[simp]
|
||||
theorem msb_neg_of_ne_intMin_of_ne_zero {x : BitVec w} (h : x ≠ intMin w) (h' : x ≠ 0#w) :
|
||||
(-x).msb = !x.msb := by
|
||||
simp only [msb_neg, bool_to_prop]
|
||||
simp [h, h']
|
||||
|
||||
@[simp]
|
||||
theorem udiv_intMin_of_msb_false {x : BitVec w} (h : x.msb = false) :
|
||||
x / intMin w = 0#w := by
|
||||
by_cases hw : w = 0
|
||||
· subst hw
|
||||
decide +revert
|
||||
have wpos : 0 < w := by omega
|
||||
have := Nat.two_pow_pos (w-1)
|
||||
simp [toNat_eq, wpos]
|
||||
rw [Nat.div_eq_zero_iff_lt (by omega)]
|
||||
exact toNat_lt_of_msb_false h
|
||||
|
||||
theorem sdiv_intMin {x : BitVec w} :
|
||||
x.sdiv (intMin w) = if x = intMin w then 1#w else 0#w := by
|
||||
by_cases hw : w = 0
|
||||
· subst hw
|
||||
decide +revert
|
||||
have wpos : 0 < w := by omega
|
||||
by_cases h : x = intMin w
|
||||
· subst h
|
||||
simp
|
||||
omega
|
||||
· simp only [sdiv_eq, msb_intMin, show 0 < w by omega, h]
|
||||
have := Nat.two_pow_pos (w-1)
|
||||
by_cases hx : x.msb
|
||||
· simp [msb_neg_of_ne_intMin_of_ne_zero (by simp [h])
|
||||
(BitVec.ne_zero_of_msb_true hx), hx]
|
||||
· simp [hx]
|
||||
|
||||
theorem sdiv_neg {x y : BitVec w} (h : y ≠ intMin w) :
|
||||
x.sdiv (-y) = -(x.sdiv y) := by
|
||||
by_cases h' : y = 0#w
|
||||
· subst h'
|
||||
simp
|
||||
· simp only [BitVec.sdiv, msb_neg_of_ne_intMin_of_ne_zero h (by simp [h'])]
|
||||
cases x.msb <;> cases y.msb <;> simp
|
||||
|
||||
theorem neg_sdiv {x y : BitVec w} (h : x ≠ intMin w) :
|
||||
(-x).sdiv y = -(x.sdiv y) := by
|
||||
by_cases hx0 : x = 0#w
|
||||
· subst hx0
|
||||
simp
|
||||
· simp only [BitVec.sdiv, msb_neg_of_ne_intMin_of_ne_zero h (by simp [hx0])]
|
||||
cases x.msb <;> cases y.msb <;> simp
|
||||
|
||||
theorem neg_sdiv_neg {x y : BitVec w} (h : x ≠ intMin w) :
|
||||
(-x).sdiv (-y) = x.sdiv y := by
|
||||
by_cases h' : y = intMin w
|
||||
· subst h'
|
||||
simp [sdiv_intMin, neg_intMin]
|
||||
· by_cases hy0 : y = 0#w
|
||||
· subst hy0
|
||||
simp
|
||||
· by_cases hx0 : x = 0#w
|
||||
· subst hx0
|
||||
simp
|
||||
· simp only [BitVec.sdiv,
|
||||
msb_neg_of_ne_intMin_of_ne_zero h (by simp [hx0]),
|
||||
msb_neg_of_ne_intMin_of_ne_zero h' (by simp [hy0])]
|
||||
cases x.msb <;> cases y.msb <;> simp
|
||||
|
||||
theorem intMin_eq_neg_two_pow : intMin w = BitVec.ofInt w (-2 ^ (w - 1)) := by
|
||||
apply BitVec.eq_of_toInt_eq
|
||||
refine (Nat.eq_zero_or_pos w).elim (by rintro rfl; simp [BitVec.toInt_zero_length]) (fun hw => ?_)
|
||||
rw [BitVec.toInt_intMin_of_pos hw, BitVec.toInt_ofInt_eq_self hw (Int.le_refl _)]
|
||||
have := Nat.two_pow_pos (w - 1)
|
||||
norm_cast
|
||||
omega
|
||||
|
||||
theorem toInt_intMin_eq_bmod : (intMin w).toInt = (-2 ^ (w - 1)).bmod (2 ^ w) := by
|
||||
rw [intMin_eq_neg_two_pow, toInt_ofInt]
|
||||
|
||||
@[simp]
|
||||
theorem toInt_bmod_cancel(b : BitVec w) : b.toInt.bmod (2 ^ w) = b.toInt := by
|
||||
rw [toInt_eq_toNat_bmod, Int.bmod_bmod]
|
||||
|
||||
theorem sdiv_ne_intMin_of_ne_intMin {x y : BitVec w} (h : x ≠ intMin w) :
|
||||
x.sdiv y ≠ intMin w := by
|
||||
by_cases hw : w = 0
|
||||
· subst hw
|
||||
simp [BitVec.eq_nil x] at h
|
||||
contradiction
|
||||
simp only [sdiv, udiv_eq, neg_eq]
|
||||
by_cases hx : x.msb <;> by_cases hy : y.msb
|
||||
<;> simp only [hx, hy, neg_ne_intMin_inj]
|
||||
<;> simp only [Bool.not_eq_true] at hx hy
|
||||
<;> apply ne_intMin_of_lt_of_msb_false (by omega)
|
||||
<;> rw [msb_udiv]
|
||||
<;> try simp only [hx, Bool.false_and]
|
||||
· simp [h, ne_zero_of_msb_true, hx]
|
||||
· simp [h, ne_zero_of_msb_true, hx]
|
||||
|
||||
theorem toInt_eq_neg_toNat_neg_of_msb_true {x : BitVec w} (h : x.msb = true) :
|
||||
x.toInt = -((-x).toNat) := by
|
||||
simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.ofNat_emod]
|
||||
norm_cast
|
||||
rw [Nat.mod_eq_of_lt]
|
||||
· omega
|
||||
· have := @BitVec.isLt w x
|
||||
have ne_zero := ne_zero_of_msb_true h
|
||||
simp only [ne_eq, toNat_eq, toNat_ofNat, zero_mod] at ne_zero
|
||||
omega
|
||||
|
||||
theorem toInt_eq_neg_toNat_neg_of_nonpos {x : BitVec w} (h : x = 0#w ∨ x.msb = true) :
|
||||
x.toInt = -((-x).toNat) := by
|
||||
cases h
|
||||
case inl h' =>
|
||||
simp [h']
|
||||
case inr h' =>
|
||||
simp [toInt_eq_neg_toNat_neg_of_msb_true h']
|
||||
|
||||
theorem intMin_udiv_eq_intMin_iff (x : BitVec w) :
|
||||
intMin w / x = intMin w ↔ x = 1#w := by
|
||||
by_cases hw : w = 0; subst hw; decide +revert
|
||||
by_cases hx : x = 1#w; subst hx; simp
|
||||
have wpos : 0 < w := by omega
|
||||
|
||||
have : 0 ≤ (2 ^ (w - 1) / x.toNat) := by simp
|
||||
have := Nat.two_pow_pos (w - 1)
|
||||
|
||||
constructor
|
||||
· intro h
|
||||
rw [← toInt_inj, toInt_eq_msb_cond] at h
|
||||
have : (intMin w / x).msb = false := by simp [msb_udiv, msb_intMin, wpos, hx]
|
||||
simp [this, wpos, toInt_intMin] at h
|
||||
omega
|
||||
· intro h
|
||||
subst h
|
||||
simp
|
||||
|
||||
theorem intMin_udiv_ne_zero_of_ne_zero {b : BitVec w} (hb : b.msb = false) (hb0 : b ≠ 0#w) :
|
||||
intMin w / b ≠ 0#w := by
|
||||
by_cases hw : w = 0; subst hw; decide +revert
|
||||
have wpos : 0 < w := by omega
|
||||
|
||||
simp [toNat_eq] at hb0
|
||||
have := @Nat.div_eq_zero_iff_lt b.toNat (2 ^ (w-1)) (by omega)
|
||||
have := toNat_lt_of_msb_false hb
|
||||
|
||||
simp [toNat_eq, wpos]
|
||||
omega
|
||||
|
||||
theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1#w) :
|
||||
(a.sdiv b).toInt = a.toInt.tdiv b.toInt := by
|
||||
by_cases hw0 : w = 0; subst hw0; decide +revert
|
||||
by_cases hw1 : w = 1; subst hw1; decide +revert
|
||||
by_cases ha0 : a = 0#w; subst ha0; simp
|
||||
by_cases hb0 : b = 0#w; subst hb0; simp
|
||||
by_cases hb1 : b = 1#w; subst hb1; simp [show 1 < w by omega]
|
||||
|
||||
have wpos : 0 < w := by omega
|
||||
have := Nat.two_pow_pos (w - 1)
|
||||
|
||||
by_cases hbintMin : b = intMin w
|
||||
· simp only [ne_eq, Decidable.not_not] at hbintMin
|
||||
subst hbintMin
|
||||
have toIntA_lt := @BitVec.toInt_lt w a; norm_cast at toIntA_lt
|
||||
have le_toIntA := @BitVec.le_toInt w a; norm_cast at le_toIntA
|
||||
simp only [sdiv_intMin, h, ↓reduceIte, toInt_zero, toInt_intMin, wpos,
|
||||
Nat.two_pow_pred_mod_two_pow, Int.tdiv_neg]
|
||||
· by_cases ha_intMin : a = intMin w
|
||||
· simp only [ha_intMin, ↓reduceIte, show 1 < w by omega, toInt_one, toInt_intMin, wpos,
|
||||
Nat.two_pow_pred_mod_two_pow, Int.neg_tdiv, Int.neg_neg]
|
||||
rw [Int.tdiv_self (by omega)]
|
||||
· by_cases ha_nonneg : 0 ≤ a.toInt
|
||||
· simp [Int.tdiv_eq_zero_of_lt ha_nonneg (by norm_cast at *), ha_intMin]
|
||||
· simp only [ne_eq, ← toInt_inj, toInt_intMin, wpos, Nat.two_pow_pred_mod_two_pow] at h
|
||||
rw [← Int.neg_tdiv, Int.tdiv_eq_zero_of_lt (by omega)]
|
||||
· simp [ha_intMin]
|
||||
· simp [wpos, ← toInt_ne, toInt_intMin] at ha_intMin
|
||||
omega
|
||||
|
||||
· by_cases ha : a.msb <;> by_cases hb : b.msb
|
||||
<;> simp only [not_eq_true] at ha hb
|
||||
· simp only [sdiv_eq, ha, hb, udiv_eq]
|
||||
rw [toInt_eq_neg_toNat_neg_of_nonpos (x := a) (by simp [ha]),
|
||||
toInt_eq_neg_toNat_neg_of_nonpos (x := b) (by simp [hb]),
|
||||
Int.neg_tdiv_neg, Int.tdiv_eq_ediv_of_nonneg (by omega)]
|
||||
rw [toInt_eq_toNat_of_msb]
|
||||
· rfl
|
||||
· by_cases ha_intMin : a = intMin w
|
||||
· simp only [ha_intMin, ne_eq, not_true_eq_false, _root_.false_or] at h
|
||||
simp [msb_udiv, neg_eq_iff_eq_neg, h]
|
||||
· simp [msb_udiv, ha_intMin, ha]
|
||||
· have sdiv_toInt_of_msb_true_of_msb_false :
|
||||
(a.sdiv b).toInt = -((-a).toNat / b.toNat) := by
|
||||
simp only [sdiv_eq, ha, hb, udiv_eq]
|
||||
rw [toInt_eq_neg_toNat_neg_of_nonpos]
|
||||
· rw [neg_neg, toNat_udiv, toNat_neg, Int.ofNat_emod, Int.neg_inj]
|
||||
norm_cast
|
||||
· rw [neg_eq_zero_iff]
|
||||
by_cases h' : -a / b = 0#w
|
||||
· simp [h']
|
||||
· by_cases ha_intMin : a = intMin w
|
||||
· have ry := (intMin_udiv_eq_intMin_iff b).mp
|
||||
simp only [hb1, imp_false] at ry
|
||||
simp [msb_udiv, ha_intMin, hb1, ry, intMin_udiv_ne_zero_of_ne_zero, hb, hb0]
|
||||
· have := @BitVec.ne_intMin_of_lt_of_msb_false w ((-a) / b) wpos (by simp [ha, ha0, ha_intMin])
|
||||
simp [msb_neg, h', this, ha, ha_intMin]
|
||||
rw [toInt_eq_toNat_of_msb hb, toInt_eq_neg_toNat_neg_of_msb_true ha, Int.neg_tdiv,
|
||||
Int.tdiv_eq_ediv_of_nonneg (by omega), sdiv_toInt_of_msb_true_of_msb_false]
|
||||
· rw [← @BitVec.neg_neg w (a.sdiv b), ← sdiv_neg hbintMin]
|
||||
have hmb : (-b).msb = false := by simp [hbintMin, hb]
|
||||
rw [toInt_neg_of_ne_intMin]
|
||||
· simp [sdiv, ha, hmb]
|
||||
rw [toInt_udiv_of_msb ha, toInt_eq_toNat_of_msb ha]
|
||||
rw [toInt_eq_neg_toNat_neg_of_msb_true hb, Int.tdiv_neg, Int.tdiv_eq_ediv_of_nonneg (by omega)]
|
||||
· apply sdiv_ne_intMin_of_ne_intMin
|
||||
apply ne_intMin_of_lt_of_msb_false (by omega) ha
|
||||
· rw [sdiv, Int.tdiv_cases, udiv_eq, neg_eq, if_pos (toInt_nonneg_of_msb_false ha),
|
||||
if_pos (toInt_nonneg_of_msb_false hb), ha, hb, toInt_udiv_of_msb ha,
|
||||
toInt_eq_toNat_of_msb ha, toInt_eq_toNat_of_msb hb]
|
||||
|
||||
theorem intMin_sdiv_neg_one : (intMin w).sdiv (-1#w) = intMin w := by
|
||||
refine (Nat.eq_zero_or_pos w).elim (by rintro rfl; exact Subsingleton.elim _ _) (fun hw => ?_)
|
||||
apply BitVec.eq_of_toNat_eq
|
||||
rw [sdiv]
|
||||
simp [msb_intMin, hw, negOne_eq_allOnes, msb_allOnes]
|
||||
have : 2 ≤ 2 ^ w := Nat.pow_one 2 ▸ (Nat.pow_le_pow_iff_right (by omega)).2 (by omega)
|
||||
rw [Nat.sub_sub_self (by omega), Nat.mod_eq_of_lt, Nat.div_one]
|
||||
omega
|
||||
|
||||
theorem toInt_sdiv (a b : BitVec w) : (a.sdiv b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ w) := by
|
||||
by_cases h : a = intMin w ∧ b = -1#w
|
||||
· rcases h with ⟨rfl, rfl⟩
|
||||
rw [BitVec.intMin_sdiv_neg_one]
|
||||
refine (Nat.eq_zero_or_pos w).elim (by rintro rfl; simp [toInt_of_zero_length]) (fun hw => ?_)
|
||||
rw [toInt_intMin_of_pos hw, negOne_eq_allOnes, toInt_allOnes, if_pos hw, Int.tdiv_neg,
|
||||
Int.tdiv_one, Int.neg_neg, Int.bmod_eq_neg (Int.pow_nonneg (by omega))]
|
||||
conv => lhs; rw [(by omega: w = (w - 1) + 1)]
|
||||
simp [Nat.pow_succ, Int.natCast_pow, Int.mul_comm]
|
||||
· rw [← toInt_bmod_cancel]
|
||||
rw [BitVec.toInt_sdiv_of_ne_or_ne _ _ (by simpa only [Classical.not_and_iff_not_or_not] using h)]
|
||||
|
||||
/-! ### Lemmas that use Bitblasting circuits -/
|
||||
|
||||
theorem add_sub_comm {x y : BitVec w} : x + y - z = x - z + y := by
|
||||
|
|
|
|||
|
|
@ -391,6 +391,15 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
|
|||
simp only [toNat_eq, toNat_ofNat, Nat.zero_mod] at h
|
||||
rw [Nat.mod_eq_of_lt (by omega)]
|
||||
|
||||
@[simp] theorem sub_toNat_mod_cancel_of_toNat {x : BitVec w} (h : x.toNat ≠ 0) :
|
||||
(2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat := by
|
||||
by_cases h : w = 0
|
||||
· subst h
|
||||
simp [BitVec.eq_nil x] at h
|
||||
have := x.isLt
|
||||
rw [Nat.mod_eq_of_lt]
|
||||
omega
|
||||
|
||||
@[simp] theorem toNat_mod_cancel_of_lt {x : BitVec n} (h : n < m) : x.toNat % (2 ^ m) = x.toNat := by
|
||||
have : 2 ^ n < 2 ^ m := Nat.pow_lt_pow_of_lt (by omega) h
|
||||
exact Nat.mod_eq_of_lt (by omega)
|
||||
|
|
@ -647,6 +656,34 @@ theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
|
|||
theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by
|
||||
simp [BitVec.toInt, show 0 < 2^w by exact Nat.two_pow_pos w]
|
||||
|
||||
@[simp]
|
||||
theorem toNat_one (h : 0 < w) : (1#w : BitVec w).toNat = 1 := by
|
||||
simp
|
||||
omega
|
||||
|
||||
@[simp]
|
||||
theorem toInt_one (h : 1 < w) : (1#w : BitVec w).toInt = 1 := by
|
||||
rw [toInt_eq_toNat_of_msb, toNat_one (by omega)]
|
||||
· simp
|
||||
· simp
|
||||
omega
|
||||
|
||||
@[simp] theorem sub_toNat_mod_cancel_of_msb_true {x : BitVec w} (h : x.msb = true) :
|
||||
(2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat := by
|
||||
simp only [msb_eq_decide, ge_iff_le, decide_eq_true_eq] at h
|
||||
have := Nat.two_pow_pos (w-1)
|
||||
exact sub_toNat_mod_cancel_of_toNat (by omega)
|
||||
|
||||
theorem toNat_lt_of_msb_false {w : Nat} {x : BitVec w} (h : x.msb = false) : x.toNat < 2 ^ (w - 1) := by
|
||||
have rt := @msb_eq_decide w x
|
||||
simp only [ge_iff_le, false_eq_decide_iff, Nat.not_le, h] at rt
|
||||
omega
|
||||
|
||||
theorem le_toNat_of_msb_true {w : Nat} {x : BitVec w} (h : x.msb = true) : 2 ^ (w - 1) ≤ x.toNat := by
|
||||
have rt := @msb_eq_decide w x
|
||||
simp only [h, ge_iff_le, true_eq_decide_iff] at rt
|
||||
omega
|
||||
|
||||
/--
|
||||
`x.toInt` is less than `2^(w-1)`.
|
||||
We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used.
|
||||
|
|
@ -972,7 +1009,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
|
|||
(extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl
|
||||
|
||||
@[simp] theorem toInt_extractLsb' {s m : Nat} {x : BitVec n} :
|
||||
(extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by
|
||||
(extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by
|
||||
simp [extractLsb', toInt_ofNat]
|
||||
|
||||
@[simp] theorem toInt_extractLsb {hi lo : Nat} {x : BitVec n} :
|
||||
|
|
@ -1179,6 +1216,11 @@ theorem extractLsb'_eq_zero {x : BitVec w} {start : Nat} :
|
|||
simp
|
||||
omega
|
||||
|
||||
theorem msb_allOnes (hw : 0 < w) : (allOnes w).msb = true := by
|
||||
rw [msb_eq_true_iff_two_mul_ge, toNat_allOnes]
|
||||
have : 2 ≤ 2 ^ w := Nat.pow_one 2 ▸ (Nat.pow_le_pow_iff_right (by omega)).2 (by omega)
|
||||
omega
|
||||
|
||||
/-! ### or -/
|
||||
|
||||
@[simp] theorem toNat_or (x y : BitVec v) :
|
||||
|
|
@ -3161,7 +3203,7 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
|
|||
simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega)]
|
||||
|
||||
theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} :
|
||||
(x.toInt - y.toInt < - 2 ^ (w - 1))
|
||||
(x.toInt - y.toInt < - 2 ^ (w - 1))
|
||||
↔ (x.toInt < 0 ∧ 0 ≤ y.toInt ∧ 0 ≤ (x.toInt - y.toInt).bmod (2 ^ w)) := by
|
||||
rcases w with _|w
|
||||
· simp [of_length_zero]
|
||||
|
|
@ -3177,7 +3219,7 @@ theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} :
|
|||
omega
|
||||
|
||||
theorem twoPow_le_toInt_sub_toInt_iff {x y : BitVec w} :
|
||||
(2 ^ (w - 1) ≤ x.toInt - y.toInt)
|
||||
(2 ^ (w - 1) ≤ x.toInt - y.toInt)
|
||||
↔ (0 ≤ x.toInt ∧ y.toInt < 0 ∧ (x.toInt - y.toInt).bmod (2 ^ w) < 0) := by
|
||||
rcases w with _|w
|
||||
· simp [of_length_zero]
|
||||
|
|
@ -3301,6 +3343,14 @@ theorem neg_neg {x : BitVec w} : - - x = x := by
|
|||
protected theorem neg_inj {x y : BitVec w} : -x = -y ↔ x = y :=
|
||||
⟨fun h => by rw [← @neg_neg w x, ← @neg_neg w y, h], congrArg _⟩
|
||||
|
||||
theorem neg_eq_iff_eq_neg {x y : BitVec w} : -x = y ↔ x = -y := by
|
||||
constructor
|
||||
all_goals
|
||||
intro h
|
||||
symm at h
|
||||
subst h
|
||||
simp
|
||||
|
||||
theorem neg_ne_iff_ne_neg {x y : BitVec w} : -x ≠ y ↔ x ≠ -y := by
|
||||
constructor
|
||||
all_goals
|
||||
|
|
@ -3736,7 +3786,8 @@ theorem msb_udiv (x y : BitVec w) :
|
|||
≤ x.toNat / 2 := by apply Nat.div_add_le_right (by omega)
|
||||
_ < 2 ^ w := by omega
|
||||
|
||||
theorem msb_udiv_eq_false_of {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
|
||||
@[simp]
|
||||
theorem msb_udiv_eq_false_of {x : BitVec w} {y : BitVec w} (h : x.msb = false) :
|
||||
(x / y).msb = false := by
|
||||
simp [msb_udiv, h]
|
||||
|
||||
|
|
@ -4610,6 +4661,17 @@ The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `
|
|||
theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by
|
||||
simp [intMin]
|
||||
|
||||
@[simp]
|
||||
theorem intMin_eq_zero_iff {w : Nat} : intMin w = 0#w ↔ w = 0 := by
|
||||
by_cases h : w = 0
|
||||
· subst h
|
||||
decide +revert
|
||||
· constructor
|
||||
· have := Nat.two_pow_pos (w - 1)
|
||||
simp [toNat_eq, show 0 < w by omega]
|
||||
omega
|
||||
· simp [h]
|
||||
|
||||
/--
|
||||
The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
|
||||
-/
|
||||
|
|
@ -4652,6 +4714,14 @@ theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
|
|||
· simp only [Nat.not_lt, Nat.le_zero_eq] at h
|
||||
simp [bitvec_to_nat, h]
|
||||
|
||||
@[simp]
|
||||
theorem neg_eq_intMin {x : BitVec w} : -x = intMin w ↔ x = intMin w := by
|
||||
rw [← BitVec.neg_inj, neg_neg, neg_intMin]
|
||||
|
||||
theorem neg_ne_intMin_inj {x : BitVec w} :
|
||||
-x ≠ intMin w ↔ x ≠ intMin w := by
|
||||
rw [←neg_intMin, neg_ne_iff_ne_neg, neg_neg, neg_intMin]
|
||||
|
||||
@[simp]
|
||||
theorem abs_intMin {w : Nat} : (intMin w).abs = intMin w := by
|
||||
simp [BitVec.abs, bitvec_to_nat]
|
||||
|
|
|
|||
|
|
@ -732,6 +732,22 @@ theorem neg_ediv {a b : Int} : (-a) / b = -(a / b) - if b ∣ a then 0 else b.si
|
|||
· have := emod_lt_of_neg a hb
|
||||
omega
|
||||
|
||||
theorem tdiv_cases (n m : Int) : n.tdiv m =
|
||||
if 0 ≤ n then
|
||||
if 0 ≤ m then n / m else -(n / (-m))
|
||||
else
|
||||
if 0 ≤ m then -((-n) / m) else (-n) / (-m) := by
|
||||
split <;> rename_i hn
|
||||
· split <;> rename_i hm
|
||||
· rw [Int.tdiv_eq_ediv_of_nonneg hn]
|
||||
· rw [Int.tdiv_eq_ediv_of_nonneg hn]
|
||||
simp
|
||||
· split <;> rename_i hm
|
||||
· rw [Int.tdiv_eq_ediv, Int.neg_ediv]
|
||||
simp [hn, Int.neg_sub, Int.add_comm]
|
||||
· rw [Int.tdiv_eq_ediv, Int.neg_ediv, Int.ediv_neg]
|
||||
simp [hn, Int.sub_eq_add_neg, apply_ite Neg.neg]
|
||||
|
||||
theorem neg_emod {a b : Int} : (-a) % b = if b ∣ a then 0 else b.natAbs - (a % b) := by
|
||||
rw [emod_def, emod_def, neg_ediv, Int.mul_sub, Int.mul_neg]
|
||||
split <;> rename_i h
|
||||
|
|
@ -2269,6 +2285,14 @@ theorem bmod_lt {x : Int} {m : Nat} (h : 0 < m) : bmod x m < (m + 1) / 2 := by
|
|||
theorem bmod_eq_emod_of_lt {x : Int} {m : Nat} (hx : x % m < (m + 1) / 2) : bmod x m = x % m := by
|
||||
simp [bmod, hx]
|
||||
|
||||
theorem bmod_eq_neg {n : Nat} {m : Int} (hm : 0 ≤ m) (hn : n = 2 * m) : m.bmod n = -m := by
|
||||
by_cases h : m = 0
|
||||
· subst h; simp
|
||||
· rw [Int.bmod_def, hn, if_neg]
|
||||
· rw [Int.emod_eq_of_lt hm] <;> omega
|
||||
· simp only [Int.not_lt]
|
||||
rw [Int.emod_eq_of_lt hm] <;> omega
|
||||
|
||||
theorem bmod_le {x : Int} {m : Nat} (h : 0 < m) : bmod x m ≤ (m - 1) / 2 := by
|
||||
refine lt_add_one_iff.mp ?_
|
||||
calc
|
||||
|
|
|
|||
|
|
@ -17,6 +17,16 @@ protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
|
|||
protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
|
||||
rw [Int.mul_comm, Int.pow_succ]
|
||||
|
||||
protected theorem pow_pos {n : Int} {m : Nat} : 0 < n → 0 < n ^ m := by
|
||||
induction m with
|
||||
| zero => simp
|
||||
| succ m ih => exact fun h => Int.mul_pos (ih h) h
|
||||
|
||||
protected theorem pow_nonneg {n : Int} {m : Nat} : 0 ≤ n → 0 ≤ n ^ m := by
|
||||
induction m with
|
||||
| zero => simp
|
||||
| succ m ih => exact fun h => Int.mul_nonneg (ih h) h
|
||||
|
||||
@[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
|
||||
abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue