From f0856ce4c1af1b12363ebb5f8ec013273a5902f0 Mon Sep 17 00:00:00 2001
From: jihgfee <jkas@itu.dk>
Date: Fri, 11 Oct 2019 20:12:26 -0400
Subject: [PATCH] Re-instated missing operator. Moved Iris specific stuff into
 a utility file.

---
 _CoqProject                    |  1 +
 theories/channel/channel.v     |  7 ++++---
 theories/channel/proto_model.v |  3 +--
 theories/utils/misc.v          | 10 ++++++++++
 4 files changed, 16 insertions(+), 5 deletions(-)
 create mode 100644 theories/utils/misc.v

diff --git a/_CoqProject b/_CoqProject
index 1127464..54eb663 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,6 +5,7 @@ theories/utils/llist.v
 theories/utils/compare.v
 theories/utils/contribution.v
 theories/utils/group.v
+theories/utils/misc.v
 theories/channel/channel.v
 theories/channel/proto_model.v
 theories/channel/proto_channel.v
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 29271fd..2a396eb 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -18,7 +18,7 @@ and [chan_own]:
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import excl auth list.
-From actris.utils Require Import auth_excl llist.
+From actris.utils Require Import auth_excl llist misc.
 Set Default Proof Using "Type".
 
 Inductive side := Left | Right.
@@ -75,6 +75,7 @@ Proof.
     |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
 Qed.
 
+
 Section channel.
   Context `{!heapG Σ, !chanG Σ} (N : namespace).
 
@@ -126,9 +127,9 @@ Section channel.
     wp_lam.
     wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
     wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
-    iMod (own_alloc (● (to_auth_excl [])  ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
+    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
     { by apply auth_both_valid. }
-    iMod (own_alloc (● (to_auth_excl [])  ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
+    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
     { by apply auth_both_valid. }
     wp_apply (newlock_spec N (∃ ls rs,
       llist sbi_internal_eq l ls ∗ own lsγ (● to_auth_excl ls) ∗
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index da6ebdf..a141822 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -15,8 +15,7 @@ depends on the communicated value V and the dependent tail
 propositions of the logic.
 
 The type is defined as a solution to a recursive domain
-equation, as it is self-referential under the guard of â–¶.
-*)
+equation, as it is self-referential under the guard of â–¶.*)
 
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
diff --git a/theories/utils/misc.v b/theories/utils/misc.v
new file mode 100644
index 0000000..86a9f3c
--- /dev/null
+++ b/theories/utils/misc.v
@@ -0,0 +1,10 @@
+From iris.heap_lang Require Import notation.
+Set Default Proof Using "Type".
+
+(** MOVE TO IRIS *)
+Global Instance fst_atomic a v1 v2 : Atomic a (Fst (v1,v2)%V).
+Proof.
+  apply strongly_atomic_atomic, ectx_language_atomic;
+    [inversion 1; naive_solver
+    |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
+Qed.
-- 
GitLab