show that the empty type is a COFE and a CMRA

Simon knows why ;)

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") }
 ]

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.

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}.

[Robbert Krebbers]

Not that it matters, but wouldn't it be more consistent to make this True. We also use True for equiv and dist (where it also doesn't matter).

[Ralf Jung]

I wanted to make those False as well but then the automation failed. Here it was easy though.

[Robbert Krebbers]

I also want to know why!