From ca714fcf354a056dcd07288fea9c06b02a77ea73 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 19 Nov 2016 01:56:21 +0100
Subject: [PATCH] Show that the fraction of a mapsto is valid.

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

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 115ff663a..6343b8ee6 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -79,6 +79,12 @@ Section heap.
   Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v).
   Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
 
+  Lemma heap_mapsto_valid l q v : l ↦{q} v ⊢ ✓ q.
+  Proof.
+    rewrite heap_mapsto_eq /heap_mapsto_def auth_own_valid !discrete_valid.
+    by apply pure_mono=> /singleton_valid [??].
+  Qed.
+
   Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ∗ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
   Proof.
     by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
-- 
GitLab