Skip to content

Commit

Permalink
chore: restore broken proofs
Browse files Browse the repository at this point in the history 
This reverts commit d099f560f72b5f18695c7fb586a9da93af0cb17e.
  • Loading branch information
@kim-em
kim-em committed Dec 3, 2024
1 parent 57d83c8 commit cb600ed
Show file tree
Hide file tree
Showing 3 changed files with 37 additions and 46 deletions.
65 changes: 29 additions & 36 deletions src/Init/Data/BitVec/Lemmas.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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`,
Expand Down
11 changes: 5 additions & 6 deletions src/Init/Data/Int/Bitwise/Lemmas.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
7 changes: 3 additions & 4 deletions src/Init/Data/Int/Pow.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit cb600ed

Please sign in to comment.