From cb600ed9b436e4290b819b0529f8454490bffeb6 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 3 Dec 2024 15:50:14 +1100
Subject: [PATCH] chore: restore broken proofs

This reverts commit d099f560f72b5f18695c7fb586a9da93af0cb17e.
---
 src/Init/Data/BitVec/Lemmas.lean      | 65 ++++++++++++---------------
 src/Init/Data/Int/Bitwise/Lemmas.lean | 11 +++--
 src/Init/Data/Int/Pow.lean            |  7 ++-
 3 files changed, 37 insertions(+), 46 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 8f05d13f93..f1f5e2db3f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -308,8 +308,7 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 
 @[simp] theorem toNat_mod_cancel' {x : BitVec n} :
     (x.toNat : Int) % (((2 ^ n) : Nat) : Int) = x.toNat := by
-  sorry -- FIXME #6278
-  -- rw_mod_cast [toNat_mod_cancel]
+  rw_mod_cast [toNat_mod_cancel]
 
 @[simp] theorem sub_toNat_mod_cancel {x : BitVec w} (h : ¬ x = 0#w) :
     (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat := by
@@ -787,10 +786,9 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 
 @[simp] theorem toInt_or (x y : BitVec w) :
     BitVec.toInt (x ||| y) = Int.bmod (BitVec.toNat x ||| BitVec.toNat y) (2^w) := by
-  sorry -- FIXME #6278
-  -- rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_or, Nat.mod_eq_of_lt
-  --   (Nat.or_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))]
-  -- omega
+  rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_or, Nat.mod_eq_of_lt
+    (Nat.or_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))]
+  omega
 
 @[simp] theorem toFin_or (x y : BitVec v) :
     BitVec.toFin (x ||| y) = BitVec.toFin x ||| BitVec.toFin y := by
@@ -861,10 +859,9 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
 
 @[simp] theorem toInt_and (x y : BitVec w) :
     BitVec.toInt (x &&& y) = Int.bmod (BitVec.toNat x &&& BitVec.toNat y) (2^w) := by
-  sorry -- FIXME #6278
-  -- rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_and, Nat.mod_eq_of_lt
-  --   (Nat.and_lt_two_pow x.toNat (BitVec.isLt y))]
-  -- omega
+  rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_and, Nat.mod_eq_of_lt
+    (Nat.and_lt_two_pow x.toNat (BitVec.isLt y))]
+  omega
 
 @[simp] theorem toFin_and (x y : BitVec v) :
     BitVec.toFin (x &&& y) = BitVec.toFin x &&& BitVec.toFin y := by
@@ -935,10 +932,9 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) wher
 
 @[simp] theorem toInt_xor (x y : BitVec w) :
     BitVec.toInt (x ^^^ y) = Int.bmod (BitVec.toNat x ^^^ BitVec.toNat y) (2^w) := by
-  sorry -- FIXME #6278
-  -- rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_xor, Nat.mod_eq_of_lt
-  --   (Nat.xor_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))]
-  -- omega
+  rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_xor, Nat.mod_eq_of_lt
+    (Nat.xor_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))]
+  omega
 
 @[simp] theorem toFin_xor (x y : BitVec v) :
     BitVec.toFin (x ^^^ y) = BitVec.toFin x ^^^ BitVec.toFin y := by
@@ -1019,11 +1015,10 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
 
 @[simp] theorem toInt_not {x : BitVec w} :
     (~~~x).toInt = Int.bmod (2^w - 1 - x.toNat) (2^w) := by
-  sorry -- FIXME #6278
-  -- rw_mod_cast [BitVec.toInt, BitVec.toNat_not, Int.bmod_def]
-  -- simp [show ((2^w : Nat) : Int) - 1 - x.toNat = ((2^w - 1 - x.toNat) : Nat) by omega]
-  -- rw_mod_cast [Nat.mod_eq_of_lt (by omega)]
-  -- omega
+  rw_mod_cast [BitVec.toInt, BitVec.toNat_not, Int.bmod_def]
+  simp [show ((2^w : Nat) : Int) - 1 - x.toNat = ((2^w - 1 - x.toNat) : Nat) by omega]
+  rw_mod_cast [Nat.mod_eq_of_lt (by omega)]
+  omega
 
 @[simp] theorem ofInt_negSucc_eq_not_ofNat {w n : Nat} :
     BitVec.ofInt w (Int.negSucc n) = ~~~.ofNat w n := by
@@ -1587,18 +1582,17 @@ theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hms
   apply BitVec.eq_of_toNat_eq
   simp only [signExtend, BitVec.toInt_eq_msb_cond, toNat_ofInt, toNat_not,
     toNat_setWidth, hmsb, ↓reduceIte]
-  sorry -- FIXME #6278
-  -- norm_cast
-  -- rw [Int.ofNat_sub_ofNat_of_lt, 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
+  norm_cast
+  rw [Int.ofNat_sub_ofNat_of_lt, 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
 
 theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
     (x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb) := by
@@ -1676,11 +1670,10 @@ theorem toInt_signExtend_of_lt {x : BitVec w} (hv : w < v):
     simp [getElem_signExtend, Nat.le_sub_one_of_lt hv]
   have H : 2^w ≤ 2^v := Nat.pow_le_pow_of_le_right (by omega) (by omega)
   simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul]
-  sorry -- FIXME #6278
-  -- by_cases h : x.msb
-  -- <;> norm_cast
-  -- <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)]
-  -- omega
+  by_cases h : x.msb
+  <;> norm_cast
+  <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)]
+  omega
 
 /-
 If the current width `w` is larger than the extended width `v`,
diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean
index ecff751c14..d2741d67f0 100644
--- a/src/Init/Data/Int/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Int/Bitwise/Lemmas.lean
@@ -24,12 +24,11 @@ theorem shiftRight_add (i : Int) (m n : Nat) :
 
 theorem shiftRight_eq_div_pow (m : Int) (n : Nat) :
     m >>> n = m / ((2 ^ n) : Nat) := by
-  sorry -- FIXME #6278
-  -- simp only [shiftRight_eq, Int.shiftRight, Nat.shiftRight_eq_div_pow]
-  -- split
-  -- · simp
-  -- · rw [negSucc_ediv _ (by norm_cast; exact Nat.pow_pos (Nat.zero_lt_two))]
-  --   rfl
+  simp only [shiftRight_eq, Int.shiftRight, Nat.shiftRight_eq_div_pow]
+  split
+  · simp
+  · rw [negSucc_ediv _ (by norm_cast; exact Nat.pow_pos (Nat.zero_lt_two))]
+    rfl
 
 @[simp]
 theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by
diff --git a/src/Init/Data/Int/Pow.lean b/src/Init/Data/Int/Pow.lean
index d617999ca1..233849788b 100644
--- a/src/Init/Data/Int/Pow.lean
+++ b/src/Init/Data/Int/Pow.lean
@@ -52,9 +52,8 @@ protected theorem two_pow_pred_sub_two_pow {w : Nat} (h : 0 < w) :
 @[simp]
 protected theorem two_pow_pred_sub_two_pow' {w : Nat} (h : 0 < w) :
     (2 : Int) ^ (w - 1) - (2 : Int) ^ w = - (2 : Int) ^ (w - 1) := by
-  sorry -- FIXME #6278
-  -- norm_cast
-  -- rw [← Nat.two_pow_pred_add_two_pow_pred h]
-  -- simp [h]
+  norm_cast
+  rw [← Nat.two_pow_pred_add_two_pow_pred h]
+  simp [h]
 
 end Int