From 666af42e7b6841a784559589a9b6fe38b9afd754 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 26 Aug 2019 14:36:11 +0200
Subject: [PATCH] show that the empty type is a COFE and a CMRA

Simon knows why ;)
---
 opam                    |  2 +-
 theories/algebra/cmra.v | 18 ++++++++++++++++++
 theories/algebra/ofe.v  | 14 ++++++++++++++
 3 files changed, 33 insertions(+), 1 deletion(-)

diff --git a/opam b/opam
index 1fc1d3a78..a8ce3bbe3 100644
--- a/opam
+++ b/opam
@@ -12,5 +12,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2019-08-24.1.adfc24d2") | (= "dev") }
+  "coq-stdpp" { (= "dev.2019-08-26.0.1ae85171") | (= "dev") }
 ]
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 714b01afb..635bb9267 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -971,6 +971,24 @@ Section unit.
   Proof. by constructor. Qed.
 End unit.
 
+(** ** CMRA for the empty type *)
+Section empty.
+  Instance Empty_set_valid : Valid Empty_set := λ x, False.
+  Instance Empty_set_validN : ValidN Empty_set := λ n x, False.
+  Instance Empty_set_pcore : PCore Empty_set := λ x, Some x.
+  Instance Empty_set_op : Op Empty_set := λ x y, x.
+  Lemma Empty_set_cmra_mixin : CmraMixin Empty_set.
+  Proof. apply discrete_cmra_mixin, ra_total_mixin; by (intros [] || done). Qed.
+  Canonical Structure Empty_setR : cmraT := CmraT Empty_set Empty_set_cmra_mixin.
+
+  Global Instance Empty_set_cmra_discrete : CmraDiscrete Empty_setR.
+  Proof. done. Qed.
+  Global Instance Empty_set_core_id (x : Empty_set) : CoreId x.
+  Proof. by constructor. Qed.
+  Global Instance Empty_set_cancelable (x : Empty_set) : Cancelable x.
+  Proof. by constructor. Qed.
+End empty.
+
 (** ** Natural numbers *)
 Section nat.
   Instance nat_valid : Valid nat := λ x, True.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1f53c8d72..e8b300267 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -616,6 +616,20 @@ Section unit.
   Proof. done. Qed.
 End unit.
 
+(** empty *)
+Section empty.
+  Instance Empty_set_dist : Dist Empty_set := λ _ _ _, True.
+  Definition Empty_set_ofe_mixin : OfeMixin Empty_set.
+  Proof. by repeat split; try exists 0. Qed.
+  Canonical Structure Empty_setO : ofeT := OfeT Empty_set Empty_set_ofe_mixin.
+
+  Global Program Instance Empty_set_cofe : Cofe Empty_setO := { compl x := x 0 }.
+  Next Obligation. by repeat split; try exists 0. Qed.
+
+  Global Instance Empty_set_ofe_discrete : OfeDiscrete Empty_setO.
+  Proof. done. Qed.
+End empty.
+
 (** Product *)
 Section product.
   Context {A B : ofeT}.
-- 
GitLab