From 4c056f5e6d327e6167668753f3bd25603b2be804 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Mon, 27 Jun 2016 17:57:32 +0200
Subject: [PATCH] Counting CMRA

---
 _CoqProject      |  1 +
 algebra/count.v  | 21 +++++++++++++++++++++
 heap_lang/lang.v |  2 +-
 3 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 algebra/count.v

diff --git a/_CoqProject b/_CoqProject
index 53a3c0def..118a945f6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -55,6 +55,7 @@ algebra/upred_tactics.v
 algebra/upred_big_op.v
 algebra/upred_hlist.v
 algebra/frac.v
+algebra/count.v
 algebra/csum.v
 algebra/list.v
 algebra/updates.v
diff --git a/algebra/count.v b/algebra/count.v
new file mode 100644
index 000000000..b9ae12650
--- /dev/null
+++ b/algebra/count.v
@@ -0,0 +1,21 @@
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import upred.
+Notation count := nat (only parsing).
+
+Section count.
+Canonical Structure countC := leibnizC count.
+
+Instance count_valid : Valid count := λ _, True.
+Instance count_pcore : PCore count := λ _, None.
+Instance count_op : Op count := λ x y, (x + y)%nat.
+
+Definition count_ra_mixin : RAMixin nat.
+Proof. by split; try apply _. Qed.
+Canonical Structure countR := discreteR count count_ra_mixin.
+End count.
+
+(** Internalized properties *)
+Lemma count_equivI {M} (x y : count) : x ≡ y ⊣⊢ (x = y : uPred M).
+Proof. by uPred.unseal. Qed.
+Lemma count_validI {M} (x : count) : ✓ x ⊣⊢ (True : uPred M).
+Proof. by uPred.unseal. Qed.
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 62bb4a4c6..d184fa8fd 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -34,7 +34,7 @@ Proof.
 Qed.
 
 (** A typeclass for whether a variable is bound in a given
-   context. Making this a typeclass means we can use tpeclass search
+   context. Making this a typeclass means we can use typeclass search
    to program solving these constraints, so this becomes extensible.
    Also, since typeclass search runs *after* unification, Coq has already
    inferred the X for us; if we were to go for embedded proof terms ot
-- 
GitLab