slight refactor of read_write_bytes_different

leanprover · Oct 11, 2024 · f428b84 · f428b84
1 parent dcf0bce
commit f428b84
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/Arm/Memory/MemoryProofs.lean b/Arm/Memory/MemoryProofs.lean
@@ -55,19 +55,19 @@ theorem mem_separate_preserved_second_start_addr_add_one
   apply BitVec.val_nat_le 1 m 64 h0 (_ : 1 < 2^64) h1
   decide
 
+set_option maxHeartbeats 0 in
 theorem Memory.read_write_bytes_different
     (h : mem_separate addr1 addr1 addr2 (addr2 + (BitVec.ofNat 64 (n - 1)))) :
       read addr1 (write_bytes n addr2 v mem) = read addr1 mem := by
   induction n generalizing mem addr1 addr2
   case zero => simp only [write_bytes]
   case succ n ih =>
-    rw [write_bytes, ih ?h_sep]
-    case h_sep =>
-      show mem_separate addr1 addr1 (addr2 + 1#64)
-                        (addr2 + 1#64 + BitVec.ofNat 64 (n - 1)) = true
+    have h_sep : mem_separate addr1 addr1 (addr2 + 1#64)
+                        (addr2 + 1#64 + BitVec.ofNat 64 (n - 1)) := by
       sorry
-    rw [Memory.read_write_different]
-    sorry
+    have h_neq : addr1 ≠ addr2 :=
+      mem_separate_starting_addresses_neq h
+    rw [write_bytes, ih h_sep, Memory.read_write_different h_neq]
 
 theorem read_mem_of_write_mem_bytes_different (hn1 : n <= 2^64)
     (h : mem_separate addr1 addr1 addr2 (addr2 + (BitVec.ofNat 64 (n - 1)))) :