[Merged by Bors] - feat: show that BitVec is a commutative ring

Mathlib/Data/BitVec/Defs.lean

@@ -140,4 +140,10 @@ def toLEList (x : BitVec w) : List Bool :=
 def toBEList (x : BitVec w) : List Bool :=
   List.ofFn x.getMsb'
 
+instance : SMul ℕ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩
+instance : SMul ℤ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩
+instance : Pow (BitVec w) ℕ  := ⟨fun x n => ofFin <| x.toFin ^ n⟩
+instance : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
+instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩
+
 end Std.BitVec

Mathlib/Data/BitVec/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Simon Hudon, Harun Khan
 -/
 
 import Mathlib.Data.BitVec.Defs
+import Mathlib.Tactic.Linarith
 
 /-!
 # Basic Theorems About Bitvectors
@@ -21,9 +22,15 @@ open Nat
 
 variable {w v : Nat}
 
-theorem toNat_injective {n : Nat} : Function.Injective (@Std.BitVec.toNat n)
+theorem toFin_injective {n : Nat} : Function.Injective (toFin : BitVec n → _)
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
+theorem toFin_inj {x y : BitVec w} : x.toFin = y.toFin ↔ x = y :=
+  toFin_injective.eq_iff
+
+theorem toNat_injective {n : Nat} : Function.Injective (BitVec.toNat : BitVec n → _) :=
+  Fin.val_injective.comp toFin_injective
+
 theorem toNat_inj {x y : BitVec w} : x.toNat = y.toNat ↔ x = y :=
   toNat_injective.eq_iff
 
@@ -105,4 +112,111 @@ theorem ofFin_toFin {n} (v : BitVec n) : ofFin (toFin v) = v := by
   rfl
 #align bitvec.of_fin_to_fin Std.BitVec.ofFin_toFin
 
+/-!
+### Distributivity of `Std.BitVec.ofFin`
+-/
+section
+variable (x y : Fin (2^w))
+
+@[simp] lemma ofFin_neg : ofFin (-x) = -(ofFin x) := by
+  rw [neg_eq_zero_sub]; rfl
+
+@[simp] lemma ofFin_and : ofFin (x &&& y) = ofFin x &&& ofFin y := by
+  simp only [HAnd.hAnd, AndOp.and, Fin.land, BitVec.and, toNat_ofFin, ofFin.injEq, Fin.mk.injEq]
+  exact mod_eq_of_lt (Nat.and_lt_two_pow _ y.prop)
+
+@[simp] lemma ofFin_or  : ofFin (x ||| y) = ofFin x ||| ofFin y := by
+  simp only [HOr.hOr, OrOp.or, Fin.lor, BitVec.or, toNat_ofFin, ofFin.injEq, Fin.mk.injEq]
+  exact mod_eq_of_lt (Nat.or_lt_two_pow x.prop y.prop)
+
+@[simp] lemma ofFin_xor : ofFin (x ^^^ y) = ofFin x ^^^ ofFin y := by
+  simp only [HXor.hXor, Xor.xor, Fin.xor, BitVec.xor, toNat_ofFin, ofFin.injEq, Fin.mk.injEq]
+  exact mod_eq_of_lt (Nat.xor_lt_two_pow x.prop y.prop)
+
+@[simp] lemma ofFin_add : ofFin (x + y)   = ofFin x + ofFin y   := rfl
+@[simp] lemma ofFin_sub : ofFin (x - y)   = ofFin x - ofFin y   := rfl
+@[simp] lemma ofFin_mul : ofFin (x * y)   = ofFin x * ofFin y   := rfl
+
+-- These should be simp, but Std's simp-lemmas do not allow this yet.
+lemma ofFin_zero : ofFin (0 : Fin (2^w)) = 0 := rfl
+lemma ofFin_one  : ofFin (1 : Fin (2^w)) = 1 := by
+  simp only [OfNat.ofNat, BitVec.ofNat, and_pow_two_is_mod]
+  rfl
+
+lemma ofFin_nsmul (n : ℕ) (x : Fin (2^w)) : ofFin (n • x) = n • ofFin x := rfl
+lemma ofFin_zsmul (z : ℤ) (x : Fin (2^w)) : ofFin (z • x) = z • ofFin x := rfl
+@[simp] lemma ofFin_pow (n : ℕ) : ofFin (x ^ n) = ofFin x ^ n := rfl
+
+@[simp] lemma ofFin_natCast (n : ℕ) : ofFin (n : Fin (2^w)) = n := by
+  simp only [Nat.cast, NatCast.natCast, OfNat.ofNat, BitVec.ofNat, and_pow_two_is_mod]
+  rfl
+
+-- See Note [no_index around OfNat.ofNat]
+@[simp] lemma ofFin_ofNat (n : ℕ) :
+    ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by
+  simp only [OfNat.ofNat, Fin.ofNat', BitVec.ofNat, and_pow_two_is_mod]
+
+end
+
+/-!
+### Distributivity of `Std.BitVec.toFin`
+-/
+section
+variable (x y : BitVec w)
+
+@[simp] lemma toFin_neg : toFin (-x) = -(toFin x) := by
+  rw [neg_eq_zero_sub]; rfl
+
+@[simp] lemma toFin_and : toFin (x &&& y) = toFin x &&& toFin y := by
+  apply toFin_inj.mpr; simp only [ofFin_and]
+
+@[simp] lemma toFin_or  : toFin (x ||| y) = toFin x ||| toFin y := by
+  apply toFin_inj.mpr; simp only [ofFin_or]
+
+@[simp] lemma toFin_xor : toFin (x ^^^ y) = toFin x ^^^ toFin y := by
+  apply toFin_inj.mpr; simp only [ofFin_xor]
+
+@[simp] lemma toFin_add : toFin (x + y)   = toFin x + toFin y   := rfl
+@[simp] lemma toFin_sub : toFin (x - y)   = toFin x - toFin y   := rfl
+@[simp] lemma toFin_mul : toFin (x * y)   = toFin x * toFin y   := rfl
+
+-- These should be simp, but Std's simp-lemmas do not allow this yet.
+lemma toFin_zero : toFin (0 : BitVec w) = 0 := rfl
+lemma toFin_one  : toFin (1 : BitVec w) = 1 := by
+  apply toFin_inj.mpr; simp only [ofNat_eq_ofNat, ofFin_ofNat]
+
+lemma toFin_nsmul (n : ℕ) (x : BitVec w) : toFin (n • x) = n • x.toFin := rfl
+lemma toFin_zsmul (z : ℤ) (x : BitVec w) : toFin (z • x) = z • x.toFin := rfl
+@[simp] lemma toFin_pow (n : ℕ) : toFin (x ^ n) = x.toFin ^ n := rfl
+
+@[simp] lemma toFin_natCast (n : ℕ) : toFin (n : BitVec w) = n := by
+  apply toFin_inj.mpr; simp only [ofFin_natCast]
+
+-- See Note [no_index around OfNat.ofNat]
+lemma toFin_ofNat (n : ℕ) :
+    toFin (no_index (OfNat.ofNat n : BitVec w)) = OfNat.ofNat n := by
+  simp only [OfNat.ofNat, BitVec.ofNat, and_pow_two_is_mod, Fin.ofNat']
+
+end
+
+/-!
+### `IntCast`
+-/
+
+-- Either of these follows trivially fromt he other. Which one to
+-- prove is not yet clear.
+proof_wanted ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z
+
+proof_wanted toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z
+
+/-!
+## Ring
+-/
+
+-- TODO: generalize to `CommRing` after `ofFin_intCast` is proven
+instance : CommSemiring (BitVec w) :=
+  toFin_injective.commSemiring _
+    toFin_zero toFin_one toFin_add toFin_mul (Function.swap toFin_nsmul)
+    toFin_pow toFin_natCast
+
 end Std.BitVec

Mathlib/Data/Nat/Order/Lemmas.lean

@@ -254,4 +254,29 @@ theorem div_lt_div_of_lt_of_dvd {a b d : ℕ} (hdb : d ∣ b) (h : a < b) : a /
   exact lt_of_le_of_lt (mul_div_le a d) h
 #align nat.div_lt_div_of_lt_of_dvd Nat.div_lt_div_of_lt_of_dvd
 
+theorem sub_succ_mod {m : ℕ} (m_pos : m > 0) (y : ℕ) :
+    (m - (y + 1) % m) % m = (m - 1 - y % m) % m := by
+  induction' y using Nat.strongInductionOn with y ih
+  by_cases h : y + 1 < m
+  · rw [Nat.mod_eq_of_lt h, Nat.mod_eq_of_lt (lt_of_succ_lt h), Nat.sub_succ', Nat.sub_right_comm]
+  · by_cases h' : y + 1 = m
+    · simp only [h', mod_self, ge_iff_le, nonpos_iff_eq_zero, tsub_zero, tsub_le_iff_right]
+      obtain rfl : y = m - 1 := by
+        apply Nat.succ_injective
+        show y + 1 = _ + 1
+        rw [h', Nat.sub_add_cancel m_pos]
+      have m_pred_lt : m - 1 < m := Nat.sub_one_lt_of_le m_pos Nat.le.refl
+      simp only [ge_iff_le, Nat.mod_eq_of_lt m_pred_lt, le_refl, tsub_eq_zero_of_le, zero_mod]
+    · have y_ge : y ≥ m := by
+        simp only [not_lt] at h
+        cases h
+        · contradiction
+        · assumption
+      rw [
+        Nat.mod_eq_sub_mod (Nat.ge_of_not_lt h),
+        Nat.mod_eq_sub_mod y_ge,
+        Nat.succ_sub y_ge
+      ]
+      apply ih _ (Nat.sub_lt (lt_of_lt_of_le m_pos y_ge) m_pos)
+
 end Nat