chore: fixup changes

leanprover · Nov 1, 2024 · 34400ea · 34400ea
1 parent fc87ccd
commit 34400ea
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 14 deletions.
diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
@@ -28,9 +28,6 @@ instance : Ord (BitVec n) where
   -- Unsigned comparison
   compare := unsigned_compare
 
-instance {w} : Hashable (BitVec w) where
-  hash x := hash x.toNat
-
 -- Adding some useful simp lemmas to `bitvec_rules`: we do not include
 -- `bv_toNat` lemmas here.
 -- See Init.Data.BitVec.Lemmas.
@@ -893,14 +890,6 @@ theorem add_sub_cancel_left {a b : BitVec w₁}
   · apply BitVec.le_add_self_of_lt
     omega
 
-theorem le_add_iff_sub_le {a b c : BitVec w₁}
-   (hac : c ≤ a) (hbc : b.toNat + c.toNat < 2^w₁) :
-    (a ≤ b + c) ↔ (a - c ≤ b) := by
-  simp_all only [BitVec.le_def]
-  rw [BitVec.toNat_sub_eq_toNat_sub_toNat_of_le (by rw [BitVec.le_def]; omega)]
-  rw [BitVec.toNat_add_eq_toNat_add_toNat (by omega)]
-  omega
-
 theorem sub_le_sub_iff_right (a b c : BitVec w₁) (hac : c ≤ a)
     (hbc : c ≤ b) : (a - c ≤ b - c) ↔ a ≤ b := by
   simp_all only [BitVec.le_def]

diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
@@ -720,7 +720,7 @@ theorem shift_right_common_aux_64_2_tff (operand : BitVec 128)
              reduceAllOnes,
              reduceZeroExtend,
              Nat.zero_mul,
-             shiftLeft_zero_eq,
+             shiftLeft_zero,
              reduceNot,
              BitVec.extractLsb_ofNat,
              Nat.reducePow,

diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean
@@ -121,7 +121,7 @@ def exec_advanced_simd_three_same
 
 theorem pc_of_exec_advanced_simd_three_same
   (h_step : s' = exec_advanced_simd_three_same inst s)
-  (h_no_err: read_err s' = None) :
+  (_h_no_err: read_err s' = None) :
   r StateField.PC s' =
   -- (r StateField.PC s) + 4#64 -- TODO: How do I use + here?
   (BitVec.add (r StateField.PC s) 4#64) := by

diff --git a/Specs/GCM.lean b/Specs/GCM.lean
@@ -104,7 +104,7 @@ protected def initialize_J0 (H : BitVec 128) (IV : BitVec lv) :=
   if h₀ : lv == 96
   then have h₁ : lv + 31 + 1 = 128 := by
          simp only [Nat.succ.injEq]
-         exact Nat.eq_of_beq_eq_true h₀
+         simpa using h₀
        BitVec.cast h₁ (IV ++ BitVec.zero 31 ++ 0b1#1)
   else let s := GCM.ceiling_in_bits lv - lv
        have h₂ : 128 ∣ (lv + (s + 64) + 64) := by