wip

src/Init/Data/BitVec/Lemmas.lean

@@ -566,6 +566,11 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   simp [h]
   omega
 
+@[simp] theorem not_not {x : BitVec w} :
+    ~~~ (~~~x) = x := by
+  ext
+  simp
+
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
@@ -744,63 +749,47 @@ private theorem Int.negSucc_emod (m : Nat) (n : Int) :
     if x.msb && i > n then
       x.toNat + (allOnes i).toNat - (allOnes n).toNat
     else
-      (zeroExtend i x).toNat := sorry
+      (zeroExtend i x).toNat := by
+  by_cases hmsb : i > n
+  · simp [hmsb]
+      norm_cast
+
+
+
+
+    sorry
+  · simp [hmsb]
+    simp only [signExtend]
+
+    simp [hmsb]
+    unfold BitVec.toInt
+    by_cases hh : 2 * x.toNat < 2 ^ n
+    · simp [hh]
+    · simp [hh]
+      norm_cast
+
+
+      sorry
+
 
 /-- To sign extend when the msb is false, then sign extension is the same as truncation -/
 theorem signExtend_eq_neg_truncate_neg_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
     (x.signExtend v) = x.truncate v := by
   rw [toNat_eq]
   rw [toNat_signExtend]
-  simp [hmsb]
+  simp only [hmsb, gt_iff_lt, Bool.false_and, Bool.false_eq_true, ↓reduceIte, toNat_truncate]
 
-theorem signExtend_eq_neg_truncate_neg_of_msb_true' {x : BitVec w} {v : Nat} (hmsb : x.msb = true) :
-    (x.signExtend v) = ~~~((~~~x).truncate v) := by
-  rw [toNat_eq]
-  simp only [toNat_not]
-  simp only [toNat_truncate]
-  simp only [toNat_not]
-  rw [toNat_signExtend]
-  simp [hmsb]
-  by_cases hv : w < v
-  · simp [hv]
-    sorry
-  · simp [hv]
-    sorry
-
---  simp
---  intros
---rw [toNat_truncate]
-
---  by_cases hv : i < v
---  · simp only [getLsb_zeroExtend, hv, decide_True, Bool.true_and]
---    rw [signExtend, getLsb]
---    simp only [toNat_ofInt]
---    rw [BitVec.toInt_eq_msb_cond]
---    simp only [hmsb, Bool.false_eq_true, ↓reduceIte]
---    rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat]
---    simp only [Nat.testBit_mod_two_pow, hv, decide_True, Bool.true_and]
---    rw [BitVec.testBit_toNat]
---  · simp only [getLsb_zeroExtend, hv, decide_False, Bool.false_and]
---    apply getLsb_ge
---    omega
-
-/-- To sign extend when the msb is true, we perform double negation to make the high bits true. -/
 theorem signExtend_eq_neg_truncate_neg_of_msb_true {x : BitVec w} {v : Nat} (hmsb : x.msb = true) :
     (x.signExtend v) = ~~~((~~~x).truncate v) := by
-  apply BitVec.eq_of_toNat_eq
-  simp only [signExtend, BitVec.toInt_eq_msb_cond, toNat_ofInt, toNat_not,
-    toNat_truncate, hmsb, ↓reduceIte]
-  norm_cast
-  rw [Int.toNat_sub_toNat_eq_negSucc_ofLt, Int.negSucc_emod]
-  simp only [Int.natAbs_ofNat, Nat.succ_eq_add_one]
-  rw [Int.subNatNat_of_le]
-  · rw [Int.toNat_ofNat, Nat.add_comm, Nat.sub_add_eq]
-  · apply Nat.le_trans
-    · apply Nat.succ_le_of_lt
-      apply Nat.mod_lt
-      apply Nat.two_pow_pos
-    · apply Nat.le_refl
-  · omega
+  by_cases hv : w < v
+  · rw [toNat_eq, toNat_signExtend]
+    simp only [hmsb, gt_iff_lt, hv, decide_True, Bool.and_self, ↓reduceIte, toNat_allOnes,
+      toNat_not, toNat_truncate]
+    rw [Nat.mod_eq_of_lt (by have hh := Nat.pow_lt_pow_of_lt (a := 2) (by omega) hv; omega)]
+    omega
+  · rw [truncate_not (by omega)]
+    simp [toNat_eq, toNat_signExtend, hmsb]
+    omega
 
 @[simp] theorem getLsb_signExtend (x  : BitVec w) {v i : Nat} :
     (x.signExtend v).getLsb i = (decide (i < v) && if i < w then x.getLsb i else x.msb) := by