chore: getLsb_replicate proof

opencompl · Jul 23, 2024 · 30b1b75 · 30b1b75
1 parent 8f9f259
commit 30b1b75
Showing 1 changed file with 8 additions and 5 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -1525,18 +1525,21 @@ theorem getLsb_replicate {n w : Nat} (x : BitVec w) :
     simp only [getLsb_cast, getLsb_append]
     by_cases hi : i < w * n
     · simp [hi, ih]
-      intros h
+      intros _
       rw [Nat.mul_succ]
       omega
     · simp [hi, ih]
       by_cases hi' : i < w * (n + 1)
       · simp [hi']
         congr
         rw [Nat.sub_eq_of_eq_add]
-        have hi : w = (i / n) := sorry
-        -- TODO: rewrite, and then use
-        -- rw [Nat.div_add_mod]
-        sorry
+        have hi : i / w = n := by
+          apply Nat.div_eq_of_lt_le (m := i) (k := n)
+            (by simp at hi; rw[Nat.mul_comm]; assumption)
+            (by rw [Nat.mul_comm]; assumption)
+        rw [← hi]
+        rw [Nat.add_comm]
+        rw [Nat.div_add_mod]
       · simp [hi']
         apply getLsb_ge
         apply Nat.le_sub_of_add_le