Counting CMRA

_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

algebra/count.v

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

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