Compare revisions

Robbert Krebbers · Robbert Krebbers · Robbert Krebbers · Ralf Jung · Robbert Krebbers · Robbert Krebbers
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -39,6 +39,11 @@ Coq 8.13 is no longer supported.
  (by Michael Sammler, Lennard Gäher, and Simon Spies).
 * Add `max_Z` and `mono_Z` cameras.
 * Add `dfrac_valid`.
+* Rename `Some_included_2` to `Some_included_mono`.
+* Consistently use `Some x ≼ Some y` to express the reflexive closure of
+  `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.
 **Changes in `bi`:**
@@ -94,6 +99,8 @@ Coq 8.13 is no longer supported.
    `iDestruct`/`iCombine`/`iSplitL`/`iSplitR` should be used instead.
 * 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`
 **Changes in `proofmode`:**

--- a/_CoqProject
+++ b/_CoqProject
@@ -50,6 +50,7 @@ iris/algebra/ufrac.v
 iris/algebra/reservation_map.v
 iris/algebra/dyn_reservation_map.v
 iris/algebra/max_prefix_list.v
+iris/algebra/mra.v
 iris/algebra/lib/excl_auth.v
 iris/algebra/lib/frac_auth.v
 iris/algebra/lib/ufrac_auth.v
@@ -184,7 +185,6 @@ iris_unstable/algebra/list.v
 iris_unstable/base_logic/algebra.v
 iris_unstable/base_logic/mono_list.v
 iris_unstable/heap_lang/interpreter.v
-iris_unstable/algebra/monotone.v
 iris_deprecated/base_logic/auth.v
 iris_deprecated/base_logic/sts.v

--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -17,6 +17,9 @@ Notation "(⋅)" := op (only parsing) : stdpp_scope.
   reflexivity.  However, if we used [option A], the following would no longer
   hold:
     x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2
+   If you need the reflexive closure of the inclusion relation, you can use
+   [Some a ≼ Some b]. There are various [Some_included] lemmas that help
+   deal with propositions of this shape.
 *)
 Definition included {A} `{!Equiv A, !Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
 Infix "≼" := included (at level 70) : stdpp_scope.
@@ -1414,6 +1417,8 @@ Section option.
    right. exists a, b. by rewrite {3}Hab.
  Qed.
+  (* See below for more [included] lemmas. *)
  Lemma option_cmra_mixin : CmraMixin (option A).
  Proof.
    apply cmra_total_mixin.
@@ -1479,6 +1484,8 @@ Section option.
  Lemma cmra_opM_opM_swap_L `{!LeibnizEquiv A} a mb mc :
    a ⋅? mb ⋅? mc = a ⋅? mc ⋅? mb.
  Proof. by rewrite !cmra_opM_opM_assoc_L (comm_L _ mb). Qed.
+  Lemma cmra_opM_fmap_Some ma1 ma2 : ma1 ⋅? (Some <$> ma2) = ma1 ⋅ ma2.
+  Proof. by destruct ma1, ma2. Qed.
  Global Instance Some_core_id a : CoreId a → CoreId (Some a).
  Proof. by constructor. Qed.
@@ -1499,10 +1506,34 @@ Section option.
  Lemma Some_includedN n a b : Some a ≼{n} Some b ↔ a ≡{n}≡ b ∨ a ≼{n} b.
  Proof. rewrite option_includedN; naive_solver. Qed.
+  Lemma Some_includedN_1 n a b : Some a ≼{n} Some b → a ≡{n}≡ b ∨ a ≼{n} b.
+  Proof. rewrite Some_includedN. auto. Qed.
+  Lemma Some_includedN_2 n a b : a ≡{n}≡ b ∨ a ≼{n} b → Some a ≼{n} Some b.
+  Proof. rewrite Some_includedN. auto. Qed.
+  Lemma Some_includedN_mono n a b : a ≼{n} b → Some a ≼{n} Some b.
+  Proof. rewrite Some_includedN. auto. Qed.
+  Lemma Some_includedN_is_Some n x mb : Some x ≼{n} mb → is_Some mb.
+  Proof. rewrite option_includedN. naive_solver. Qed.
  Lemma Some_included a b : Some a ≼ Some b ↔ a ≡ b ∨ a ≼ b.
  Proof. rewrite option_included; naive_solver. Qed.
-  Lemma Some_included_2 a b : a ≼ b → Some a ≼ Some b.
+  Lemma Some_included_1 a b : Some a ≼ Some b → a ≡ b ∨ a ≼ b.
-  Proof. rewrite Some_included; eauto. Qed.
+  Proof. rewrite Some_included. auto. Qed.
+  Lemma Some_included_2 a b : a ≡ b ∨ a ≼ b → Some a ≼ Some b.
+  Proof. rewrite Some_included. auto. Qed.
+  Lemma Some_included_mono a b : a ≼ b → Some a ≼ Some b.
+  Proof. rewrite Some_included. auto. Qed.
+  Lemma Some_included_is_Some x mb : Some x ≼ mb → is_Some mb.
+  Proof. rewrite option_included. naive_solver. Qed.
+  Lemma Some_includedN_opM n a b : Some a ≼{n} Some b ↔ ∃ mc, b ≡{n}≡ a ⋅? mc.
+  Proof.
+    rewrite /includedN. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
+  Qed.
+  Lemma Some_included_opM a b : Some a ≼ Some b ↔ ∃ mc, b ≡ a ⋅? mc.
+  Proof.
+    rewrite /included. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
+  Qed.
  Lemma Some_includedN_total `{!CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
  Proof. rewrite Some_includedN. split; [|by eauto]. by intros [->|?]. Qed.

--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -112,15 +112,15 @@ Global Arguments gmapO _ {_ _} _.
 (** Non-expansiveness of higher-order map functions and big-ops *)
 Global Instance merge_ne `{Countable K} {A B C : ofe} n :
-  Proper (((dist (A:=option A) n) ==> (dist (A:=option B) n) ==> (dist (A:=option C) n)) ==>
+  Proper ((dist (A:=option A) n ==> dist (A:=option B) n ==> dist (A:=option C) n) ==>
-   (dist n) ==> (dist n) ==> (dist n)) (merge (M:=gmap K)).
+          dist n ==> dist n ==> dist n) (merge (M:=gmap K)).
 Proof.
  intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
  destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
 Qed.
 Global Instance union_with_proper `{Countable K} {A : ofe} n :
-  Proper (((dist n) ==> (dist n) ==> (dist n)) ==>
+  Proper ((dist n ==> dist n ==> dist n) ==>
-          (dist n) ==> (dist n) ==>(dist n)) (union_with (M:=gmap K A)).
+          dist n ==> dist n ==> dist n) (union_with (M:=gmap K A)).
 Proof.
  intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ne _ _); auto.
  by do 2 destruct 1; first [apply Hf | constructor].
@@ -361,16 +361,18 @@ Proof.
  intros (y&?&->%(Some_included_exclusive _)); eauto using lookup_valid_Some.
 Qed.
 Lemma singleton_included i x y :
-  {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ x ≡ y ∨ x ≼ y.
+  {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ Some x ≼ Some y.
 Proof.
  rewrite singleton_included_l. split.
-  - intros (y'&Hi&?). rewrite lookup_insert in Hi.
+  - intros (y'&Hi&?). rewrite lookup_insert in Hi. by rewrite Hi.
-    apply Some_included. by rewrite Hi.
+  - intros ?. exists y. by rewrite lookup_insert.
-  - intros ?. exists y. by rewrite lookup_insert Some_included.
 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 :
  x ≼ y → {[ i := x ]} ≼ ({[ i := y ]} : gmap K A).
-Proof. intros Hincl. apply singleton_included. right. done. Qed.
+Proof. intros Hincl. apply singleton_included, Some_included_mono. done. Qed.
 Global Instance singleton_cancelable i x :
  Cancelable (Some x) → Cancelable {[ i := x ]}.
@@ -523,16 +525,21 @@ Proof.
    eauto using alloc_unit_singleton_updateP with subst.
 Qed.
+Lemma gmap_local_update m1 m2 m1' m2' :
+  (∀ i, (m1 !! i, m2 !! i) ~l~> (m1' !! i, m2' !! i)) →
+  (m1, m2) ~l~> (m1', m2').
+Proof.
+  intros Hupd. apply local_update_unital=> n mf Hmv Hm.
+  apply forall_and_distr=> i. rewrite lookup_op -cmra_opM_fmap_Some.
+  apply Hupd; simpl; first done. by rewrite Hm lookup_op cmra_opM_fmap_Some.
+Qed.
 Lemma alloc_local_update m1 m2 i x :
  m1 !! i = None → ✓ x → (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2).
 Proof.
-  rewrite cmra_valid_validN=> Hi ?.
+  intros Hi ?. apply gmap_local_update=> j.
-  apply local_update_unital=> n mf Hmv Hm; simpl in *.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
-  split; auto using insert_validN.
+  rewrite !lookup_insert Hi. by apply alloc_option_local_update.
-  intros j; destruct (decide (i = j)) as [->|].
-  - move: (Hm j); rewrite Hi symmetry_iff dist_None lookup_op op_None=>-[_ Hj].
-    by rewrite lookup_op !lookup_insert Hj.
-  - rewrite Hm lookup_insert_ne // !lookup_op lookup_insert_ne //.
 Qed.
 Lemma alloc_singleton_local_update m i x :
@@ -544,24 +551,20 @@ Lemma insert_local_update m1 m2 i x y x' y' :
  (x, y) ~l~> (x', y') →
  (m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2).
 Proof.
-  intros Hi1 Hi2 Hup; apply local_update_unital=> n mf Hmv Hm; simpl in *.
+  intros Hi1 Hi2 Hup. apply gmap_local_update=> j.
-  destruct (Hup n (mf !! i)) as [? Hx']; simpl in *.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
-  { move: (Hmv i). by rewrite Hi1. }
+  rewrite !lookup_insert Hi1 Hi2. by apply option_local_update.
-  { move: (Hm i). by rewrite lookup_op Hi1 Hi2 Some_op_opM (inj_iff Some). }
-  split; auto using insert_validN.
-  rewrite Hm Hx'=> j; destruct (decide (i = j)) as [->|].
-  - by rewrite lookup_insert lookup_op lookup_insert Some_op_opM.
-  - by rewrite lookup_insert_ne // !lookup_op lookup_insert_ne.
 Qed.
 Lemma singleton_local_update_any m i y x' y' :
  (∀ x, m !! i = Some x → (x, y) ~l~> (x', y')) →
  (m, {[ i := y ]}) ~l~> (<[i:=x']>m, {[ i := y' ]}).
 Proof.
-  intros. rewrite /singletonM /map_singleton -(insert_insert ∅ i y' y).
+  intros. apply gmap_local_update=> j.
-  apply local_update_total_valid0=>_ _ /singleton_includedN_l [x0 [/dist_Some_inv_r Hlk0 _]].
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
-  edestruct Hlk0 as [x [Hlk _]]; [done..|].
+  rewrite !lookup_singleton lookup_insert.
-  eapply insert_local_update; [|eapply lookup_insert|]; eauto.
+  destruct (m !! j); first by eauto using option_local_update.
+  apply local_update_total_valid0=> _ _ /option_includedN; naive_solver.
 Qed.
 Lemma singleton_local_update m i x y x' y' :
@@ -576,13 +579,9 @@ Qed.
 Lemma delete_local_update m1 m2 i x `{!Exclusive x} :
  m2 !! i = Some x → (m1, m2) ~l~> (delete i m1, delete i m2).
 Proof.
-  intros Hi. apply local_update_unital=> n mf Hmv Hm; simpl in *.
+  intros Hi. apply gmap_local_update=> j.
-  split; auto using delete_validN.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_delete_ne.
-  rewrite Hm=> j; destruct (decide (i = j)) as [<-|].
+  rewrite !lookup_delete Hi. by apply delete_option_local_update.
-  - rewrite lookup_op !lookup_delete left_id symmetry_iff dist_None.
-    apply eq_None_not_Some=> -[y Hi'].
-    move: (Hmv i). rewrite Hm lookup_op Hi Hi' -Some_op. by apply exclusiveN_l.
-  - by rewrite lookup_op !lookup_delete_ne // lookup_op.
 Qed.
 Lemma delete_singleton_local_update m i x `{!Exclusive x} :
@@ -596,12 +595,9 @@ Lemma delete_local_update_cancelable m1 m2 i mx `{!Cancelable mx} :
  m1 !! i ≡ mx → m2 !! i ≡ mx →
  (m1, m2) ~l~> (delete i m1, delete i m2).
 Proof.
-  intros Hm1i Hm2i. apply local_update_unital=> n mf Hmv Hm; simpl in *.
+  intros Hi1 Hi2. apply gmap_local_update=> j.
-  split; [eauto using delete_validN|].
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_delete_ne.
-  intros j. destruct (decide (i = j)) as [->|].
+  rewrite !lookup_delete Hi1 Hi2. by apply delete_option_local_update_cancelable.
-  - move: (Hm j). rewrite !lookup_op Hm1i Hm2i !lookup_delete. intros Hmx.
-    rewrite (cancelableN mx n (mf !! j) None) ?right_id // -Hmx -Hm1i. apply Hmv.
-  - by rewrite lookup_op !lookup_delete_ne // Hm lookup_op.
 Qed.
 Lemma delete_singleton_local_update_cancelable m i x `{!Cancelable (Some x)} :

--- a/iris/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -76,30 +76,28 @@ Section updates.
  Qed.
  Lemma local_update_valid0 x y x' y' :
-    (✓{0} x → ✓{0} y → x ≡{0}≡ y ∨ y ≼{0} x → (x,y) ~l~> (x',y')) →
+    (✓{0} x → ✓{0} y → Some y ≼{0} Some x → (x,y) ~l~> (x',y')) →
    (x,y) ~l~> (x',y').
  Proof.
    intros Hup n mz Hmz Hz; simpl in *. apply Hup; auto.
    - by apply (cmra_validN_le n); last lia.
    - apply (cmra_validN_le n); last lia.
      move: Hmz; rewrite Hz. destruct mz; simpl; eauto using cmra_validN_op_l.
-    - destruct mz as [z|].
+    - eapply (cmra_includedN_le n); last lia.
-      + right. exists z. apply dist_le with n; auto with lia.
+      apply Some_includedN_opM. eauto.
-      + left. apply dist_le with n; auto with lia.
  Qed.
  Lemma local_update_valid `{!CmraDiscrete A} x y x' y' :
-    (✓ x → ✓ y → x ≡ y ∨ y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
+    (✓ x → ✓ y → Some y ≼ Some x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
  Proof.
-    rewrite !(cmra_discrete_valid_iff 0)
+    rewrite !(cmra_discrete_valid_iff 0) (cmra_discrete_included_iff 0).
-      (cmra_discrete_included_iff 0) (discrete_iff 0).
    apply local_update_valid0.
  Qed.
  Lemma local_update_total_valid0 `{!CmraTotal A} x y x' y' :
    (✓{0} x → ✓{0} y → y ≼{0} x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
  Proof.
-    intros Hup. apply local_update_valid0=> ?? [Hx|?]; apply Hup; auto.
+    intros Hup. apply local_update_valid0=> ?? Hincl. apply Hup; auto.
-    by rewrite Hx.
+    by apply Some_includedN_total.
  Qed.
  Lemma local_update_total_valid `{!CmraTotal A, !CmraDiscrete A} x y x' y' :
    (✓ x → ✓ y → y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
@@ -137,6 +135,19 @@ Section updates_unital.
  Proof. rewrite -{2}(right_id ε op x). by apply cancel_local_update. Qed.
 End updates_unital.
+(** * Unit *)
+Lemma unit_local_update (x y x' y' : unit) : (x, y) ~l~> (x', y').
+Proof. destruct x,y,x',y'; reflexivity. Qed.
+(** * Dependently-typed functions over a discrete domain *)
+Lemma discrete_fun_local_update {A} {B : A → ucmra} (f g f' g' : discrete_fun B) :
+  (∀ x : A, (f x, g x) ~l~> (f' x, g' x)) →
+  (f, g) ~l~> (f', g').
+Proof.
+  setoid_rewrite local_update_unital. intros Hupd n h Hf Hg.
+  split=> x; eapply Hupd, Hg; eauto.
+Qed.
 (** * Product *)
 Lemma prod_local_update {A B : cmra} (x y x' y' : A * B) :
  (x.1,y.1) ~l~> (x'.1,y'.1) → (x.2,y.2) ~l~> (x'.2,y'.2) →
@@ -160,8 +171,6 @@ Lemma prod_local_update_2 {A B : cmra} (x1 y1 : A) (x2 y2 x2' y2' : B) :
 Proof. intros. by apply prod_local_update. Qed.
 (** * Option *)
-(* TODO: Investigate whether we can use these in proving the very similar local
-   updates on finmaps. *)
 Lemma option_local_update {A : cmra} (x y x' y' : A) :
  (x, y) ~l~> (x',y') →
  (Some x, Some y) ~l~> (Some x', Some y').
@@ -200,3 +209,10 @@ Proof.
  move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
  eapply cmra_validN_le; [|lia]. eapply Hy.
 Qed.
+Lemma delete_option_local_update_cancelable {A : cmra} (mx : option A) :
+  Cancelable mx → (mx, mx) ~l~> (None, None).
+Proof.
+  intros ?. apply local_update_unital=>n mf /= Hmx Heq. split; first done.
+  rewrite left_id. eapply (cancelableN mx); by rewrite right_id_L.
+Qed.
--- a/iris/algebra/mra.v
+++ b/iris/algebra/mra.v
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import updates local_updates.
+From iris.prelude Require Import options.
+(** Given a preorder [R] on a type [A] we construct the "monotone" resource
+algebra [mra R] and an injection [principal : A → mra R] such that:
+   [R x y] iff [principal x ≼ principal y]
+Here, [≼] is the extension order of the [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
+*)
+Record mra {A} (R : relation A) := { mra_car : list A }.
+Definition principal {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 ∈ mra_car x ∧ R a b.
+  Local Lemma below_principal a b : below a (principal b) ↔ R a b.
+  Proof. set_solver. Qed.
+  (* OFE *)
+  Local Instance mra_equiv : Equiv (mra R) := λ x y,
+    ∀ a, below a x ↔ 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,
+    {| 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; 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 : 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) := {| mra_car := [] |}.
+  Lemma auth_ucmra_mixin : UcmraMixin (mra R).
+  Proof. split; done. Qed.
+  Canonical Structure mraUR := Ucmra (mra R) auth_ucmra_mixin.
+  (* Laws *)
+  Lemma mra_idemp x : x ⋅ x ≡ x.
+  Proof. intros a. set_solver. Qed.
+  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_op `{!Transitive R} a b :
+    R a b →
+    principal a ⋅ principal b ≡ principal b.
+  Proof. intros Hab c. set_solver. Qed.
+  Lemma principal_included `{!PreOrder R} a b :
+    principal a ≼ principal b ↔ R a b.
+  Proof.
+    split.
+    - move=> [z Hz]. specialize (Hz a). set_solver.
+    - intros ?; exists (principal b). by rewrite principal_R_op.
+  Qed.
+  Lemma mra_local_update_grow `{!Transitive R} a x b:
+    R a b →
+    (principal a, x) ~l~> (principal b, principal b).
+  Proof.
+    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 a, ε) ~l~> (principal a, principal b).
+  Proof.
+    intros Hana. apply local_update_unital_discrete=> z _.
+    rewrite left_id. intros <-. split; first done.
+    apply mra_included; by apply principal_included.
+  Qed.
+End mra.
+Global Arguments mraO {_} _.
+Global Arguments mraR {_} _.
+Global Arguments mraUR {_} _.
+(** If [R] is a partial order, relative to a reflexive relation [S] on the
+carrier [A], then [principal] 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.
+  Lemma principal_rel_proper :
+    Reflexive S →
+    Proper (S ==> S ==> iff) R →
+    Proper (S ==> (≡@{mra R})) (principal).
+  Proof. intros ? HR a1 a2 Ha b. rewrite !below_principal. by apply HR. Qed.
+  Lemma principal_rel_inj :
+    Reflexive R →
+    AntiSymm S R →
+    Inj S (≡@{mra R}) (principal).
+  Proof.
+    intros ?? a b Hab. move: (Hab a) (Hab b). rewrite !below_principal.
+    intros. apply (anti_symm R); naive_solver.
+  Qed.
+End mra_over_rel.
+Global Instance principal_inj {A} {R : relation A} :
+  Reflexive R →
+  AntiSymm (=) R →
+  Inj (=) (≡@{mra R}) (principal) | 0. (* Lower cost than [principal_inj] *)
+Proof. intros. by apply (principal_rel_inj (=)). Qed.
+Global Instance principal_proper `{Equiv A} {R : relation A} :
+  Reflexive (≡@{A}) →
+  Proper ((≡) ==> (≡) ==> iff) R →
+  Proper ((≡) ==> (≡@{mra R})) (principal).
+Proof. intros. by apply (principal_rel_proper (≡)). Qed.
+Global Instance principal_equiv_inj `{Equiv A} {R : relation A} :
+  Reflexive R →
+  AntiSymm (≡) R →
+  Inj (≡) (≡@{mra R}) (principal) | 1.
+Proof. intros. by apply (principal_rel_inj (≡)). Qed.
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -219,8 +219,9 @@ Section inv_heap.
  Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l ↦_I □.
  Proof.
-    iApply own_mono. apply auth_frag_mono. rewrite singleton_included pair_included.
+    iApply own_mono. apply auth_frag_mono.
-    right. split; [apply: ucmra_unit_least|done].
+    rewrite singleton_included_total pair_included.
+    split; [apply: ucmra_unit_least|done].
  Qed.
  (** An accessor to make use of [inv_mapsto_own].

--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -12,6 +12,7 @@ Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
 Global Arguments bi_wand_iff {_} _%I _%I : simpl never.
 Global Instance: Params (@bi_wand_iff) 1 := {}.
 Infix "∗-∗" := bi_wand_iff : bi_scope.
+Notation "P ∗-∗ Q" := (⊢ P ∗-∗ Q) : stdpp_scope.
 Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
 Global Arguments Persistent {_} _%I : simpl never.

--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -306,7 +306,9 @@ Tactic Notation "iAssumption" :=
  end.
 (** * False *)
-Tactic Notation "iExFalso" := apply tac_ex_falso.
+Tactic Notation "iExFalso" :=
+  iStartProof;
+  apply tac_ex_falso.
 (** * Making hypotheses intuitionistic or pure *)
 Local Tactic Notation "iIntuitionistic" constr(H) "as" constr(H') :=
@@ -637,9 +639,19 @@ Local Tactic Notation "iForallRevert" ident(x) :=
  lazymatch type of A with
  | Prop =>
     revert x; first
-       [eapply tac_pure_revert; [tc_solve (* [FromAffinely], should never fail *)|]
+       [eapply tac_pure_revert;
+         [tc_solve (* [FromAffinely], should never fail *)
+         |]
       |err x]
-  | _ => revert x; first [apply tac_forall_revert|err x]
+  | _ =>
+    revert x; first
+      [apply tac_forall_revert;
+       (* Ensure the name [x] is preserved, see [test_iRevert_order_and_names]. *)
+       lazymatch goal with
+       | |- envs_entails ?Δ (bi_forall ?P) =>
+         change (envs_entails Δ (∀ x, P x)); lazy beta
+       end
+      |err x]
  end.
 (** The tactic [iRevertHyp H with tac] reverts the hypothesis [H] and calls
@@ -667,7 +679,10 @@ Tactic Notation "iRevert" constr(Hs) :=
       go Hs
    | ESelIdent _ ?H :: ?Hs => iRevertHyp H; go Hs
    end in
-  iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
+  iStartProof;
+  let Hs := iElaborateSelPat Hs in
+  (* No need to reverse [Hs], [iElaborateSelPat] already does that. *)
+  go Hs.
 Tactic Notation "iRevert" "(" ident(x1) ")" :=
  iForallRevert x1.

--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -63,9 +63,9 @@ Module StringToIdent.
  (** [coq_string_to_ident] implements the ident to string conversion in Ltac2 *)
  Ltac2 coq_string_to_ident (s : constr) := ident_from_string (coq_string_to_string s).
-  (** We want to wrap this in an Ltac1 API, but Ltac1-2 FFI does not support
+  (** We want to wrap [coq_string_to_ident] in an Ltac1 API, but Ltac1-2 FFI
-      returning values from Ltac2 to Ltac1. So we wrute this in CPS instead.
+  does not support returning values from Ltac2 to Ltac1. So we provide
-   *)
+  [string_to_ident_cps] in CPS instead. *)
  Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end.

--- a/iris_unstable/algebra/list.v
+++ b/iris_unstable/algebra/list.v
@@ -267,8 +267,8 @@ Section properties.
    - rewrite list_lookup_singletonM_lt //.
      destruct (lookup_lt_is_Some_2 l j) as [z Hz].
      { trans i; eauto using lookup_lt_Some. }
-      rewrite Hz. by apply Some_included_2, ucmra_unit_least.
+      rewrite Hz. by apply Some_included_mono, ucmra_unit_least.
-    - rewrite list_lookup_singletonM Hi. by apply Some_included_2.
+    - rewrite list_lookup_singletonM Hi. by apply Some_included_mono.
    - rewrite list_lookup_singletonM_gt //. apply: ucmra_unit_least.
  Qed.

--- a/iris_unstable/algebra/monotone.v
+++ b/iris_unstable/algebra/monotone.v
-(** This file is still experimental. See its tracking issue
-https://gitlab.mpi-sws.org/iris/iris/-/issues/414 for details on remaining
-issues before stabilization. *)
-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.
-  Local Definition below (a : A) (x : mra R) := ∃ b, b ∈ 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 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.
-  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.
-  Canonical Structure mraO := discreteO (mra R).
-End ofe.
-Global Arguments mraO [_] _.
-(* CMRA *)
-Section cmra.
-  Context {A : Type} {R : relation A}.
-  Implicit Types a b : A.
-  Implicit Types x y : mra R.
-  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 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.
-  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.
-  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.
-  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.
-  Lemma mra_included (x y : mra R) : 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 principal_includedN `{!PreOrder R} n a b :
-    principal R a ≼{n} principal R 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.
-  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).
-  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.
-  Qed.
-  Lemma mra_local_update_get_frag `{!PreOrder R} a b:
-    R b a →
-    (principal R a, ε) ~l~> (principal R a, principal R 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.
-  Qed.
-End cmra.
-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}.
-  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 principal_inj_related a b :
-    principal R a ≡ principal R b → R a a → R a b.
-  Proof.
-    intros Hab ?.
-    destruct (Hab a) as [[? [?%elem_of_list_singleton ?]] _];
-      last by subst; auto.
-    exists a; rewrite /principal elem_of_list_singleton; done.
-  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.
--- a/iris_unstable/base_logic/algebra.v
+++ b/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.
--- a/tests/mra.ref
+++ b/tests/mra.ref
+"mra_test_eq"
+     : string
+1 goal
+  X, Y : gset nat
+  H : X = Y
+  ============================
+  X = Y
--- a/tests/mra.v
+++ b/tests/mra.v
+From stdpp Require Import propset gmap strings.
+From iris.unstable.algebra Require Import monotone.
+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 : principal X ≡@{gset_mra nat} principal Y → X = Y.
+Proof. intros ?%(inj _). Show. done. Qed.
+Notation propset_mra K := (mra (⊆@{propset K})).
+Lemma mra_test_equiv X Y : principal X ≡@{propset_mra nat} principal Y → X ≡ Y.
+Proof. intros ?%(inj _). done. Qed.
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -628,6 +628,14 @@ No applicable tactic.
  "H" : <affine> ⌜φ⌝ -∗ P
  --------------------------------------∗
  <affine> ⌜φ⌝ -∗ P
+"test_iRevert_order_and_names"
+     : string
+1 goal
+  PROP : bi
+  ============================
+  --------------------------------------∗
+  ∀ P1 P2, P1 -∗ P2 -∗ P1 ∗ P2
 "test_iRevert_pure_affine"
     : string
 1 goal

--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -9,10 +9,14 @@ Section tests.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
-Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
+Lemma test_eauto_iSplit_emp_wand_iff P : emp ⊢ P ∗-∗ P.
 Proof. eauto 6. Qed.
-Lemma test_eauto_isplit_biwand P : ⊢ P ∗-∗ P.
+Lemma test_eauto_iSplit_wand_iff P : ⊢ P ∗-∗ P.
+Proof. eauto. Qed.
+(** We get the [⊢] automatically from the notation in [stdpp_scope]. *)
+Lemma test_eauto_iSplit_wand_iff_std_scope P : P ∗-∗ P.
 Proof. eauto. Qed.
 Fixpoint test_fixpoint (n : nat) {struct n} : True → emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝.
@@ -1416,6 +1420,11 @@ Proof.
  iIntros (?) "HP HQ". iModIntro. Show. by iFrame.
 Qed.
+Lemma test_iExfalso_start_proof P : 0 = 1 → ⊢ P.
+Proof.
+  intros. iExFalso. done.
+Qed.
 Check "test_iRevert_pure".
 Lemma test_iRevert_pure (φ : Prop) P :
  φ → (<affine> ⌜ φ ⌝ -∗ P) -∗ P.
@@ -1424,6 +1433,16 @@ Proof.
  iIntros (Hφ) "H". iRevert (Hφ). Show. done.
 Qed.
+Check "test_iRevert_order_and_names".
+Lemma test_iRevert_order_and_names P1 P2 : P1 -∗ P2 -∗ P1 ∗ P2.
+Proof.
+  iIntros "H1 H2". iRevert (P1 P2) "H1 H2".
+  (* Check that the reverts are performed in the right order (i.e., reverse),
+  and that the names [P1] and [P2] are used in the goal. *)
+  Show.
+  auto with iFrame.
+Qed.
 Check "test_iRevert_pure_affine".
 Lemma test_iRevert_pure_affine `{!BiAffine PROP} (φ : Prop) P :
  φ → (⌜ φ ⌝ -∗ P) -∗ P.
No results found