From e3c01577cf3ec57842eea2b197f6ec440be3c5cd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 27 Feb 2016 09:51:49 +0100
Subject: [PATCH] prove a lemma for splitting \mapsto

---
 heap_lang/heap.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index b6d415b14..a2235f1a6 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -132,6 +132,10 @@ Section heap.
     rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
   Qed.
 
+  Lemma heap_mapsto_op_split l q v :
+    (l ↦{q} v)%I ≡ (l ↦{q/2} v ★ l ↦{q/2} v)%I.
+  Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
+
   (** Weakest precondition *)
   Lemma wp_alloc N E e v P Φ :
     to_val e = Some v →
-- 
GitLab