addressed comments

leanprover · Oct 7, 2024 · 5da12c5 · 5da12c5
1 parent 61024eb
commit 5da12c5
Showing 1 changed file with 3 additions and 7 deletions.
diff --git a/Proofs/SHA512/SHA512_block_armv8_rules.lean b/Proofs/SHA512/SHA512_block_armv8_rules.lean
@@ -138,21 +138,17 @@ theorem truncate_of_concat_is_lsb_64 (x y : BitVec 64) :
   BitVec.zeroExtend 64 (x ++ y) = y := by
   bv_check "lrat_files/Sha512_block_armv8_rules.lean-truncate_of_concat_is_lsb_64-106-2.lrat"
 
-theorem truncate_of_concat_is_lsb (w : Nat) (x y : BitVec w) :
+theorem zeroExtend_append_eq (w : Nat) (x y : BitVec w) :
   BitVec.zeroExtend w (x ++ y) = y := by
   ext
-  simp [BitVec.leftshift_n_or_mod_2n]
+  simp only [truncate_append, Nat.le_refl, ↓reduceDIte, zeroExtend_eq]
 
+-- use BitVec.zeroExtend_zeroExtend_of_le for arbitrary-length bitvec
 theorem zeroextend_bigger_smaller_64 (x : BitVec 64) :
   BitVec.zeroExtend 64 (BitVec.zeroExtend 128 x) =
   BitVec.zeroExtend 64 x := by
   bv_omega
 
-theorem zeroextend_bigger_smaller (w : Nat) (x : BitVec w) :
-  BitVec.zeroExtend w (BitVec.zeroExtend (w + w) x) =
-  BitVec.zeroExtend w x := by
-  simp
-
 -- (FIXME) Generalize to arbitrary-length bitvecs.
 theorem rsh_concat_identity_128 (x : BitVec 128) :
   zeroExtend 64 (x >>> 64) ++ zeroExtend 64 x = x := by