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

This follows the norm for all other Bitvector operations, and makes the symbolic version the simp normal form. I would imagine that @hargoniX would prefer that this be merged after #5628, so as to prevent churn for his PR. I'm happy to rebase the PR.
leanprover · Oct 8, 2024 · f1b996e · f1b996e
1 parent 3e75d8f
commit f1b996e
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 12 deletions.
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
@@ -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
 

diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -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
@@ -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
@@ -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 *
@@ -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
@@ -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 ..)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -1339,13 +1339,14 @@ 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]
@@ -1358,14 +1359,15 @@ theorem udiv_zero {x : BitVec n} : x.udiv 0#n = 0#n := by
 
 /-! ### 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