slight refactor of read_write_bytes_different

leanprover · Oct 11, 2024 · a221670 · a221670
1 parent dcf0bce
commit a221670
Showing 1 changed file with 5 additions and 6 deletions.
diff --git a/Arm/Memory/MemoryProofs.lean b/Arm/Memory/MemoryProofs.lean
@@ -61,13 +61,12 @@ theorem Memory.read_write_bytes_different
   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)))) :