Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: define udiv normal form to be /, resp. umod and % #5645

Merged
merged 2 commits into from
Oct 8, 2024
Merged

chore: define udiv normal form to be /, resp. umod and % #5645

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f1b996e
chore: define udiv normal form to be %, resp. umod and %.
bollu Oct 8, 2024
5e958f5
fix rebased changes
hargoniX Oct 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/Init/Data/BitVec/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -718,6 +718,8 @@ section normalization_eqs
@[simp] theorem add_eq (x y : BitVec w) : BitVec.add x y = x + y := rfl
@[simp] theorem sub_eq (x y : BitVec w) : BitVec.sub x y = x - y := rfl
@[simp] theorem mul_eq (x y : BitVec w) : BitVec.mul x y = x * y := rfl
@[simp] theorem udiv_eq (x y : BitVec w) : BitVec.udiv x y = x / y := rfl
@[simp] theorem umod_eq (x y : BitVec w) : BitVec.umod x y = x % y := rfl
@[simp] theorem zero_eq : BitVec.zero n = 0#n := rfl
end normalization_eqs

Expand Down
12 changes: 6 additions & 6 deletions src/Init/Data/BitVec/Bitblast.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -571,7 +571,7 @@ 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
n / 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
Expand All @@ -587,7 +587,7 @@ theorem udiv_eq_of_mul_add_toNat {d n q r : BitVec w} (hd : 0 < d)
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
n % 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
Expand Down Expand Up @@ -688,7 +688,7 @@ 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
n / 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 *
Expand All @@ -701,7 +701,7 @@ 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
n % d = qr.r := by
apply umod_eq_of_mul_add_toNat h.hrLtDivisor
have hdiv := h.hdiv
simp only [shiftRight_zero] at hdiv
Expand Down Expand Up @@ -875,15 +875,15 @@ theorem wn_divRec (args : DivModArgs w) (qr : DivModState w) :
/-- 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
n / 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
n % d = out.r := by
have := DivModState.lawful_init {n, d} hd
have := lawful_divRec this
apply DivModState.umod_eq_of_lawful this (wn_divRec ..)
Expand Down
25 changes: 13 additions & 12 deletions src/Init/Data/BitVec/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1339,37 +1339,38 @@ theorem sshiftRight_eq' (x : BitVec w) : x.sshiftRight' y = x.sshiftRight y.toNa

/-! ### udiv -/

theorem udiv_eq {x y : BitVec n} : x.udiv y = BitVec.ofNat n (x.toNat / y.toNat) := by
theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat) := by
have h : x.toNat / y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)
rw [← udiv_eq]
simp [udiv, bv_toNat, h, Nat.mod_eq_of_lt]

@[simp, bv_toNat]
theorem toNat_udiv {x y : BitVec n} : (x.udiv y).toNat = x.toNat / y.toNat := by
simp only [udiv_eq]
theorem toNat_udiv {x y : BitVec n} : (x / y).toNat = x.toNat / y.toNat := by
rw [udiv_def]
by_cases h : y = 0
· simp [h]
· rw [toNat_ofNat, Nat.mod_eq_of_lt]
exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)

@[simp]
theorem udiv_zero {x : BitVec n} : x.udiv 0#n = 0#n := by
simp only [udiv, toNat_ofNat, Nat.zero_mod, Nat.div_zero]
rfl
theorem udiv_zero {x : BitVec n} : x / 0#n = 0#n := by
simp [udiv_def]

/-! ### umod -/

theorem umod_eq {x y : BitVec n} :
x.umod y = BitVec.ofNat n (x.toNat % y.toNat) := by
theorem umod_def {x y : BitVec n} :
x % y = BitVec.ofNat n (x.toNat % y.toNat) := by
rw [← umod_eq]
have h : x.toNat % y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt
simp [umod, bv_toNat, Nat.mod_eq_of_lt h]

@[simp, bv_toNat]
theorem toNat_umod {x y : BitVec n} :
(x.umod y).toNat = x.toNat % y.toNat := rfl
(x % y).toNat = x.toNat % y.toNat := rfl

@[simp]
theorem umod_zero {x : BitVec n} : x.umod 0#n = x := by
simp [umod_eq]
theorem umod_zero {x : BitVec n} : x % 0#n = x := by
simp [umod_def]

/-! ### sdiv -/

Expand Down Expand Up @@ -2203,7 +2204,7 @@ protected theorem ne_of_lt {x y : BitVec n} : x < y → x ≠ y := by
simp only [lt_def, ne_eq, toNat_eq]
apply Nat.ne_of_lt

protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x.umod y < y := by
protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x % y < y := by
simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod, umod, toNat_ofNatLt]
apply Nat.mod_lt

Expand Down
Loading