From 0918e16a4f10a3c3dc6a152bb9a115c1d46a43c0 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 21 Aug 2020 11:27:42 +0200
Subject: [PATCH] Proved contractiveness of iProto_own and iProto_mapsto

---
 theories/channel/channel.v | 4 ++++
 theories/channel/proto.v   | 4 ++++
 2 files changed, 8 insertions(+)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 5b9f353..d394efa 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -110,6 +110,10 @@ Instance: Params (@iProto_mapsto) 4 := {}.
 Notation "c ↣ p" := (iProto_mapsto c p)
   (at level 20, format "c  ↣  p").
 
+Instance iProto_mapsto_contractive `{!heapG Σ, !chanG Σ} c :
+  Contractive (iProto_mapsto c).
+Proof. rewrite iProto_mapsto_eq. solve_contractive.
+
 Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
     (p1 p2 : iProto Σ) : iProto Σ :=
   (<a @ (b : bool)> MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index fe123a1..70a07db 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -338,6 +338,10 @@ Definition iProto_own `{!protoG Σ V}
 Arguments iProto_own {_ _ _} _ _%proto.
 Instance: Params (@iProto_own) 3 := {}.
 
+Instance iProto_own_contractive `{protoG Σ V} γ s :
+  Contractive (iProto_own γ s).
+Proof. solve_contractive. Qed.
+
 (** * Proofs *)
 Section proto.
   Context `{!protoG Σ V}.
-- 
GitLab