chore: show how to show equivalence between defns for add

opencompl · Jan 6, 2025 · b9b33c2 · b9b33c2
1 parent caa4016
commit b9b33c2
Showing 1 changed file with 19 additions and 0 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -3569,6 +3569,25 @@ instance instDecidableExistsBitVec :
 
 /-! ### Overflow Theorems -/
 
+theorem uaddOverflow_iff (x y : BitVec w) :
+    uaddOverflow x y ↔ (x.toNat + y.toNat ≥ 2^w) := by
+  simp [uaddOverflow, UnsignedOverflow]
+  have h : x.toNat + y.toNat < 2^ (w + 1) := by 
+    rw [Nat.pow_succ, Nat.mul_two]
+    apply Nat.add_lt_add  <;> omega
+  rw [Nat.mod_eq_of_lt h] 
+  constructor
+  · intros hmod 
+    apply Classical.byContradiction
+    intros hcontra
+    simp at hcontra
+    rw [Nat.mod_eq_of_lt hcontra] at hmod
+    simp at hmod
+  · intros h'
+    rw [Nat.mod_eq_sub_mod h']
+    rw [Nat.mod_eq_of_lt (by omega)]
+    omega
+
 -- theorem udiv_overflow (x y : BitVec w) : ¬ NatOverflows w (x.toNat / y.toNat) := by sorry
 
 /-! ### Deprecations -/