CHANGELOG.md

@@ -44,6 +44,9 @@ Coq 8.13 is no longer supported.
   `x ≼ y`. This changes the statements of some lemmas: `singleton_included`,
   `local_update_valid0`, `local_update_valid`. Also add various new
   `Some_included` lemmas to help deal with these assertions.
+* Add hints for `a ≼ a ⋅ _` / `a ≼ _ ⋅ a` / `ε ≼ _` / `_ ≼ CsumBot` /
+  `_ ≼ ExclBot` with cost 0, which means they are used by `done` to finish
+  proofs. (by Ike Mulder)
 
 **Changes in `bi`:**
 
@@ -100,7 +103,8 @@ Coq 8.13 is no longer supported.
 * Add missing transitivity, symmetry and reflexivity lemmas about the `↔`, `→`,
   `-∗` and `∗-∗` connectives. (by Ike Mulder)
 * Add `∗-∗` as notation in `stdpp_scope` similar to `-∗`. This means `P ∗-∗ Q`
-  can be directly used as lemma statement, and is syntactic sugar for `⊢ P ∗-∗ Q`
+  can be directly used as lemma statement, and is syntactic sugar for `⊢ P ∗-∗ Q`.
+* Add `≼` connective (`internal_included`) on the BI level. (by Ike Mulder)
 
 **Changes in `proofmode`:**
 

_CoqProject

@@ -77,6 +77,7 @@ iris/bi/monpred.v
 iris/bi/embedding.v
 iris/bi/weakestpre.v
 iris/bi/telescopes.v
+iris/bi/lib/cmra.v
 iris/bi/lib/counterexamples.v
 iris/bi/lib/fixpoint.v
 iris/bi/lib/fractional.v

iris/algebra/cmra.v

@@ -637,6 +637,12 @@ Global Instance exclusive_id_free x : Exclusive x → IdFree x.
 Proof. intros ? z ? Hid. apply (exclusiveN_l 0 x z). by rewrite Hid. Qed.
 End cmra.
 
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
+Global Hint Extern 0 (?a ≼ ?a ⋅ _) => apply: cmra_included_l : core.
+Global Hint Extern 0 (?a ≼ _ ⋅ ?a) => apply: cmra_included_r : core.
+
 (** * Properties about CMRAs with a unit element **)
 Section ucmra.
   Context {A : ucmra}.
@@ -667,6 +673,7 @@ Section ucmra.
 End ucmra.
 
 Global Hint Immediate cmra_unit_cmra_total : core.
+Global Hint Extern 0 (ε ≼ _) => apply: ucmra_unit_least : core.
 
 (** * Properties about CMRAs with Leibniz equality *)
 Section cmra_leibniz.
@@ -1380,7 +1387,7 @@ Section option.
       destruct ma as [a|]; [right|by left].
       destruct mb as [b|]; [exists a, b|destruct mc; inversion_clear Hmc].
       destruct mc as [c|]; inversion_clear Hmc; split_and?; auto;
-        setoid_subst; eauto using cmra_included_l.
+        setoid_subst; eauto.
     - intros [->|(a&b&->&->&[Hc|[c Hc]])].
       + exists mb. by destruct mb.
       + exists None; by constructor.

iris/algebra/csum.v

@@ -199,6 +199,9 @@ Lemma Cinl_included a a' : Cinl a ≼ Cinl a' ↔ a ≼ a'.
 Proof. rewrite csum_included. naive_solver. Qed.
 Lemma Cinr_included b b' : Cinr b ≼ Cinr b' ↔ b ≼ b'.
 Proof. rewrite csum_included. naive_solver. Qed.
+Lemma CsumBot_included x : x ≼ CsumBot.
+Proof. exists CsumBot. by destruct x. Qed.
+(** We register a hint for [CsumBot_included] below. *)
 
 Lemma csum_includedN n x y :
   x ≼{n} y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼{n} a')
@@ -366,6 +369,10 @@ Proof.
 Qed.
 End cmra.
 
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
+Global Hint Extern 0 (_ ≼ CsumBot) => apply: CsumBot_included : core.
 Global Arguments csumR : clear implicits.
 
 (* Functor *)

iris/algebra/dyn_reservation_map.v

@@ -240,9 +240,10 @@ Section cmra.
   Proof.
       by rewrite {2}/op /dyn_reservation_map_op_instance /dyn_reservation_map_data /= singleton_op left_id_L.
   Qed.
+
   Lemma dyn_reservation_map_data_mono k a b :
     a ≼ b → dyn_reservation_map_data k a ≼ dyn_reservation_map_data k b.
-  Proof. intros [c ->]. rewrite dyn_reservation_map_data_op. apply cmra_included_l. Qed.
+  Proof. intros [c ->]. by rewrite dyn_reservation_map_data_op. Qed.
   Global Instance dyn_reservation_map_data_is_op k a b1 b2 :
     IsOp a b1 b2 →
     IsOp' (dyn_reservation_map_data k a) (dyn_reservation_map_data k b1) (dyn_reservation_map_data k b2).

iris/algebra/excl.v

@@ -112,8 +112,15 @@ Lemma Excl_included a b : Excl' a ≼ Excl' b ↔ a ≡ b.
 Proof.
   split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
 Qed.
+Lemma ExclBot_included ea : ea ≼ ExclBot.
+Proof. by exists ExclBot. Qed.
 End excl.
 
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
+Global Hint Extern 0 (_ ≼ ExclBot) => apply: ExclBot_included : core.
+
 Global Arguments exclO : clear implicits.
 Global Arguments exclR : clear implicits.
 

iris/algebra/gmap.v

@@ -346,8 +346,7 @@ Lemma singleton_included_l m i x :
 Proof.
   split.
   - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
-    exists (x ⋅? m' !! i). rewrite -Some_op_opM.
-    split; first done. apply cmra_included_l.
+    exists (x ⋅? m' !! i). by rewrite -Some_op_opM.
   - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
     intros j; destruct (decide (i = j)) as [->|].
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.

iris/algebra/max_prefix_list.v

@@ -104,7 +104,7 @@ Section max_prefix_list.
     split.
     - intros. eexists. apply equiv_dist=> n.
       apply to_max_prefix_list_includedN_aux. by apply: cmra_included_includedN.
-    - intros [l ->]. rewrite to_max_prefix_list_app. apply: cmra_included_l.
+    - intros [l ->]. rewrite to_max_prefix_list_app. eauto.
   Qed.
   Lemma to_max_prefix_list_included_L `{!LeibnizEquiv A} l1 l2 :
     to_max_prefix_list l1 ≼ to_max_prefix_list l2 ↔ l1 `prefix_of` l2.

iris/algebra/reservation_map.v

@@ -225,7 +225,7 @@ Section cmra.
   Qed.
   Lemma reservation_map_data_mono k a b :
     a ≼ b → reservation_map_data k a ≼ reservation_map_data k b.
-  Proof. intros [c ->]. rewrite reservation_map_data_op. apply cmra_included_l. Qed.
+  Proof. intros [c ->]. by rewrite reservation_map_data_op. Qed.
   Global Instance reservation_map_data_is_op k a b1 b2 :
     IsOp a b1 b2 →
     IsOp' (reservation_map_data k a) (reservation_map_data k b1) (reservation_map_data k b2).

iris/algebra/view.v

@@ -288,7 +288,7 @@ Section cmra.
   Lemma view_frag_op b1 b2 : ◯V (b1 ⋅ b2) = ◯V b1 ⋅ ◯V b2.
   Proof. done. Qed.
   Lemma view_frag_mono b1 b2 : b1 ≼ b2 → ◯V b1 ≼ ◯V b2.
-  Proof. intros [c ->]. rewrite view_frag_op. apply cmra_included_l. Qed.
+  Proof. intros [c ->]. by rewrite view_frag_op. Qed.
   Lemma view_frag_core b : core (◯V b) = ◯V (core b).
   Proof. done. Qed.
   Lemma view_both_core_discarded a b :
@@ -409,7 +409,7 @@ Section cmra.
     split.
     - intros [[[[dqf agf]|] bf]
         [[?%(discrete_iff _ _) ?]%(inj Some) _]]; simplify_eq/=.
-      + split; [left; apply: cmra_included_l|]. apply to_agree_includedN. by exists agf.
+      + split; [eauto|]. apply to_agree_includedN. by exists agf.
       + split; [right; done|]. by apply (inj to_agree).
     - intros [[[? ->]| ->] ->].
       + rewrite view_auth_dfrac_op -assoc. apply cmra_includedN_l.
@@ -424,8 +424,8 @@ Section cmra.
       + apply equiv_dist=> n.
         by eapply view_auth_dfrac_includedN, cmra_included_includedN.
     - intros [[[dq ->]| ->] ->].
-      + rewrite view_auth_dfrac_op -assoc. apply cmra_included_l.
-      + apply cmra_included_l.
+      + by rewrite view_auth_dfrac_op -assoc.
+      + done.
   Qed.
   Lemma view_auth_includedN n a1 a2 b :
     ●V a1 ≼{n} ●V a2 ⋅ ◯V b ↔ a1 ≡{n}≡ a2.
@@ -448,7 +448,7 @@ Section cmra.
     split.
     - intros [xf [_ Hb]]; simpl in *.
       revert Hb; rewrite left_id. by exists (view_frag_proj xf).
-    - intros [bf ->]. rewrite comm view_frag_op -assoc. apply cmra_included_l.
+    - intros [bf ->]. by rewrite comm view_frag_op -assoc.
   Qed.
 
   (** The weaker [view_both_included] lemmas below are a consequence of the

iris/base_logic/algebra.v

@@ -59,20 +59,8 @@ Section upred.
 
   Section excl.
     Context {A : ofe}.
-    Implicit Types a b : A.
-    Implicit Types x y : excl A.
-
-    Lemma excl_equivI x y :
-      x ≡ y ⊣⊢ match x, y with
-                          | Excl a, Excl b => a ≡ b
-                          | ExclBot, ExclBot => True
-                          | _, _ => False
-                          end.
-    Proof.
-      uPred.unseal. do 2 split.
-      - by destruct 1.
-      - by destruct x, y; try constructor.
-    Qed.
+    Implicit Types x : excl A.
+
     Lemma excl_validI x :
       ✓ x ⊣⊢ if x is ExclBot then False else True.
     Proof. uPred.unseal. by destruct x. Qed.
@@ -132,24 +120,6 @@ Section upred.
     Qed.
   End agree.
 
-  Section csum_ofe.
-    Context {A B : ofe}.
-    Implicit Types a : A.
-    Implicit Types b : B.
-
-    Lemma csum_equivI (x y : csum A B) :
-      x ≡ y ⊣⊢ match x, y with
-                          | Cinl a, Cinl a' => a ≡ a'
-                          | Cinr b, Cinr b' => b ≡ b'
-                          | CsumBot, CsumBot => True
-                          | _, _ => False
-                          end.
-    Proof.
-      uPred.unseal; do 2 split; first by destruct 1.
-        by destruct x, y; try destruct 1; try constructor.
-    Qed.
-  End csum_ofe.
-
   Section csum_cmra.
     Context {A B : cmra}.
     Implicit Types a : A.

iris/bi/internal_eq.v

 From iris.bi Require Import derived_laws_later big_op.
 From iris.prelude Require Import options.
+From iris.algebra Require Import excl csum.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (* We enable primitive projections in this file to improve the performance of the Iris proofmode:
@@ -157,6 +158,46 @@ Section internal_eq_derived.
     - destruct x as [a|], y as [a'|]; auto. apply f_equivI, _.
   Qed.
 
+  Lemma csum_equivI {A B : ofe} (sx sy : csum A B) :
+    sx ≡ sy ⊣⊢ match sx, sy with
+               | Cinl x, Cinl y => x ≡ y
+               | Cinr x, Cinr y => x ≡ y
+               | CsumBot, CsumBot => True
+               | _, _ => False
+               end.
+  Proof.
+    apply (anti_symm _).
+    - apply (internal_eq_rewrite' sx sy (λ sy',
+               match sx, sy' with
+               | Cinl x, Cinl y => x ≡ y
+               | Cinr x, Cinr y => x ≡ y
+               | CsumBot, CsumBot => True
+               | _, _ => False
+               end)%I); [solve_proper|auto|].
+      destruct sx; eauto.
+    - destruct sx; destruct sy; eauto;
+      apply f_equivI, _.
+  Qed.
+
+  Lemma excl_equivI {O : ofe} (x y : excl O) :
+    x ≡ y ⊣⊢ match x, y with
+             | Excl a, Excl b => a ≡ b
+             | ExclBot, ExclBot => True
+             | _, _ => False
+             end.
+  Proof.
+    apply (anti_symm _).
+    - apply (internal_eq_rewrite' x y (λ y',
+               match x, y' with
+               | Excl a, Excl b => a ≡ b
+               | ExclBot, ExclBot => True
+               | _, _ => False
+               end)%I); [solve_proper|auto|].
+      destruct x; eauto.
+    - destruct x as [e1|]; destruct y as [e2|]; [|by eauto..].
+      apply f_equivI, _.
+  Qed.
+
   Lemma sig_equivI {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
   Proof.
     apply (anti_symm _).

iris/bi/lib/cmra.v

+From iris.proofmode Require Import proofmode.
+From iris.bi Require Import internal_eq.
+From iris.algebra Require Import cmra csum excl agree.
+From iris.prelude Require Import options.
+
+(** Derived [≼] connective on [cmra] elements. This can be defined on
+    any [bi] that has internal equality [≡]. It corresponds to the
+    step-indexed [≼{n}] connective in the [uPred] model. *)
+Definition internal_included `{!BiInternalEq PROP} {A : cmra} (a b : A) : PROP :=
+  ∃ c, b ≡ a ⋅ c.
+Global Arguments internal_included {_ _ _} _ _ : simpl never.
+Global Instance: Params (@internal_included) 3 := {}.
+Global Typeclasses Opaque internal_included.
+
+Infix "≼" := internal_included : bi_scope.
+
+Section internal_included_laws.
+  Context `{!BiInternalEq PROP}.
+  Implicit Type A B : cmra.
+
+  (* Force implicit argument PROP *)
+  Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+  Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
+
+  (** Propers *)
+  Global Instance internal_included_nonexpansive A :
+    NonExpansive2 (internal_included (PROP := PROP) (A := A)).
+  Proof. solve_proper. Qed.
+  Global Instance internal_included_proper A :
+    Proper ((≡) ==> (≡) ==> (⊣⊢)) (internal_included (PROP := PROP) (A := A)).
+  Proof. solve_proper. Qed.
+
+  (** Proofmode support *)
+  Global Instance into_pure_internal_included {A} (a b : A) `{!Discrete b} :
+    @IntoPure PROP (a ≼ b) (a ≼ b).
+  Proof. rewrite /IntoPure /internal_included. eauto. Qed.
+
+  Global Instance from_pure_internal_included {A} (a b : A) :
+    @FromPure PROP false (a ≼ b) (a ≼ b).
+  Proof. rewrite /FromPure /= /internal_included. eauto. Qed.
+
+  Global Instance into_exist_internal_included {A} (a b : A) :
+    IntoExist (PROP := PROP) (a ≼ b) (λ c, b ≡ a ⋅ c)%I (λ x, x).
+  Proof. by rewrite /IntoExist. Qed.
+
+  Global Instance from_exist_internal_included {A} (a b : A) :
+    FromExist (PROP := PROP) (a ≼ b) (λ c, b ≡ a ⋅ c)%I.
+  Proof. by rewrite /FromExist. Qed.
+
+  Global Instance internal_included_persistent {A} (a b : A) :
+    Persistent (PROP := PROP) (a ≼ b).
+  Proof. rewrite /internal_included. apply _. Qed.
+
+  Global Instance internal_included_absorbing {A} (a b : A) :
+    Absorbing (PROP := PROP) (a ≼ b).
+  Proof. rewrite /internal_included. apply _. Qed.
+
+  Lemma internal_included_refl `{!CmraTotal A} (x : A) : ⊢@{PROP} x ≼ x.
+  Proof. iExists (core x). by rewrite cmra_core_r. Qed.
+  Lemma internal_included_trans {A} (x y z : A) :
+    ⊢@{PROP} x ≼ y -∗ y ≼ z -∗ x ≼ z.
+  Proof.
+    iIntros "#[%x' Hx'] #[%y' Hy']". iExists (x' ⋅ y').
+    rewrite assoc. by iRewrite -"Hx'".
+  Qed.
+
+  (** Simplification lemmas *)
+  Lemma f_homom_includedI {A B} (x y : A) (f : A → B) `{!NonExpansive f} :
+    (* This is a slightly weaker condition than being a [CmraMorphism] *)
+    (∀ c, f x ⋅ f c ≡ f (x ⋅ c)) →
+    (x ≼ y ⊢ f x ≼ f y).
+  Proof.
+    intros f_homom. iDestruct 1 as (z) "Hz".
+    iExists (f z). rewrite f_homom.
+    by iApply f_equivI.
+  Qed.
+
+  Lemma prod_includedI {A B} (x y : A * B) :
+    x ≼ y ⊣⊢ (x.1 ≼ y.1) ∧ (x.2 ≼ y.2).
+  Proof.
+    destruct x as [x1 x2], y as [y1 y2]; simpl; iSplit.
+    - iIntros "#[%z H]". rewrite prod_equivI /=. iDestruct "H" as "[??]".
+      iSplit; by iExists _.
+    - iIntros "#[[%z1 Hz1] [%z2 Hz2]]". iExists (z1, z2).
+      rewrite prod_equivI /=; auto.
+  Qed.
+
+  Lemma option_includedI {A} (mx my : option A) :
+    mx ≼ my ⊣⊢ match mx, my with
+               | Some x, Some y => (x ≼ y) ∨ (x ≡ y)
+               | None, _ => True
+               | Some x, None => False
+               end.
+  Proof.
+    iSplit.
+    - iIntros "[%mz H]". rewrite option_equivI.
+      destruct mx as [x|], my as [y|], mz as [z|]; simpl; auto; [|].
+      + iLeft. by iExists z.
+      + iRight. by iRewrite "H".
+    - destruct mx as [x|], my as [y|]; simpl; auto; [|].
+      + iDestruct 1 as "[[%z H]|H]"; iRewrite "H".
+        * by iExists (Some z).
+        * by iExists None.
+      + iIntros "_". by iExists (Some y).
+  Qed.
+
+  Lemma option_included_totalI `{!CmraTotal A} (mx my : option A) :
+    mx ≼ my ⊣⊢ match mx, my with
+               | Some x, Some y => x ≼ y
+               | None, _ => True
+               | Some x, None => False
+               end.
+  Proof.
+    rewrite option_includedI. destruct mx as [x|], my as [y|]; [|done..].
+    iSplit; [|by auto].
+    iIntros "[Hx|Hx] //". iRewrite "Hx". iApply (internal_included_refl y).
+  Qed.
+
+  Lemma csum_includedI {A B} (sx sy : csum A B) :
+    sx ≼ sy ⊣⊢ match sx, sy with
+               | Cinl x, Cinl y => x ≼ y
+               | Cinr x, Cinr y => x ≼ y
+               | _, CsumBot => True
+               | _, _ => False
+               end.
+  Proof.
+    iSplit.
+    - iDestruct 1 as (sz) "H". rewrite csum_equivI.
+      destruct sx, sy, sz; rewrite /internal_included /=; auto.
+    - destruct sx as [x|x|], sy as [y|y|]; eauto; [|].
+      + iIntros "#[%z H]". iExists (Cinl z). by rewrite csum_equivI.
+      + iIntros "#[%z H]". iExists (Cinr z). by rewrite csum_equivI.
+  Qed.
+
+  Lemma excl_includedI {O : ofe} (x y : excl O) :
+    x ≼ y ⊣⊢ match y with
+             | ExclBot => True
+             |  _ => False
+             end.
+  Proof.
+    iSplit.
+    - iIntros "[%z Hz]". rewrite excl_equivI. destruct y, x, z; auto.
+    - destruct y; [done|]. iIntros "_". by iExists ExclBot.
+  Qed.
+
+  Lemma agree_includedI {O : ofe} (x y : agree O) : x ≼ y ⊣⊢ y ≡ x ⋅ y.
+  Proof.
+    iSplit.
+    + iIntros "[%z Hz]". iRewrite "Hz". by rewrite assoc agree_idemp.
+    + iIntros "H". by iExists _.
+  Qed.
+End internal_included_laws.
\ No newline at end of file

iris_unstable/algebra/monotone.v

@@ -6,241 +6,209 @@ From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.prelude Require Import options.
 
-Local Arguments pcore _ _ !_ /.
-Local Arguments cmra_pcore _ !_ /.
-Local Arguments validN _ _ _ !_ /.
-Local Arguments valid _ _  !_ /.
-Local Arguments cmra_validN _ _ !_ /.
-Local Arguments cmra_valid _  !_ /.
-
-(* Given a preorder relation R on a type A we construct a resource algebra mra R
-   and an injection principal : A -> mra R such that:
-   [R x y] iff [principal x ≼ principal y]
-   where ≼ is the extension order of mra R resource algebra. This is exactly
-   what the lemma [principal_included] shows.
-
-   This resource algebra is useful for reasoning about monotonicity.
-   See the following paper for more details:
-
-   Reasoning About Monotonicity in Separation Logic
-   Amin Timany and Lars Birkedal
-   in Certified Programs and Proofs (CPP) 2021
-*)
-
-Definition mra {A : Type} (R : relation A) : Type := list A.
-Definition principal {A : Type} (R : relation A) (a : A) : mra R := [a].
-
-(* OFE *)
-Section ofe.
-  Context {A : Type} {R : relation A}.
-  Implicit Types a b : A.
-  Implicit Types x y : mra R.
+(** Given a preorder [R] on a type [A] we construct the "monotone" resource
+algebra [mra R] and an injection [to_mra : A → mra R] such that:
 
-  Local Definition below (a : A) (x : mra R) := ∃ b, b ∈ x ∧ R a b.
+   [R x y] iff [to_mra x ≼ to_mra y]
 
-  Local Lemma below_app a x y : below a (x ++ y) ↔ below a x ∨ below a y.
-  Proof.
-    split.
-    - intros (b & [|]%elem_of_app & ?); [left|right]; exists b; eauto.
-    - intros [(b & ? & ?)|(b & ? & ?)]; exists b; rewrite elem_of_app; eauto.
-  Qed.
+Here, [≼] is the extension order of the [mra R] resource algebra. This is
+exactly what the lemma [to_mra_included] shows.
 
-  Local Lemma below_principal a b : below a (principal R b) ↔ R a b.
-  Proof.
-    split.
-    - intros (c & ->%elem_of_list_singleton & ?); done.
-    - intros Hab; exists b; split; first apply elem_of_list_singleton; done.
-  Qed.
+This resource algebra is useful for reasoning about monotonicity. See the
+following paper for more details:
 
-  Local Instance mra_equiv : Equiv (mra R) :=
-    λ x y, ∀ a, below a x ↔ below a y.
+  Reasoning About Monotonicity in Separation Logic
+  Amin Timany and Lars Birkedal
+  in Certified Programs and Proofs (CPP) 2021
 
-  Local Instance mra_equiv_equiv : Equivalence mra_equiv.
-  Proof.
-    split; [by firstorder|by firstorder|].
-    intros ??? Heq1 Heq2 ?; split; intros ?;
-      [apply Heq2; apply Heq1|apply Heq1; apply Heq2]; done.
-  Qed.
+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.)
 
-  Canonical Structure mraO := discreteO (mra R).
-End ofe.
+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
 
-Global Arguments mraO [_] _.
+That means:
 
-(* CMRA *)
-Section cmra.
-  Context {A : Type} {R : relation A}.
+  ∀ 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 :=
+  {| mra_car := [a] |}.
+Global Arguments mra_car {_ _} _.
+
+Section mra.
+  Context {A} {R : relation A}.
   Implicit Types a b : A.
   Implicit Types x y : mra R.
 
+  Local Definition mra_below (a : A) (x : mra R) := ∃ b, b ∈ mra_car x ∧ R a b.
+
+  Local Lemma mra_below_to_mra a b : mra_below a (to_mra b) ↔ R a b.
+  Proof. set_solver. Qed.
+
+  (* OFE *)
+  Local Instance mra_equiv : Equiv (mra R) := λ x y,
+    ∀ a, mra_below a x ↔ mra_below a y.
+
+  Local Instance mra_equiv_equiv : Equivalence mra_equiv.
+  Proof. unfold mra_equiv; split; intros ?; naive_solver. Qed.
+
+  Canonical Structure mraO := discreteO (mra R).
+
+  (* CMRA *)
   Local Instance mra_valid : Valid (mra R) := λ x, True.
   Local Instance mra_validN : ValidN (mra R) := λ n x, True.
-  Local Program Instance mra_op : Op (mra R) := λ x y, x ++ y.
+  Local Program Instance mra_op : Op (mra R) := λ x y,
+    {| mra_car := mra_car x ++ mra_car y |}.
   Local Instance mra_pcore : PCore (mra R) := Some.
 
   Lemma mra_cmra_mixin : CmraMixin (mra R).
   Proof.
     apply discrete_cmra_mixin; first apply _.
-    apply ra_total_mixin.
-    - eauto.
-    - intros ??? Heq a; specialize (Heq a); rewrite !below_app; firstorder.
-    - intros ?; done.
-    - done.
-    - intros ????; rewrite !below_app; firstorder.
-    - intros ???; rewrite !below_app; firstorder.
-    - rewrite /core /pcore /=; intros ??; rewrite below_app; firstorder.
-    - done.
-    - intros ? ? [? ?]; eexists _; done.
-    - done.
+    apply ra_total_mixin; try done.
+    - (* [Proper] of [op] *) intros x y z Hyz a. specialize (Hyz a). set_solver.
+    - (* [Proper] of [core] *) apply _.
+    - (* [Assoc] *) intros x y z a. set_solver.
+    - (* [Comm] *) intros x y a. set_solver.
+    - (* [core x ⋅ x ≡ x] *) intros x a. set_solver.
   Qed.
 
   Canonical Structure mraR : cmra := Cmra (mra R) mra_cmra_mixin.
 
   Global Instance mra_cmra_total : CmraTotal mraR.
   Proof. rewrite /CmraTotal; eauto. Qed.
-  Global Instance mra_core_id (x : mra R) : CoreId x.
+  Global Instance mra_core_id x : CoreId x.
   Proof. by constructor. Qed.
 
   Global Instance mra_cmra_discrete : CmraDiscrete mraR.
   Proof. split; last done. intros ? ?; done. Qed.
 
-  Local Instance mra_unit : Unit (mra R) := @nil A.
+  Local Instance mra_unit : Unit (mra R) := {| mra_car := [] |}.
   Lemma auth_ucmra_mixin : UcmraMixin (mra R).
   Proof. split; done. Qed.
 
   Canonical Structure mraUR := Ucmra (mra R) auth_ucmra_mixin.
 
-  Lemma mra_idemp (x : mra R) : x ⋅ x ≡ x.
-  Proof. intros a; rewrite below_app; naive_solver. Qed.
+  (* Laws *)
+  Lemma mra_idemp x : x ⋅ x ≡ x.
+  Proof. intros a. set_solver. Qed.
 
-  Lemma mra_included (x y : mra R) : x ≼ y ↔ y ≡ x ⋅ y.
+  Lemma mra_included x y : x ≼ y ↔ y ≡ x ⋅ y.
   Proof.
     split; [|by intros ?; exists y].
     intros [z ->]; rewrite assoc mra_idemp; done.
   Qed.
 
-  Lemma principal_R_opN_base `{!Transitive R} n x y :
-    (∀ b, b ∈ y → ∃ c, c ∈ x ∧ R b c) → y ⋅ x ≡{n}≡ x.
-  Proof.
-    intros HR; split; rewrite /op /mra_op below_app; [|by firstorder].
-    intros [(c & (d & Hd1 & Hd2)%HR & Hc2)|]; [|done].
-    exists d; split; [|transitivity c]; done.
-  Qed.
-
-  Lemma principal_R_opN `{!Transitive R} n a b :
-    R a b → principal R a ⋅ principal R b ≡{n}≡ principal R b.
-  Proof.
-    intros; apply principal_R_opN_base; intros c; rewrite /principal.
-    setoid_rewrite elem_of_list_singleton => ->; eauto.
-  Qed.
-
-  Lemma principal_R_op `{!Transitive R} a b :
-    R a b → principal R a ⋅ principal R b ≡ principal R b.
-  Proof. by intros ? ?; apply (principal_R_opN 0). Qed.
-
-  Lemma principal_op_RN n a b x :
-    R a a → principal R a ⋅ x ≡{n}≡ principal R b → R a b.
-  Proof.
-    intros Ha HR.
-    destruct (HR a) as [[z [HR1%elem_of_list_singleton HR2]] _];
-      last by subst; eauto.
-    rewrite /op /mra_op /principal below_app below_principal; auto.
-  Qed.
-
-  Lemma principal_op_R' a b x :
-    R a a → principal R a ⋅ x ≡ principal R b → R a b.
-  Proof. intros ? ?; eapply (principal_op_RN 0); eauto. Qed.
-
-  Lemma principal_op_R `{!Reflexive R} a b x :
-    principal R a ⋅ x ≡ principal R b → R a b.
-  Proof. intros; eapply principal_op_R'; eauto. Qed.
+  Lemma to_mra_R_op `{!Transitive R} a b :
+    R a b →
+    to_mra a ⋅ to_mra b ≡ to_mra b.
+  Proof. intros Hab c. set_solver. Qed.
 
-  Lemma principal_includedN `{!PreOrder R} n a b :
-    principal R a ≼{n} principal R b ↔ R a b.
+  Lemma to_mra_included `{!PreOrder R} a b :
+    to_mra a ≼ to_mra b ↔ R a b.
   Proof.
     split.
-    - intros [z Hz]; eapply principal_op_RN; first done. by rewrite Hz.
-    - intros ?; exists (principal R b); rewrite principal_R_opN; eauto.
+    - move=> [z Hz]. specialize (Hz a). set_solver.
+    - intros ?; exists (to_mra b). by rewrite to_mra_R_op.
   Qed.
 
-  Lemma principal_included `{!PreOrder R} a b :
-    principal R a ≼ principal R b ↔ R a b.
-  Proof. apply (principal_includedN 0). Qed.
-
   Lemma mra_local_update_grow `{!Transitive R} a x b:
     R a b →
-    (principal R a, x) ~l~> (principal R b, principal R b).
+    (to_mra a, x) ~l~> (to_mra b, to_mra b).
   Proof.
-    intros Hana Hanb.
-    apply local_update_unital_discrete.
-    intros z _ Habz.
-    split; first done.
-    intros w; split.
-    - intros (y & ->%elem_of_list_singleton & Hy2).
-      exists b; split; first constructor; done.
-    - intros (y & [->|Hy1]%elem_of_cons & Hy2).
-      + exists b; split; first constructor; done.
-      + exists b; split; first constructor.
-        specialize (Habz w) as [_ [c [->%elem_of_list_singleton Hc2]]].
-        { exists y; split; first (by apply elem_of_app; right); eauto. }
-        etrans; eauto.
+    intros Hana. apply local_update_unital_discrete=> z _ Habz.
+    split; first done. intros c. specialize (Habz c). set_solver.
   Qed.
 
   Lemma mra_local_update_get_frag `{!PreOrder R} a b:
     R b a →
-    (principal R a, ε) ~l~> (principal R a, principal R b).
+    (to_mra a, ε) ~l~> (to_mra a, to_mra b).
   Proof.
-    intros Hana.
-    apply local_update_unital_discrete.
-    intros z _; rewrite left_id; intros <-.
-    split; first done.
-    apply mra_included; by apply principal_included.
+    intros Hana. apply local_update_unital_discrete=> z _.
+    rewrite left_id. intros <-. split; first done.
+    apply mra_included; by apply to_mra_included.
   Qed.
+End mra.
 
-End cmra.
-
+Global Arguments mraO {_} _.
 Global Arguments mraR {_} _.
 Global Arguments mraUR {_} _.
 
-
-(* Might be useful if the type of elements is an OFE. *)
-Section mra_over_ofe.
-  Context {A : ofe} {R : relation A}.
+(** If [R] is a partial order, relative to a reflexive relation [S] on the
+carrier [A], then [to_mra] is proper and injective. The theory for
+arbitrary relations [S] is overly general, so we do not declare the results
+as instances. Below we provide instances for [S] being [=] and [≡]. *)
+Section mra_over_rel.
+  Context {A} {R : relation A} (S : relation A).
   Implicit Types a b : A.
   Implicit Types x y : mra R.
 
-  Global Instance principal_ne
-         `{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
-    NonExpansive (principal R).
-  Proof. intros n a1 a2 Ha; split; rewrite !below_principal !Ha; done. Qed.
+  Lemma to_mra_rel_proper :
+    Reflexive S →
+    Proper (S ==> S ==> iff) R →
+    Proper (S ==> (≡@{mra R})) (to_mra).
+  Proof. intros ? HR a1 a2 Ha b. rewrite !mra_below_to_mra. by apply HR. Qed.
 
-  Global Instance principal_proper
-         `{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
-    Proper ((≡) ==> (≡)) (principal R) := ne_proper _.
-
-  Lemma principal_inj_related a b :
-    principal R a ≡ principal R b → R a a → R a b.
+  Lemma to_mra_rel_inj :
+    Reflexive R →
+    AntiSymm S R →
+    Inj S (≡@{mra R}) (to_mra).
   Proof.
-    intros Hab ?.
-    destruct (Hab a) as [[? [?%elem_of_list_singleton ?]] _];
-      last by subst; auto.
-    exists a; rewrite /principal elem_of_list_singleton; done.
+    intros ?? a b Hab. move: (Hab a) (Hab b). rewrite !mra_below_to_mra.
+    intros. apply (anti_symm R); naive_solver.
   Qed.
-
-  Lemma principal_inj_general a b :
-    principal R a ≡ principal R b →
-    R a a → R b b → (R a b → R b a → a ≡ b) → a ≡ b.
-  Proof. intros ??? Has; apply Has; apply principal_inj_related; auto. Qed.
-
-  Global Instance principal_inj_instance `{!Reflexive R} `{!AntiSymm (≡) R} :
-    Inj (≡) (≡) (principal R).
-  Proof. intros ???; apply principal_inj_general; auto. Qed.
-
-  Global Instance principal_injN `{!Reflexive R} {Has : AntiSymm (≡) R} n :
-    Inj (dist n) (dist n) (principal R).
-  Proof.
-    intros x y Hxy%discrete_iff; last apply _.
-    eapply equiv_dist; revert Hxy; apply inj; apply _.
-  Qed.
-
-End mra_over_ofe.
+End mra_over_rel.
+
+Global Instance to_mra_inj {A} {R : relation A} :
+  Reflexive R →
+  AntiSymm (=) R →
+  Inj (=) (≡@{mra R}) (to_mra) | 0. (* Lower cost than [to_mra_inj] *)
+Proof. intros. by apply (to_mra_rel_inj (=)). Qed.
+
+Global Instance to_mra_proper `{Equiv A} {R : relation A} :
+  Reflexive (≡@{A}) →
+  Proper ((≡) ==> (≡) ==> iff) R →
+  Proper ((≡) ==> (≡@{mra R})) (to_mra).
+Proof. intros. by apply (to_mra_rel_proper (≡)). Qed.
+
+Global Instance to_mra_equiv_inj `{Equiv A} {R : relation A} :
+  Reflexive R →
+  AntiSymm (≡) R →
+  Inj (≡) (≡@{mra R}) (to_mra) | 1.
+Proof. intros. by apply (to_mra_rel_inj (≡)). Qed.

iris_unstable/base_logic/algebra.v

 (** This is just an integration file for [iris_staging.algebra.list];
 both should be stabilized together. *)
 From iris.algebra Require Import cmra.
-From iris.unstable.algebra Require Import list monotone.
+From iris.unstable.algebra Require Import list.
 From iris.base_logic Require Import bi derived.
 From iris.prelude Require Import options.
 
@@ -19,16 +19,4 @@ Section list_cmra.
   Lemma list_validI l : ✓ l ⊣⊢ ∀ i, ✓ (l !! i).
   Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
 End list_cmra.
-
-Section monotone.
-  Lemma monotone_equivI {A : ofe} (R : relation A)
-        `{!(∀ n : nat, Proper (dist n ==> dist n ==> iff) R)}
-        `{!Reflexive R} `{!AntiSymm (≡) R} a b :
-    principal R a ≡ principal R b ⊣⊢ (a ≡ b).
-  Proof.
-    uPred.unseal. do 2 split; intros ?.
-    - exact: principal_injN.
-    - exact: principal_ne.
-  Qed.
-End monotone.
 End upred.

tests/monotone.ref

+"mra_test_eq"
+     : string
+1 goal
+  
+  X, Y : gset nat
+  H : X = Y
+  ============================
+  X = Y

tests/monotone.v

+From stdpp Require Import propset gmap strings.
+From iris.unstable.algebra Require Import monotone.
+
+Unset Mangle Names.
+
+Notation gset_mra K:= (mra (⊆@{gset K})).
+
+(* Check if we indeed get [=], i.e., the right [Inj] instance is used. *)
+Check "mra_test_eq".
+Lemma mra_test_eq X Y : to_mra X ≡@{gset_mra nat} to_mra Y → X = Y.
+Proof. intros ?%(inj _). Show. done. Qed.
+
+Notation propset_mra K := (mra (⊆@{propset K})).
+
+Lemma mra_test_equiv X Y : to_mra X ≡@{propset_mra nat} to_mra Y → X ≡ Y.
+Proof. intros ?%(inj _). done. Qed.