From bbc9820d1bfc6983ae1989b62443ff42de543343 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 23 Jun 2016 14:31:15 +0200
Subject: [PATCH] add some comments explaining design decisions

---
 algebra/cmra.v    | 5 +++++
 algebra/updates.v | 4 ++++
 2 files changed, 9 insertions(+)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 87f4f717b..3fa2eb417 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -8,6 +8,11 @@ Instance: Params (@op) 2.
 Infix "â‹…" := op (at level 50, left associativity) : C_scope.
 Notation "(â‹…)" := op (only parsing) : C_scope.
 
+(* The inclusion quantifies over [A], not [option A].  This means we do not get
+   reflexivity.  However, if we used [option A], the following would no longer
+   hold:
+     x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2
+*)
 Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
 Infix "≼" := included (at level 70) : C_scope.
 Notation "(≼)" := included (only parsing) : C_scope.
diff --git a/algebra/updates.v b/algebra/updates.v
index 46dcfe7ab..6b5957120 100644
--- a/algebra/updates.v
+++ b/algebra/updates.v
@@ -10,6 +10,10 @@ Notation "x ~l~> y @ mz" := (local_update mz x y) (at level 70).
 Instance: Params (@local_update) 1.
 
 (** * Frame preserving updates *)
+(* This quantifies over [option A] for the frame.  That is necessary to
+   make the following hold:
+     x ~~> P → Some c ~~> Some P
+*)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n mz,
   ✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz).
 Instance: Params (@cmra_updateP) 1.
-- 
GitLab