From 2241ea738d63072ca32b4f2bbc246e543bd65996 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Aug 2016 17:15:02 +0200
Subject: [PATCH] Better lemmas for splitting the fractional heap_mapsto.

---
 heap_lang/heap.v      | 13 +++++++++++--
 heap_lang/proofmode.v |  2 +-
 2 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 65de4c448..adbcaa676 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -144,8 +144,17 @@ Section heap.
     by apply pure_elim_r.
   Qed.
 
-  Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
-  Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
+  Lemma heap_mapsto_op_1 l q1 q2 v1 v2 :
+    l ↦{q1} v1 ★ l ↦{q2} v2 ⊢ v1 = v2 ∧ l ↦{q1+q2} v1.
+  Proof. by rewrite heap_mapsto_op. Qed.
+
+  Lemma heap_mapsto_op_half l q v1 v2 :
+    l ↦{q/2} v1 ★ l ↦{q/2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q} v1.
+  Proof. by rewrite heap_mapsto_op Qp_div_2. Qed.
+
+  Lemma heap_mapsto_op_half_1 l q v1 v2 :
+    l ↦{q/2} v1 ★ l ↦{q/2} v2 ⊢ v1 = v2 ∧ l ↦{q} v1.
+  Proof. by rewrite heap_mapsto_op_half. Qed.
 
   (** Weakest precondition *)
   (* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *)
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 68f480a12..1fbd36651 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -13,7 +13,7 @@ Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)).
 
 Global Instance into_sep_mapsto l q v :
   IntoSep false (l ↦{q} v) (l ↦{q/2} v) (l ↦{q/2} v).
-Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed.
+Proof. by rewrite /IntoSep heap_mapsto_op_eq Qp_div_2. Qed.
 
 Lemma tac_wp_alloc Δ Δ' E j e v Φ :
   to_val e = Some v →
-- 
GitLab