From 730a39a3512f042f7369149b071f0d91cfc44f3a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2016 20:37:47 +0100
Subject: [PATCH] barrier: change invariant such that the mapsto can be
 obtained without case distinction

---
 barrier/barrier.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index 33a32a2d1..3d7976acb 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -114,11 +114,12 @@ Section proof.
   Definition ress (I : gset gname) : iProp :=
     (Π★{set I} (λ i, ∃ R, saved_prop_own SpI i R ★ ▷R))%I.
 
+  Local Notation state_to_val s :=
+    (match s with State Low _ => 0 | State High _ => 1 end).
   Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp :=
-    match s with
-    | State Low I' => (heap_mapsto HeapI HeapG l ('0) ★ waiting P I')%I
-    | State High I' => (heap_mapsto HeapI HeapG l ('1) ★ ress I')%I
-    end.
+    (heap_mapsto HeapI HeapG l '(state_to_val s) ★
+     match s with State Low I' => waiting P I' | State High I' => ress I' end
+    )%I.
 
   Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
     (heap_ctx HeapI HeapG HeapN ★ sts_ctx StsI sts γ N (barrier_inv l P))%I.
-- 
GitLab