CHANGELOG.md

@@ -47,6 +47,7 @@ Coq 8.13 is no longer supported.
 * 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)
+* Rename `singleton_mono` to `singleton_included_mono`.
 
 **Changes in `bi`:**
 
@@ -105,6 +106,10 @@ Coq 8.13 is no longer supported.
 * 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`.
 * Add `≼` connective (`internal_included`) on the BI level. (by Ike Mulder)
+* Move laws of persistence modality out of `BiMixin` into `BiPersistentlyMixin`.
+* Provide smart constructor `bi_persistently_mixin_discrete` for
+  `BiPersistentlyMixin`: Given a discrete BI that enjoys the existential
+  property, a trivial definition of the persistence modality can be given.
 
 **Changes in `proofmode`:**
 

docs/style_guide.md

@@ -210,10 +210,6 @@ theories/base_logic/lib is for constructions in the base logic (using own)
 * `list_lookup_insert` is named by context (the type involved), then the two functions outside-in on the left-hand-side, so it has the type `lookup (insert …) = …` where the `insert` is on a list. Notations mean it doesn’t actually look like this and the insert is textually first.
 * Injectivity theorems are instances of `Inj` and then are used with `inj`
 * Suffixes `_l` and `_r` when we have binary `op x y` and a theorem related to the left or right. For example, `sep_mono_l` says bi_sep is monotonic in its left argument (holding the right constant).
-* Entailments at the top level are typically written `P -* Q`, which is notation
-  for `P ⊢ Q`. If you have a theorem which has no premises you have to write ⊢ P
-  explicitly (for example, it is common to have `⊢ |==> ∃ γ, …` for an allocation
-  theorem)
 * Suffix `'` (prime) is used when `foo'` is a corollary of `foo`. Try to avoid
   these since the name doesn't convey how `foo'` is related to `foo`.
 * Given a polymorphic function/relation `f` (e.g., `eq`, `equiv`, `subseteq`), the instance of type `A` is called `A_f_instance`, and we add a lemma `A_f` that characterizes the instance. In case of many instances, this lemma is proved by unfolding the definition of the instance, e.g., `frac_op`, `frac_valid`. However, in some cases, e.g., `list_eq`, `map_eq`, `set_eq` this lemma might require non-trivial proof work.
@@ -224,6 +220,7 @@ theories/base_logic/lib is for constructions in the base logic (using own)
     M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
     M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
     ```
+* Monotonicity lemmas where the relation can be ambiguous are called `<f>_<relation>_mono`, e.g. `Some_included_mono`.
 
 ### Naming algebra libraries
 

iris/algebra/gmap.v

@@ -369,7 +369,7 @@ Qed.
 Lemma singleton_included_total `{!CmraTotal A}  i x y :
   {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ x ≼ y.
 Proof. rewrite singleton_included Some_included_total. done. Qed.
-Lemma singleton_mono i x y :
+Lemma singleton_included_mono i x y :
   x ≼ y → {[ i := x ]} ≼ ({[ i := y ]} : gmap K A).
 Proof. intros Hincl. apply singleton_included, Some_included_mono. done. Qed.
 

iris/algebra/ofe.v

@@ -860,6 +860,10 @@ Section product.
   Global Instance prod_ofe_discrete :
     OfeDiscrete A → OfeDiscrete B → OfeDiscrete prodO.
   Proof. intros ?? [??]; apply _. Qed.
+
+  Lemma pair_dist n (a1 a2 : A) (b1 b2 : B) :
+    (a1, b1) ≡{n}≡ (a2, b2) ↔ a1 ≡{n}≡ a2 ∧ b1 ≡{n}≡ b2.
+  Proof. reflexivity. Qed.
 End product.
 
 Global Arguments prodO : clear implicits.

iris/base_logic/bi.v

@@ -13,8 +13,7 @@ Local Existing Instance entails_po.
 Lemma uPred_bi_mixin (M : ucmra) :
   BiMixin
     uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
-    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
-    uPred_persistently.
+    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand.
 Proof.
   split.
   - exact: entails_po.
@@ -27,7 +26,6 @@ Proof.
   - exact: exist_ne.
   - exact: sep_ne.
   - exact: wand_ne.
-  - exact: persistently_ne.
   - exact: pure_intro.
   - exact: pure_elim'.
   - exact: and_elim_l.
@@ -49,6 +47,15 @@ Proof.
   - exact: sep_assoc'.
   - exact: wand_intro_r.
   - exact: wand_elim_l'.
+Qed.
+
+Lemma uPred_bi_persistently_mixin (M : ucmra) :
+  BiPersistentlyMixin
+    uPred_entails uPred_emp uPred_and
+    (@uPred_exist M) uPred_sep uPred_persistently.
+Proof.
+  split.
+  - exact: persistently_ne.
   - exact: persistently_mono.
   - exact: persistently_idemp_2.
   - (* emp ⊢ <pers> emp (ADMISSIBLE) *)
@@ -96,7 +103,8 @@ Qed.
 Canonical Structure uPredI (M : ucmra) : bi :=
   {| bi_ofe_mixin := ofe_mixin_of (uPred M);
      bi_bi_mixin := uPred_bi_mixin M;
-     bi_bi_later_mixin := uPred_bi_later_mixin M |}.
+     bi_bi_later_mixin := uPred_bi_later_mixin M;
+     bi_bi_persistently_mixin := uPred_bi_persistently_mixin M |}.
 
 Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
 Proof.

iris/base_logic/lib/fancy_updates.v

@@ -132,20 +132,42 @@ Qed.
 
 (** * [fupd] soundness lemmas *)
 
+(** "Unfolding" soundness stamement for no-LC fupd:
+This exposes that when initializing the [invGS_gen], we can provide
+a general lemma that lets one unfold a [|={E1, E2}=> P] into a basic update
+while also carrying around some frame [ω E] that tracks the current mask.
+We also provide a bunch of later credits for consistency,
+but there is no way to use them since this is a [HasNoLc] lemma. *)
+Lemma fupd_soundness_no_lc_unfold `{!invGpreS Σ} m E :
+  ⊢ |==> ∃ `(Hws: invGS_gen HasNoLc Σ) (ω : coPset → iProp Σ),
+    £ m ∗ ω E ∗ □ (∀ E1 E2 P, (|={E1, E2}=> P) -∗ ω E1 ==∗ ◇ (ω E2 ∗ P)).
+Proof.
+  iMod wsat_alloc as (Hw) "[Hw HE]".
+  (* We don't actually want any credits, but we need the [lcGS]. *)
+  iMod (later_credits.le_upd.lc_alloc m) as (Hc) "[_ Hlc]".
+  set (Hi := InvG HasNoLc _ Hw Hc).
+  iExists Hi, (λ E, wsat ∗ ownE E)%I.
+  rewrite (union_difference_L E ⊤); [|set_solver].
+  rewrite ownE_op; [|set_solver].
+  iDestruct "HE" as "[HE _]". iFrame.
+  iIntros "!>!>" (E1 E2 P) "HP HwE".
+  rewrite fancy_updates.uPred_fupd_unseal
+          /fancy_updates.uPred_fupd_def -assoc /=.
+  by iApply ("HP" with "HwE").
+Qed.
+
 (** Note: the [_no_lc] soundness lemmas also allow generating later credits, but
   these cannot be used for anything. They are merely provided to enable making
   the adequacy proof generic in whether later credits are used. *)
 Lemma fupd_soundness_no_lc `{!invGpreS Σ} E1 E2 (P : iProp Σ) `{!Plain P} m :
   (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={E1,E2}=∗ P) → ⊢ P.
 Proof.
-  iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hw) "[Hw HE]".
-  (* We don't actually want any credits, but we need the [lcGS]. *)
-  iMod (later_credits.le_upd.lc_alloc m) as (Hc) "[_ Hc]".
-  set (Hi := InvG HasNoLc _ Hw Hc).
-  iAssert (|={⊤,E2}=> P)%I with "[Hc]" as "H".
-  { iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd; last done. }
-  rewrite uPred_fupd_unseal /uPred_fupd_def.
-  iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
+  iIntros (Hfupd).
+  apply later_soundness, bupd_soundness; [by apply later_plain|].
+  iMod fupd_soundness_no_lc_unfold as (hws ω) "(Hlc & Hω & #H)".
+  iMod ("H" with "[Hlc] Hω") as "H'".
+  { iMod (Hfupd with "Hlc") as "H'". iModIntro. iApply "H'". }
+  iDestruct "H'" as "[>H1 >H2]". by iFrame.
 Qed.
 
 Lemma fupd_soundness_lc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} :

iris/bi/interface.v

@@ -19,7 +19,6 @@ Section bi_mixin.
   Context (bi_exist : ∀ A, (A → PROP) → PROP).
   Context (bi_sep : PROP → PROP → PROP).
   Context (bi_wand : PROP → PROP → PROP).
-  Context (bi_persistently : PROP → PROP).
 
   Bind Scope bi_scope with PROP.
   Local Infix "⊢" := bi_entails.
@@ -36,7 +35,6 @@ Section bi_mixin.
     (bi_exist _ (λ x, .. (bi_exist _ (λ y, P%I)) ..)) : bi_scope.
   Local Infix "∗" := bi_sep : bi_scope.
   Local Infix "-∗" := bi_wand : bi_scope.
-  Local Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
 
   (** * Axioms for a general BI (logic of bunched implications) *)
 
@@ -64,7 +62,6 @@ Section bi_mixin.
       Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A);
     bi_mixin_sep_ne : NonExpansive2 bi_sep;
     bi_mixin_wand_ne : NonExpansive2 bi_wand;
-    bi_mixin_persistently_ne : NonExpansive bi_persistently;
 
     (** Higher-order logic *)
     bi_mixin_pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝;
@@ -95,8 +92,40 @@ Section bi_mixin.
     bi_mixin_sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R);
     bi_mixin_wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R;
     bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
+  }.
+
+  (** We require any BI to have a persistence modality that carves out the
+  intuitionistic fragment of the separation logic. For logics such as Iris,
+  the persistence modality has a non-trivial definition (involving the [core] of
+  the camera). It is not clear whether a trivial definition exists: while
+  [<pers> P := False] comes close, it does not satisfy [later_persistently_1].
+  
+  However, for some simpler discrete BIs the persistence modality
+  can be defined as:
+
+    <pers> P := ⌜ emp ⊢ P ⌝
+
+  That is, [P] holds persistently if it holds without resources.
+
+  The nesting of the entailment below the pure embedding ⌜ ⌝ only works for
+  discrete BIs: Non-expansiveness of [<pers>] relies on [dist] ignoring the
+  step-index.
+
+  To prove the rule [<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> Ψ a] the BI furthermore
+  needs to satisfy the "existential property": [emp ⊢ ∃ x, Φ x] implies
+  [∃ x, emp ⊢ Φ x].
+
+  This construction is formalized by the smart constructor
+  [bi_persistently_mixin_discrete] for [BiPersistentlyMixin]. See
+  [tests/heapprop] and [tests/heapprop_affine] for examples of how to use this
+  smart constructor. *)
+
+  Context (bi_persistently : PROP → PROP).
+  Local Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
+
+  Record BiPersistentlyMixin := {
+    bi_mixin_persistently_ne : NonExpansive bi_persistently;
 
-    (** Persistently *)
     (* In the ordered RA model: Holds without further assumptions. *)
     bi_mixin_persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q;
     (* In the ordered RA model: `core` is idempotent *)
@@ -121,6 +150,50 @@ Section bi_mixin.
     bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;
   }.
 
+  Lemma bi_persistently_mixin_discrete :
+    (∀ n (P Q : PROP), P ≡{n}≡ Q → P ≡ Q) →
+    (∀ {A} (Φ : A → PROP), (emp ⊢ ∃ x, Φ x) → ∃ x, emp ⊢ Φ x) →
+    (∀ P : PROP, (<pers> P)%I = ⌜ emp ⊢ P ⌝%I) →
+    BiMixin →
+    BiPersistentlyMixin.
+  Proof.
+    intros Hdiscrete Hex Hpers Hbi. pose proof (bi_mixin_entails_po Hbi).
+    split.
+    - (* [NonExpansive bi_persistently] *)
+      intros n P Q [HPQ HQP]%Hdiscrete%(bi_mixin_equiv_entails Hbi).
+      rewrite !Hpers. apply (bi_mixin_pure_ne Hbi). split=> ?; by etrans.
+    - (*[(P ⊢ Q) → <pers> P ⊢ <pers> Q] *)
+      intros P Q HPQ. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> ?.
+      apply (bi_mixin_pure_intro Hbi). by trans P.
+    - (* [<pers> P ⊢ <pers> <pers> P] *)
+      intros P. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> ?.
+      by do 2 apply (bi_mixin_pure_intro Hbi).
+    - (* [emp ⊢ <pers> emp] *)
+      rewrite Hpers. by apply (bi_mixin_pure_intro Hbi).
+    - (* [<pers> P ∧ <pers> Q ⊢ <pers> (P ∧ Q)] *)
+      intros P Q. rewrite !Hpers.
+      apply (bi_mixin_impl_elim_l' Hbi). apply (bi_mixin_pure_elim' Hbi)=> ?.
+      apply (bi_mixin_impl_intro_r Hbi).
+      etrans; [apply (bi_mixin_and_elim_r Hbi)|].
+      apply (bi_mixin_pure_elim' Hbi)=> ?.
+      apply (bi_mixin_pure_intro Hbi). by apply (bi_mixin_and_intro Hbi).
+    - (* [<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> Ψ a] *)
+      intros A Φ. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> /Hex [x ?].
+      etrans; [|apply (bi_mixin_exist_intro Hbi x)]; simpl.
+      rewrite Hpers. by apply (bi_mixin_pure_intro Hbi).
+    - (* [<pers> P ∗ Q ⊢ <pers> P] *)
+      intros P Q. rewrite !Hpers.
+      apply (bi_mixin_wand_elim_l' Hbi). apply (bi_mixin_pure_elim' Hbi)=> ?.
+      apply (bi_mixin_wand_intro_r Hbi). by apply (bi_mixin_pure_intro Hbi).
+    - (* [<pers> P ∧ Q ⊢ P ∗ Q] *)
+      intros P Q. rewrite !Hpers.
+      apply (bi_mixin_impl_elim_l' Hbi). apply (bi_mixin_pure_elim' Hbi)=> ?.
+      apply (bi_mixin_impl_intro_r Hbi).
+      etrans; [apply (bi_mixin_and_elim_r Hbi)|].
+      etrans; [apply (bi_mixin_emp_sep_1 Hbi)|].
+      by apply (bi_mixin_sep_mono Hbi).
+  Qed.
+
   (** We equip any BI with a later modality. This avoids an additional layer in
   the BI hierachy and improves performance significantly (see Iris issue #303).
 
@@ -157,7 +230,7 @@ Section bi_mixin.
     BiMixin → BiLaterMixin.
   Proof.
     intros Hlater Hbi. pose proof (bi_mixin_entails_po Hbi).
-    split; repeat intro; rewrite ?Hlater ?Hequiv //.
+    split; repeat intro; rewrite ?Hlater //.
     - apply (bi_mixin_forall_intro Hbi)=> a.
       etrans; [apply (bi_mixin_forall_elim Hbi a)|]. by rewrite Hlater.
     - etrans; [|apply (bi_mixin_or_intro_r Hbi)].
@@ -194,7 +267,9 @@ Structure bi := Bi {
   bi_ofe_mixin : OfeMixin bi_car;
   bi_cofe_aux : Cofe (Ofe bi_car bi_ofe_mixin);
   bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
-                        bi_exist bi_sep bi_wand bi_persistently;
+                        bi_exist bi_sep bi_wand;
+  bi_bi_persistently_mixin :
+    BiPersistentlyMixin bi_entails bi_emp bi_and bi_exist bi_sep bi_persistently;
   bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
                                    bi_forall bi_exist bi_sep bi_persistently bi_later;
 }.
@@ -326,7 +401,7 @@ Proof. eapply bi_mixin_sep_ne, bi_bi_mixin. Qed.
 Global Instance wand_ne : NonExpansive2 (@bi_wand PROP).
 Proof. eapply bi_mixin_wand_ne, bi_bi_mixin. Qed.
 Global Instance persistently_ne : NonExpansive (@bi_persistently PROP).
-Proof. eapply bi_mixin_persistently_ne, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_ne, bi_bi_persistently_mixin. Qed.
 
 (* Higher-order logic *)
 Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
@@ -381,24 +456,28 @@ Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
 
 (* Persistently *)
 Lemma persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q.
-Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_mono, bi_bi_persistently_mixin. Qed.
 Lemma persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P.
-Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_persistently_mixin. Qed.
 
 Lemma persistently_emp_2 : emp ⊢@{PROP} <pers> emp.
-Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_emp_2, bi_bi_persistently_mixin. Qed.
 
 Lemma persistently_and_2 (P Q : PROP) :
   ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q).
-Proof. eapply bi_mixin_persistently_and_2, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_and_2, bi_bi_persistently_mixin. Qed.
 Lemma persistently_exist_1 {A} (Ψ : A → PROP) :
   <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a).
-Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_exist_1, bi_bi_persistently_mixin. Qed.
 
 Lemma persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P.
-Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
+Proof.
+  eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_persistently_mixin.
+Qed.
 Lemma persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q.
-Proof. eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_mixin. Qed.
+Proof.
+  eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_persistently_mixin.
+Qed.
 
 (* Later *)
 Global Instance later_ne : NonExpansive (@bi_later PROP).

iris/bi/monpred.v

@@ -315,8 +315,7 @@ Section instances.
 
   Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
     monPred_entails monPred_emp monPred_pure monPred_and monPred_or
-    monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand
-    monPred_persistently.
+    monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand.
   Proof.
     split; rewrite ?monPred_defs.monPred_unseal;
       try by (split=> ? /=; repeat f_equiv).
@@ -354,6 +353,15 @@ Section instances.
       apply bi.wand_intro_r. by rewrite -HR /= !Hij.
     - intros P Q R [HP]. split=> i. apply bi.wand_elim_l'.
       rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
+  Qed.
+
+  Lemma monPred_bi_persistently_mixin :
+    BiPersistentlyMixin (PROP:=monPred I PROP)
+      monPred_entails monPred_emp monPred_and
+      monPred_exist monPred_sep monPred_persistently.
+  Proof.
+    split; rewrite ?monPred_defs.monPred_unseal;
+      try by (split=> ? /=; repeat f_equiv).
     - intros P Q [?]. split=> i /=. by f_equiv.
     - intros P. split=> i. by apply bi.persistently_idemp_2.
     - split=> i. by apply bi.persistently_emp_intro.
@@ -386,7 +394,9 @@ Section instances.
   Qed.
 
   Canonical Structure monPredI : bi :=
-    {| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin;
+    {| bi_ofe_mixin := monPred_ofe_mixin;
+       bi_bi_mixin := monPred_bi_mixin;
+       bi_bi_persistently_mixin := monPred_bi_persistently_mixin;
        bi_bi_later_mixin := monPred_bi_later_mixin |}.
 
   (** We restate the unsealing lemmas so that they also unfold the BI layer. The

iris/si_logic/bi.v

@@ -20,8 +20,7 @@ Local Existing Instance entails_po.
 Lemma siProp_bi_mixin :
   BiMixin
     siProp_entails siProp_emp siProp_pure siProp_and siProp_or siProp_impl
-    (@siProp_forall) (@siProp_exist) siProp_sep siProp_wand
-    siProp_persistently.
+    (@siProp_forall) (@siProp_exist) siProp_sep siProp_wand.
 Proof.
   split.
   - exact: entails_po.
@@ -34,7 +33,6 @@ Proof.
   - exact: exist_ne.
   - exact: and_ne.
   - exact: impl_ne.
-  - solve_proper.
   - exact: pure_intro.
   - exact: pure_elim'.
   - exact: and_elim_l.
@@ -68,6 +66,15 @@ Proof.
     apply impl_intro_r.
   - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
     apply impl_elim_l'.
+Qed.
+
+Lemma siProp_bi_persistently_mixin :
+  BiPersistentlyMixin
+    siProp_entails siProp_emp siProp_and
+    (@siProp_exist) siProp_sep siProp_persistently.
+Proof.
+  split.
+  - solve_proper.
   - (* (P ⊢ Q) → <pers> P ⊢ <pers> Q *)
     done.
   - (* <pers> P ⊢ <pers> <pers> P *)
@@ -119,7 +126,9 @@ Qed.
 
 Canonical Structure siPropI : bi :=
   {| bi_ofe_mixin := ofe_mixin_of siProp;
-     bi_bi_mixin := siProp_bi_mixin; bi_bi_later_mixin := siProp_bi_later_mixin |}.
+     bi_bi_mixin := siProp_bi_mixin;
+     bi_bi_persistently_mixin := siProp_bi_persistently_mixin;
+     bi_bi_later_mixin := siProp_bi_later_mixin |}.
 
 Global Instance siProp_pure_forall : BiPureForall siPropI.
 Proof. exact: @pure_forall_2. Qed.

iris_unstable/algebra/monotone.v

@@ -6,241 +6,186 @@ 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}.
+(** 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:
+
+   [R x y] iff [to_mra x ≼ to_mra y]
+
+Here, [≼] is the extension order of the [mra R] resource algebra. This is
+exactly what the lemma [to_mra_included] shows.
+
+This resource algebra is useful for reasoning about monotonicity. See the
+following paper for more details ([to_mra] is called "principal"):
+
+  Reasoning About Monotonicity in Separation Logic
+  Amin Timany and Lars Birkedal
+  in Certified Programs and Proofs (CPP) 2021
+
+Note that unlike most Iris algebra constructions [mra A] works on [A : Type],
+not on [A : ofe]. See the comment at [mraO] below for more information. If [A]
+has an [Equiv A] (i.e., is a setoid), there are some results at the bottom of
+this file. *)
+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 below (a : A) (x : mra R) := ∃ b, b ∈ x ∧ R a b.
+  (** Pronounced [a] is below [x]. *)
+  Local Definition mra_below (a : A) (x : mra R) := ∃ b, b ∈ mra_car x ∧ R a b.
 
-  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.
+  Local Lemma mra_below_to_mra a b : mra_below a (to_mra b) ↔ R a b.
+  Proof. set_solver. Qed.
 
-  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.
-
-  Local Instance mra_equiv : Equiv (mra R) :=
-    λ x y, ∀ a, below a x ↔ below a y.
+  (* 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.
-    split; [by firstorder|by firstorder|].
-    intros ??? Heq1 Heq2 ?; split; intros ?;
-      [apply Heq2; apply Heq1|apply Heq1; apply Heq2]; done.
-  Qed.
+  Proof. unfold mra_equiv; split; intros ?; naive_solver. Qed.
 
-  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:
 
-Global Arguments mraO [_] _.
+    cmra_extend :
+      x ≡{n}≡ y1 ⋅ y2 →
+      ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ y1 ≡{n}≡ z1 ∧ y2 ≡{n}≡ z2
 
-(* CMRA *)
-Section cmra.
-  Context {A : Type} {R : relation A}.
-  Implicit Types a b : A.
-  Implicit Types x y : mra R.
+  To prove this, assume ([⋅] is defined as [++], see [mra_op]):
+
+    x ≡{n}≡ y1 ++ y2
+
+  When defining [dist] as the step-indexed version of [mra_equiv], this means:
+
+    ∀ n' a, n' ≤ n →
+            mra_below a x n' ↔ mra_below a y1 n' ∨ mra_below a y2 n'
+
+  From this assumption it is not clear how to obtain witnesses [z1] and [z2]. *)
+  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.
-
-  Global Instance principal_proper
-         `{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
-    Proper ((≡) ==> (≡)) (principal R) := ne_proper _.
+  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.
 
-  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_equiv_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/heapprop.v

@@ -94,7 +94,7 @@ Local Definition heapProp_wand_unseal:
   @heapProp_wand = @heapProp_wand_def := seal_eq heapProp_wand_aux.
 
 Local Definition heapProp_persistently_def (P : heapProp) : heapProp :=
-  {| heapProp_holds σ := P ∅ |}.
+  heapProp_pure (heapProp_entails heapProp_emp P).
 Local Definition heapProp_persistently_aux : seal (@heapProp_persistently_def).
 Proof. by eexists. Qed.
 Definition heapProp_persistently := unseal heapProp_persistently_aux.
@@ -120,7 +120,7 @@ Section mixins.
     BiMixin
       heapProp_entails heapProp_emp heapProp_pure heapProp_and heapProp_or
       heapProp_impl (@heapProp_forall) (@heapProp_exist)
-      heapProp_sep heapProp_wand heapProp_persistently.
+      heapProp_sep heapProp_wand.
   Proof.
     split.
     - (* [PreOrder heapProp_entails] *)
@@ -145,8 +145,6 @@ Section mixins.
       unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
     - (* [NonExpansive2 bi_wand] *)
       unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
-    - (* [NonExpansive2 bi_persistently] *)
-      unseal=> n P1 P2 [HP]; split; naive_solver.
     - (* [φ → P ⊢ ⌜ φ ⌝] *)
       unseal=> φ P ?; by split.
     - (* [(φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P] *)
@@ -193,21 +191,18 @@ Section mixins.
       unseal=> P Q R [HPQR]; split=> σ1 ? σ2 ??. apply HPQR. by exists σ1, σ2.
     - (* [(P ⊢ Q -∗ R) → P ∗ Q ⊢ R] *)
       unseal=> P Q R [HPQR]; split; intros ? (σ1&σ2&->&?&?&?). by apply HPQR.
-    - (* [(P ⊢ Q) → <pers> P ⊢ <pers> Q] *)
-      unseal=> P Q [HPQ]; split=> σ. apply HPQ.
-    - (* [<pers> P ⊢ <pers> <pers> P] *)
-      unseal=> P; split=> σ; done.
-    - (* [emp ⊢ <pers> emp] *)
-      unseal; split=> σ; done.
-    - (* [(∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a)] *)
-      unseal=> A Ψ; split=> σ; done.
-    - (* [<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a)] *)
-      unseal=> A Ψ; split=> σ; done.
-    - (* [<pers> P ∗ Q ⊢ <pers> P] *)
-      unseal=> P Q; split; intros ? (σ1&σ2&->&?&?&?); done.
-    - (* [<pers> P ∧ Q ⊢ P ∗ Q] *)
-      unseal=> P Q; split=> σ [??]. eexists ∅, σ. rewrite left_id_L.
-      split_and!; done || apply map_disjoint_empty_l.
+  Qed.
+
+  Lemma heapProp_bi_persistently_mixin :
+    BiPersistentlyMixin
+      heapProp_entails heapProp_emp heapProp_and
+      (@heapProp_exist) heapProp_sep heapProp_persistently.
+  Proof.
+    eapply bi_persistently_mixin_discrete, heapProp_bi_mixin; [done|..].
+    - (* [(emp ⊢ ∃ x, Φ x) → ∃ x, emp ⊢ Φ x] *)
+      unseal. intros A Φ [H]. destruct (H ∅) as [x ?]; [done|].
+      exists x. by split=> σ ->.
+    - by rewrite heapProp_persistently_unseal.
   Qed.
 
   Lemma heapProp_bi_later_mixin :
@@ -220,7 +215,9 @@ End mixins.
 
 Canonical Structure heapPropI : bi :=
   {| bi_ofe_mixin := ofe_mixin_of heapProp;
-     bi_bi_mixin := heapProp_bi_mixin; bi_bi_later_mixin := heapProp_bi_later_mixin |}.
+     bi_bi_mixin := heapProp_bi_mixin;
+     bi_bi_persistently_mixin := heapProp_bi_persistently_mixin;
+     bi_bi_later_mixin := heapProp_bi_later_mixin |}.
 
 Global Instance heapProp_pure_forall : BiPureForall heapPropI.
 Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed.

tests/heapprop_affine.v

+From stdpp Require Import gmap.
+From iris.bi Require Import interface.
+From iris.proofmode Require Import tactics.
+From iris.prelude Require Import options.
+
+(** This file constructs a simple non step-indexed affine separation logic as
+predicates over heaps (modeled as maps from integer locations to integer values).
+It shows that Iris's [bi] canonical structure can be inhabited, and the Iris
+proof mode can be used to prove lemmas in this separation logic. *)
+Definition loc := Z.
+Definition val := Z.
+
+Record heapProp := HeapProp {
+  heapProp_holds :> gmap loc val → Prop;
+  heapProp_closed σ1 σ2 : heapProp_holds σ1 → σ1 ⊆ σ2 → heapProp_holds σ2;
+}.
+Global Arguments heapProp_holds : simpl never.
+Add Printing Constructor heapProp.
+
+Section ofe.
+  Inductive heapProp_equiv' (P Q : heapProp) : Prop :=
+    { heapProp_in_equiv : ∀ σ, P σ ↔ Q σ }.
+  Local Instance heapProp_equiv : Equiv heapProp := heapProp_equiv'.
+  Local Instance heapProp_equivalence : Equivalence (≡@{heapProp}).
+  Proof. split; repeat destruct 1; constructor; naive_solver. Qed.
+  Canonical Structure heapPropO := discreteO heapProp.
+End ofe.
+
+(** logical entailement *)
+Inductive heapProp_entails (P Q : heapProp) : Prop :=
+  { heapProp_in_entails : ∀ σ, P σ → Q σ }.
+
+(** logical connectives *)
+Local Program Definition heapProp_pure_def (φ : Prop) : heapProp :=
+  {| heapProp_holds _ := φ |}.
+Solve Obligations with done.
+Local Definition heapProp_pure_aux : seal (@heapProp_pure_def). Proof. by eexists. Qed.
+Definition heapProp_pure := unseal heapProp_pure_aux.
+Local Definition heapProp_pure_unseal :
+  @heapProp_pure = @heapProp_pure_def := seal_eq heapProp_pure_aux.
+
+Definition heapProp_emp : heapProp := heapProp_pure True.
+
+Local Program Definition heapProp_and_def (P Q : heapProp) : heapProp :=
+  {| heapProp_holds σ := P σ ∧ Q σ |}.
+Solve Obligations with naive_solver eauto using heapProp_closed.
+Local Definition heapProp_and_aux : seal (@heapProp_and_def). Proof. by eexists. Qed.
+Definition heapProp_and := unseal heapProp_and_aux.
+Local Definition heapProp_and_unseal:
+  @heapProp_and = @heapProp_and_def := seal_eq heapProp_and_aux.
+
+Local Program Definition heapProp_or_def (P Q : heapProp) : heapProp :=
+  {| heapProp_holds σ := P σ ∨ Q σ |}.
+Solve Obligations with naive_solver eauto using heapProp_closed.
+Local Definition heapProp_or_aux : seal (@heapProp_or_def). Proof. by eexists. Qed.
+Definition heapProp_or := unseal heapProp_or_aux.
+Local Definition heapProp_or_unseal:
+  @heapProp_or = @heapProp_or_def := seal_eq heapProp_or_aux.
+
+Local Program Definition heapProp_impl_def (P Q : heapProp) : heapProp :=
+  {| heapProp_holds σ := ∀ σ', σ ⊆ σ' → P σ' → Q σ' |}.
+Next Obligation. intros P Q σ1 σ2 HPQ ? σ' ?; simpl in *. apply HPQ. by etrans. Qed.
+Local Definition heapProp_impl_aux : seal (@heapProp_impl_def). Proof. by eexists. Qed.
+Definition heapProp_impl := unseal heapProp_impl_aux.
+Local Definition heapProp_impl_unseal :
+  @heapProp_impl = @heapProp_impl_def := seal_eq heapProp_impl_aux.
+
+Local Program Definition heapProp_forall_def {A} (Ψ : A → heapProp) : heapProp :=
+  {| heapProp_holds σ := ∀ a, Ψ a σ |}.
+Solve Obligations with naive_solver eauto using heapProp_closed.
+Local Definition heapProp_forall_aux : seal (@heapProp_forall_def). Proof. by eexists. Qed.
+Definition heapProp_forall {A} := unseal heapProp_forall_aux A.
+Local Definition heapProp_forall_unseal :
+  @heapProp_forall = @heapProp_forall_def := seal_eq heapProp_forall_aux.
+
+Local Program Definition heapProp_exist_def {A} (Ψ : A → heapProp) : heapProp :=
+  {| heapProp_holds σ := ∃ a, Ψ a σ |}.
+Solve Obligations with naive_solver eauto using heapProp_closed.
+Local Definition heapProp_exist_aux : seal (@heapProp_exist_def). Proof. by eexists. Qed.
+Definition heapProp_exist {A} := unseal heapProp_exist_aux A.
+Local Definition heapProp_exist_unseal :
+  @heapProp_exist = @heapProp_exist_def := seal_eq heapProp_exist_aux.
+
+Local Program Definition heapProp_sep_def (P Q : heapProp) : heapProp :=
+  {| heapProp_holds σ := ∃ σ1 σ2, σ = σ1 ∪ σ2 ∧ σ1 ##ₘ σ2 ∧ P σ1 ∧ Q σ2 |}.
+Next Obligation.
+  intros P Q σ1 σ2 (σ11 & σ12 & -> & ? & ? & ?) ?.
+  assert (σ11 ⊆ σ2) by (by etrans; [apply map_union_subseteq_l|]).
+  exists σ11, (σ2 ∖ σ11). split_and!; [| |done|].
+  - by rewrite map_difference_union.
+  - by apply map_disjoint_difference_r.
+  - eapply heapProp_closed; [done|].
+    apply map_union_reflecting_l with σ11; [done|..].
+    + by apply map_disjoint_difference_r.
+    + by rewrite map_difference_union.
+Qed.
+Local Definition heapProp_sep_aux : seal (@heapProp_sep_def). Proof. by eexists. Qed.
+Definition heapProp_sep := unseal heapProp_sep_aux.
+Local Definition heapProp_sep_unseal:
+  @heapProp_sep = @heapProp_sep_def := seal_eq heapProp_sep_aux.
+
+Local Program Definition heapProp_wand_def (P Q : heapProp) : heapProp :=
+  {| heapProp_holds σ := ∀ σ', σ ##ₘ σ' → P σ' → Q (σ ∪ σ') |}.
+Next Obligation.
+  intros P Q σ1 σ2 HPQ ? σ' ??; simpl in *.
+  apply heapProp_closed with (σ1 ∪ σ'); [by eauto using map_disjoint_weaken_l|].
+  by apply map_union_mono_r.
+Qed.
+Local Definition heapProp_wand_aux : seal (@heapProp_wand_def). Proof. by eexists. Qed.
+Definition heapProp_wand := unseal heapProp_wand_aux.
+Local Definition heapProp_wand_unseal:
+  @heapProp_wand = @heapProp_wand_def := seal_eq heapProp_wand_aux.
+
+Local Definition heapProp_persistently_def (P : heapProp) : heapProp :=
+  heapProp_pure (heapProp_entails heapProp_emp P).
+Local Definition heapProp_persistently_aux : seal (@heapProp_persistently_def).
+Proof. by eexists. Qed.
+Definition heapProp_persistently := unseal heapProp_persistently_aux.
+Local Definition heapProp_persistently_unseal:
+  @heapProp_persistently = @heapProp_persistently_def := seal_eq heapProp_persistently_aux.
+
+(** Iris's [bi] class requires the presence of a later modality, but for non
+step-indexed logics, it can be defined as the identity. *)
+Definition heapProp_later (P : heapProp) : heapProp := P.
+
+Local Definition heapProp_unseal :=
+  (heapProp_pure_unseal, heapProp_and_unseal,
+   heapProp_or_unseal, heapProp_impl_unseal, heapProp_forall_unseal,
+   heapProp_exist_unseal, heapProp_sep_unseal, heapProp_wand_unseal,
+   heapProp_persistently_unseal).
+Ltac unseal := rewrite !heapProp_unseal /=.
+
+Section mixins.
+  (** Enable [simpl] locally, which is useful for proofs in the model. *)
+  Local Arguments heapProp_holds !_ _ /.
+
+  Lemma heapProp_bi_mixin :
+    BiMixin
+      heapProp_entails heapProp_emp heapProp_pure heapProp_and heapProp_or
+      heapProp_impl (@heapProp_forall) (@heapProp_exist)
+      heapProp_sep heapProp_wand.
+  Proof.
+    split.
+    - (* [PreOrder heapProp_entails] *)
+      split; repeat destruct 1; constructor; naive_solver.
+    - (* [P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P)] *)
+      intros P Q; split.
+      + intros [HPQ]; split; split; naive_solver.
+      + intros [[HPQ] [HQP]]; split; naive_solver.
+    - (* [Proper (iff ==> dist n) bi_pure] *)
+      unseal=> n φ1 φ2 Hφ; split; naive_solver.
+    - (* [NonExpansive2 bi_and] *)
+      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+    - (* [NonExpansive2 bi_or] *)
+      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+    - (* [NonExpansive2 bi_impl] *)
+      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+    - (* [Proper (pointwise_relation _ (dist n) ==> dist n) (bi_forall A)] *)
+      unseal=> A n Φ1 Φ2 HΦ; split=> σ /=; split=> ? x; by apply HΦ.
+    - (* [Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A)] *)
+      unseal=> A n Φ1 Φ2 HΦ; split=> σ /=; split=> -[x ?]; exists x; by apply HΦ.
+    - (* [NonExpansive2 bi_sep] *)
+      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+    - (* [NonExpansive2 bi_wand] *)
+      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+    - (* [φ → P ⊢ ⌜ φ ⌝] *)
+      unseal=> φ P ?; by split.
+    - (* [(φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P] *)
+      unseal=> φ P HP; split=> σ ?. by apply HP.
+    - (* [P ∧ Q ⊢ P] *)
+      unseal=> P Q; split=> σ [??]; done.
+    - (* [P ∧ Q ⊢ Q] *)
+      unseal=> P Q; split=> σ [??]; done.
+    - (* [(P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R] *)
+      unseal=> P Q R [HPQ] [HPR]; split=> σ; split; auto.
+    - (* [P ⊢ P ∨ Q] *)
+      unseal=> P Q; split=> σ; by left.
+    - (* [Q ⊢ P ∨ Q] *)
+      unseal=> P Q; split=> σ; by right.
+    - (* [(P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R] *)
+      unseal=> P Q R [HPQ] [HQR]; split=> σ [?|?]; auto.
+    - (* [(P ∧ Q ⊢ R) → P ⊢ Q → R] *)
+      unseal=> P Q R HPQR; split=> σ ? σ' ??. apply HPQR.
+      split; eauto using heapProp_closed.
+    - (* [(P ⊢ Q → R) → P ∧ Q ⊢ R] *)
+      unseal=> P Q R HPQR; split=> σ [??]. by eapply HPQR.
+    - (* [(∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a] *)
+      unseal=> A P Ψ HPΨ; split=> σ ? a. by apply HPΨ.
+    - (* [(∀ a, Ψ a) ⊢ Ψ a] *)
+      unseal=> A Ψ a; split=> σ ?; done.
+    - (* [Ψ a ⊢ ∃ a, Ψ a] *)
+      unseal=> A Ψ a; split=> σ ?. by exists a.
+    - (* [(∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q] *)
+      unseal=> A Φ Q HΦQ; split=> σ [a ?]. by apply (HΦQ a).
+    - (* [(P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'] *)
+      unseal=> P P' Q Q' [HPQ] [HP'Q']; split; naive_solver.
+    - (* [P ⊢ emp ∗ P] *)
+      unfold heapProp_emp; unseal=> P; split=> σ ? /=.
+      eexists ∅, σ. rewrite left_id_L.
+      split_and!; done || apply map_disjoint_empty_l.
+    - (* [emp ∗ P ⊢ P] *)
+      unfold heapProp_emp; unseal=> P; split; intros ? (?&σ&->&?&_&?).
+      eapply heapProp_closed; [done|]. by apply map_union_subseteq_r.
+    - (* [P ∗ Q ⊢ Q ∗ P] *)
+      unseal=> P Q; split; intros ? (σ1&σ2&->&?&?&?).
+      exists σ2, σ1. by rewrite map_union_comm.
+    - (* [(P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R)] *)
+      unseal=> P Q R; split; intros ? (?&σ3&->&?&(σ1&σ2&->&?&?&?)&?).
+      exists σ1, (σ2 ∪ σ3). split_and!; [by rewrite assoc_L|solve_map_disjoint|done|].
+      exists σ2, σ3; split_and!; [done|solve_map_disjoint|done..].
+    - (* [(P ∗ Q ⊢ R) → P ⊢ Q -∗ R] *)
+      unseal=> P Q R [HPQR]; split=> σ1 ? σ2 ??. apply HPQR. by exists σ1, σ2.
+    - (* [(P ⊢ Q -∗ R) → P ∗ Q ⊢ R] *)
+      unseal=> P Q R [HPQR]; split; intros ? (σ1&σ2&->&?&?&?). by apply HPQR.
+  Qed.
+
+  Lemma heapProp_bi_persistently_mixin :
+    BiPersistentlyMixin
+      heapProp_entails heapProp_emp heapProp_and
+      (@heapProp_exist) heapProp_sep heapProp_persistently.
+  Proof.
+    eapply bi_persistently_mixin_discrete, heapProp_bi_mixin; [done|..].
+    - (* The "existential property" [(emp ⊢ ∃ x, Φ x) → ∃ x, emp ⊢ Φ x]. For an
+      affine BI the proof relies on there being a smallest resource/the unit
+      (here the empty heap [∅]). *)
+      unfold heapProp_emp. unseal. intros A Φ [H].
+      destruct (H ∅) as [x ?]; [done|]. exists x. split=> σ _.
+      eapply heapProp_closed; [done|]. by apply map_empty_subseteq.
+    - by rewrite heapProp_persistently_unseal.
+  Qed.
+
+  Lemma heapProp_bi_later_mixin :
+    BiLaterMixin
+      heapProp_entails heapProp_pure heapProp_or heapProp_impl
+      (@heapProp_forall) (@heapProp_exist)
+      heapProp_sep heapProp_persistently heapProp_later.
+  Proof. eapply bi_later_mixin_id; [done|apply heapProp_bi_mixin]. Qed.
+End mixins.
+
+Canonical Structure heapPropI : bi :=
+  {| bi_ofe_mixin := ofe_mixin_of heapProp;
+     bi_bi_mixin := heapProp_bi_mixin;
+     bi_bi_persistently_mixin := heapProp_bi_persistently_mixin;
+     bi_bi_later_mixin := heapProp_bi_later_mixin |}.
+
+Global Instance heapProp_pure_forall : BiPureForall heapPropI.
+Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed.
+
+Global Instance heapProp_affine : BiAffine heapPropI.
+Proof. exact: bi.True_intro. Qed.
+
+Lemma heapProp_proofmode_test {A} (P Q Q' R : heapProp) (Φ Ψ : A → heapProp) :
+  P ∗ Q ∗ Q' -∗ (* [Q'] is not used, to demonstrate affinity *)
+  □ R -∗
+  □ (R -∗ ∃ x, Φ x) -∗
+  ∃ x, Φ x ∗ Φ x ∗ P ∗ Q.
+Proof.
+  iIntros "(HP & HQ & HQ') #HR #HRΦ".
+  iDestruct ("HRΦ" with "HR") as (x) "#HΦ".
+  iExists x. iFrame. by iSplitL.
+Qed.

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.