@@ -66,7 +66,7 @@ namespace BVLems
6666 have hle := of_decide_eq_true hdec
6767 rw [Bool.dite_eq_true (proof:=hle), toNat_zeroExtend']
6868 rw [Nat.mod_eq_of_lt]; rcases a with ⟨⟨a, isLt⟩⟩;
69- apply Nat.le_trans isLt; apply Nat.pow_le_pow_right (Nat.le_step .refl) hle
69+ apply Nat.le_trans isLt; apply Nat.pow_le_pow_right (Nat.lt_succ_of_lt .refl) hle
7070
7171 theorem toNat_sub (a b : BitVec n) : (a - b).toNat = (2 ^ n - b.toNat + a.toNat) % (2 ^ n) := rfl
7272
@@ -93,55 +93,32 @@ namespace BVLems
9393 theorem ushiftRight_ge_length_eq_zero (a : BitVec n) (i : Nat) : i ≥ n → a >>> i = 0 #n := by
9494 intro h; apply eq_of_val_eq; rw [toNat_ushiftRight, toNat_ofNat]
9595 apply (Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)).mpr
96- apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (.step .refl) h)
97-
98- theorem ushiftRight_ge_length_eq_zero' (a : BitVec n) (i : Nat) : i ≥ n → BitVec.ofNat n (a.toNat >>> i) = 0 #n := by
99- intro h; apply congrArg (@BitVec.ofNat n)
100- rw [Nat.shiftRight_eq_div_pow, Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)]
101- apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (.step .refl) h)
102-
103- theorem msb_equiv_lt (a : BitVec n) : !a.msb ↔ a.toNat < 2 ^ (n - 1 ) := by
104- dsimp [BitVec.msb, BitVec.getMsbD, BitVec.getLsbD]
105- cases n
106- case zero => cases a <;> simp
107- case succ n =>
108- have dtrue : decide (0 < n + 1 ) = true := by simp
109- rw [dtrue, Bool.not_eq_true', Bool.true_and, Nat.succ_sub_one, Nat.testBit_false_iff]
110- rw [Nat.mod_eq_of_lt (toNat_le _)]
111-
112- theorem msb_equiv_lt' (a : BitVec n) : !a.msb ↔ 2 * a.toNat < 2 ^ n := by
113- rw [msb_equiv_lt]
114- cases n
115- case zero => cases a <;> simp
116- case succ n =>
117- rw [Nat.succ_sub_one, Nat.pow_succ, Nat.mul_comm (m:=2 )]
118- apply Iff.symm; apply Nat.mul_lt_mul_left
119- exact .step .refl
96+ apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (Nat.lt_succ_of_lt .refl) h)
12097
12198 theorem sshiftRight_ge_length_eq_msb (a : BitVec n) (i : Nat) : i ≥ n → a.sshiftRight i =
12299 if a.msb then (1 #n).neg else 0 #n := by
123- intro h; simp only [sshiftRight, BitVec.toInt, ← msb_equiv_lt']
124- cases hmsb : a.msb <;> simp only [Int.shiftRight_def] <;> dsimp
100+ intro h
101+ cases hmsb : a.msb <;> dsimp <;> rw [eq_iff_val_eq]
125102 case false =>
126- rw [BitVec.ofNat]
127- apply ushiftRight_ge_length_eq_zero'; exact h
103+ rw [BitVec.sshiftRight_eq_of_msb_false hmsb]
104+ have ha : a.toNat < 2 ^ i := Nat.le_trans (toNat_le _) (
105+ Nat.pow_le_pow_right Nat.zero_lt_two h)
106+ simp [Nat.shiftRight_eq_div_pow, ha]
128107 case true =>
129- rw [← Int.subNatNat_eq_coe, Int.subNatNat_of_lt (toNat_le _)]
130- simp only [BitVec.ofInt]; dsimp
131- have hzero : (2 ^ n - BitVec.toNat a - 1 ) >>> i = 0 := by
132- rw [Nat.shiftRight_eq_div_pow]; apply (Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)).mpr
133- rw [Nat.sub_one, Nat.pred_lt_iff_le (Nat.two_pow_pos _)]
134- apply Nat.le_trans (Nat.sub_le _ _) (Nat.pow_le_pow_right (.step .refl) h)
135- apply eq_of_val_eq; rw [toNat_ofNatLt, hzero]
136- rw [toNat_neg, Int.mod_def', Int.emod]
137- rw [Nat.zero_mod, Int.natAbs_natCast, Nat.succ_eq_add_one, Nat.zero_add]
138- rw [Int.subNatNat_of_sub_eq_zero ((Nat.sub_eq_zero_iff_le).mpr (Nat.two_pow_pos _))]
139- rw [Int.toNat_natCast, BitVec.toNat_ofNat]
140- cases n <;> try rfl
141- case succ n =>
142- have hlt : 2 ≤ 2 ^ Nat.succ n := @Nat.pow_le_pow_right 2 (.step .refl) 1 (.succ n) (Nat.succ_le_succ (Nat.zero_le _))
143- rw [Nat.mod_eq_of_lt (a:=1 ) hlt]
144- rw [Nat.mod_eq_of_lt]; apply Nat.sub_lt (Nat.le_trans (.step .refl) hlt) .refl
108+ have hn : n > 0 := by
109+ apply Nat.ne_zero_iff_zero_lt.mp; intro hn; cases hn
110+ rw [BitVec.msb_eq_toNat] at hmsb
111+ have := toNat_le a; simp_all
112+ have hpn : 2 ^ n > 1 := Nat.pow_le_pow_right Nat.zero_lt_two hn
113+ have hin : 2 ^ n ≤ 2 ^ i := Nat.pow_le_pow_right Nat.zero_lt_two h
114+ rw [BitVec.sshiftRight_eq_of_msb_true hmsb]
115+ rw [BitVec.toNat_not, BitVec.toNat_neg, BitVec.toNat_ofNat]
116+ rw [Nat.one_mod_eq_one.mpr (Nat.ne_of_gt hpn)]
117+ have hsa : 2 ^ n - 1 - a.toNat < 2 ^ i := by
118+ apply Nat.sub_lt_of_lt; apply Nat.lt_iff_add_one_le.mpr
119+ rw [Nat.sub_add_cancel (Nat.le_of_lt hpn)]; exact hin
120+ have han : (~~~a >>> i).toNat = 0 := by simp [Nat.shiftRight_eq_div_pow, hsa]
121+ simp [han]
145122
146123 theorem shiftRight_eq_zero_iff (a : BitVec n) (b : Nat) : a >>> b = 0 #n ↔ a.toNat < 2 ^ b := by
147124 rw [ushiftRight_def]; rcases a with ⟨⟨a, isLt⟩⟩;
@@ -201,7 +178,7 @@ namespace BVLems
201178
202179 theorem shl_toNat_equiv_short (a : BitVec n) (b : BitVec m) (h : m ≤ n) : a <<< b.toNat = a <<< (zeroExtend n b) := by
203180 apply eq_of_val_eq; rw [toNat_shiftLeft, smtshiftLeft_def, toNat_shiftLeft, toNat_zeroExtend, Nat.mod_eq_of_lt (a:=BitVec.toNat b)]
204- apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (.step .refl) h)
181+ apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (Nat.lt_succ_of_lt .refl) h)
205182
206183 theorem shl_toNat_equiv_long (a : BitVec n) (b : BitVec m) (h : m > n) : a <<< b.toNat =
207184 if (b >>> (BitVec.ofNat m n)) = 0 #m then a <<< (zeroExtend n b) else 0 := by
@@ -244,7 +221,7 @@ namespace BVLems
244221
245222 theorem lshr_toNat_equiv_short (a : BitVec n) (b : BitVec m) (h : m ≤ n) : a >>> b.toNat = a >>> (zeroExtend n b) := by
246223 apply eq_of_val_eq; rw [toNat_ushiftRight, smtushiftRight_def, toNat_ushiftRight, toNat_zeroExtend, Nat.mod_eq_of_lt]
247- apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (.step .refl) h)
224+ apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (Nat.lt_succ_of_lt .refl) h)
248225
249226 theorem lshr_toNat_equiv_long (a : BitVec n) (b : BitVec m) (h : m > n) : a >>> b.toNat =
250227 if (b >>> (BitVec.ofNat m n)) = 0 #m then a >>> (zeroExtend n b) else 0 := by
@@ -289,7 +266,7 @@ namespace BVLems
289266
290267 theorem ashr_toNat_equiv_short (a : BitVec n) (b : BitVec m) (h : m ≤ n) : a.sshiftRight b.toNat = a.sshiftRight (zeroExtend n b).toNat := by
291268 apply eq_of_val_eq; rw [toNat_zeroExtend, Nat.mod_eq_of_lt]
292- apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (.step .refl) h)
269+ apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (Nat.lt_succ_of_lt .refl) h)
293270
294271 theorem ashr_toNat_equiv_long (a : BitVec n) (b : BitVec m) (h : m > n) : a.sshiftRight b.toNat =
295272 if (b >>> (BitVec.ofNat m n)) = 0 #m then a.sshiftRight (zeroExtend n b).toNat else (if a.msb then (1 #n).neg else 0 #n) := by
0 commit comments