From c8343385fd7c6d0d5d9ebc69993b76b8819c2654 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 25 Jul 2023 09:09:22 +0200
Subject: [PATCH] Counterexample for generalizing `mra A` to `A : ofe`.

---
 iris_unstable/algebra/monotone.v | 47 +++++++++++++++++++++++++++++++-
 1 file changed, 46 insertions(+), 1 deletion(-)

diff --git a/iris_unstable/algebra/monotone.v b/iris_unstable/algebra/monotone.v
index 45e2d6306..bb1c0c498 100644
--- a/iris_unstable/algebra/monotone.v
+++ b/iris_unstable/algebra/monotone.v
@@ -20,7 +20,52 @@ following paper for more details:
   Reasoning About Monotonicity in Separation Logic
   Amin Timany and Lars Birkedal
   in Certified Programs and Proofs (CPP) 2021
-*)
+
+Note that [mra A] works on [A : Type], not on [A : ofe]. (There are some results
+below if [A] has an [Equiv A], i.e., is a setoid.)
+
+Generalizing [mra A] to [A : ofe] and [R : A -n> A -n> siProp] is not obvious.
+It is not clear what axioms to impose on [R] for the "extension axiom" to hold:
+
+  cmra_extend :
+    x ≡{n}≡ y1 ⋅ y2 →
+    ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ y1 ≡{n}≡ z1 ∧ y2 ≡{n}≡ z2
+
+To prove this, assume
+
+  x ≡{n}≡ y1 ++ y2
+
+That means:
+
+  ∀ n' a, n' ≤ n →
+          mra_below a x n' ↔ mra_below a y1 n' ∨ mra_below a y2 n')
+
+From this assumption we cannot construct a [z1] and [z2].
+
+Here is a counterexample that shows the extension axiom is false without
+imposing any restrictions on the preorder [R]:
+
+  R a b := (a ≡ b) ∨ (▷ False ∧ a ≡ a1 ∧ b ≡ a2) ∨ (▷ False ∧ a ≡ a1 ∧ b ≡ a3)
+
+Visually:
+
+    R @ 0                         R @ n for n > 0
+
+      a1                            a1
+    /   \
+   /     \
+  a2     a3                      a2     a3
+
+We have:
+
+  [a1] ≡{0}≡ [a2] ++ [a3]
+
+Any [a] is below [a1] iff it is below [a2;a3]. The only [a] for which that is
+possible is [a1]. We do not have:
+
+  [a1] ≡{1}≡ [a2] ++ [a3]
+
+We have that [a1] is below [a1], but [a1] is not below [a2;a3]. *)
 
 Record mra {A} (R : relation A) := { mra_car : list A }.
 Definition to_mra {A} {R : relation A} (a : A) : mra R :=
-- 
GitLab