.gitlab-ci.yml

@@ -44,38 +44,42 @@ variables:
 
 ## Build jobs
 
-build-coq.8.17.0:
+# The newest version runs with timing.
+build-coq.8.18.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.17.0"
+    OPAM_PINS: "coq version 8.18.0"
     DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
+    OPAM_PKG: "1"
+    DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
+    DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
+  tags:
+  - fp-timing
+  interruptible: false
 
-build-coq.8.17.0-mr:
+# The newest version also runs in MRs, without timing.
+build-coq.8.18.0-mr:
   <<: *template
   <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.17.0"
+    OPAM_PINS: "coq version 8.18.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
-build-coq.8.16.1:
+build-coq.8.17.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.16.1"
+    OPAM_PINS: "coq version 8.17.1"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
-    OPAM_PKG: "1"
-    DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
-    DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
-  tags:
-  - fp-timing
-  interruptible: false
 
-build-coq.8.15.2:
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.16.1:
   <<: *template
   <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.15.2"
+    OPAM_PINS: "coq version 8.16.1"
     DENY_WARNINGS: "1"
 
 trigger-stdpp.dev:

CHANGELOG.md

@@ -5,7 +5,7 @@ lemma.
 
 ## Iris master
 
-Coq 8.13 is no longer supported.
+Coq 8.13, 8.14, and 8.15 are no longer supported.
 
 **Changes in `prelude`:**
 
@@ -36,16 +36,30 @@ Coq 8.13 is no longer supported.
     now called `dist_later_fin`.
   - If you need to deal with a `dist_later`/`dist_later_fin` in a manual proof,
     use the tactic `dist_later_intro`/`dist_later_fin_intro` to introduce it.
-  (by Michael Sammler, Lennard Gäher, and Simon Spies).
+  (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.
+* 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`.
+* Use `Strategy expand` for CMRA/UCMRA coercions and most projections to improve
+  performance of type-checking some large CMRA/OFE types. (by Ike Mulder)
+* Add monotone resource algebra, `algebra/mra.v`, to enable reasoning about
+  monotonicity with respect to an arbitrary preorder relation: the extension order
+  of `mra R` is designed to embed the preorder relation `R`. (by Amin Timany)
 
 **Changes in `bi`:**
 
 * Use `binder` in notations for big ops. This means one can write things such
   as `[∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝`.
 * Add constructions `bi_tc`/`bi_nsteps` to create the transitive/`n`-step
-  closure of a PROP-level binary relation. (by Simcha van Collem).
+  closure of a PROP-level binary relation. (by Simcha van Collem)
 * Make the `unseal` tactic of `monPred` more consistent with `uPred`:
   + Rename `MonPred.unseal` → `monPred.unseal`
   + No longer unfold derived BI connectives `<affine>`, `<absorb>` and `◇`.
@@ -54,7 +68,7 @@ Coq 8.13 is no longer supported.
 * Add `unseal` tactic for `siProp`.
 * Add compatibility lemmas for `big_sepL <-> big_sepL2`, `big_sepM <-> big_sepM2`
   with list/maps of pairs; and `big_sepM <-> big_sepL` via `list_to_map` and
-  `map_to_list`. (by Dorian Lesbre).
+  `map_to_list`. (by Dorian Lesbre)
 * Make `persistently_True` a bi-entailment; this changes the default `rewrite`
   direction.
 * Make `BiLaterContractive` a class instead of a notation.
@@ -94,6 +108,18 @@ 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`.
+* 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.
+* Fix `greatest_fixpoint_ne'` accidentally being about the least fixpoint.
+* Add `Plain` instance for `|==> P` when `P` is plain.
+* Rename `bupd_plain` → `bupd_elim`.
+* Change notation for atomic updates and atomic accessors to use `<{ ... }>`
+  instead of `<< ... >>`. This avoids a conflict with Autosubst.
 
 **Changes in `proofmode`:**
 
@@ -126,6 +152,18 @@ Coq 8.13 is no longer supported.
 * The `iFrame` tactic now removes some conjunctions and disjunctions with `False`,
   since additional `MakeOr` and `MakeAnd` instances were provided. If you use these
   classes, their results may have become more concise.
+* Support n-ary versions of `iIntros`, `iRevert`, `iExists`, `iDestruct`, `iMod`,
+  `iFrame`, `iRevertIntros`, `iPoseProof`, `iInduction`, `iLöb`, `iInv`, and
+  `iAssert`. (by Jan-Oliver Kaiser and Rodolphe Lepigre)
+* Add tactics `ltac1_list_iter` and `ltac1_list_rev_iter` to iterate over
+  lists of `ident`s/`simple intropatterns`/`constr`/etc using Ltac1. See
+  [proofmode/base.v](iris/proofmode/base.v) for documentation on how
+  to use these tactics to convert your own fixed arity tactics to an n-ary
+  variant.
+* Improve the `IntoPure` instance for internal equality. Whenever possible,
+  `a ≡ b` will now be simplified to `a = b` upon introduction into the pure 
+  context. This will break but simplify some existing proofs: 
+  `iIntros (H%leibniz_equiv)` should be replaced by `iIntros (H)`. (by Ike Mulder)
 
 **Changes in `base_logic`:**
 
@@ -146,12 +184,30 @@ Coq 8.13 is no longer supported.
 * Remove `frac_validI`. Instead, move to the pure context (with `%` in the proof
   mode or `uPred.discrete_valid` in manual proofs) and use `frac_valid`.
 
+**Changes in `program_logic`:**
+
+* Change the notation for logically atomic triples: we add support for specifying private (non-atomic) postconditions,
+  and we avoid a notation conflict with Autosubst. The new notation looks as follows:
+  `<<{ ∀∀ x, atomic_pre x }>> code @ ∅ <<{ ∃∃ y, atomic_post x y | z, RET v, non_atomic_post x y z }>>`.
+  To keep the notation without private postcondition consistent, the way the return value is specified changes slightly
+  even when there is no private postcondition:
+  `<<{ ∀∀ x, atomic_pre x }>> code @ ∅ <<{ ∃∃ y, atomic_post x y | RET v }>>`.
+
 **Changes in `heap_lang`:**
 
 * Move operations and lemmas about locations into a module `Loc`.
 * Extend `wp_apply` and `wp_smart_apply` to support immediately introducing the
   postcondition into the context via `as (x1 ... xn) "ipat1 ... ipatn"`.
-* Add comparison `≤` and `<` for locations. (by Arthur Azevedo de Amorim).
+* Add comparison `≤` and `<` for locations. (by Arthur Azevedo de Amorim)
+* Make the generic `lock` interface a typeclass and make sure the lock code
+  does not depend on `Σ`. Code that is generic about lock implementations, or
+  that instantiates that specification, needs adjustment. See
+  [iris_heap_lang/lib/lock.v](iris_heap_lang/lib/lock.v) for documentation on
+  how to work with this specification.
+* Adjust the generic `atomic_heap` interface to follow the same pattern as
+  `lock`.
+* Add a generic `rwlock` interface and a spinning implementation.
+  (by Isaac van Bakel)
 
 **LaTeX changes:**
 
@@ -175,6 +231,10 @@ s/\bfresh_locs(_fresh|)\b/Loc.fresh\1/g
 s/\bMonPred\.unseal\b/monPred\.unseal/g
 # big op
 s/\bbig_sepM2_alt\b/big_sepM2_alt_lookup/g
+s/\bbupd_plain\b/bupd_elim/g
+# Logical atomicity (will break Autosubst notation!)
+s/<<</<<\{/g
+s/>>>/\}>>/g
 EOF
 ```
 

README.md

@@ -30,7 +30,7 @@ Importing Iris has some side effects as the library sets some global options.
 
 This version is known to compile with:
 
- - Coq 8.15.2 / 8.16.1 / 8.17.0
+ - Coq 8.16.1 / 8.17.1 / 8.18.0
  - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
 
 Generally we always aim to support the last two stable Coq releases. Support for

_CoqProject

@@ -18,6 +18,8 @@
 # Disabling warnings about future coercion syntax that requires Coq 8.17
 # (https://github.com/coq/coq/pull/16230)
 -arg -w -arg -future-coercion-class-field
+# Some warnings exist only on some Coq versions
+-arg -w -arg -unknown-warning
 
 iris/prelude/options.v
 iris/prelude/prelude.v
@@ -50,6 +52,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
@@ -77,6 +80,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
@@ -167,8 +171,10 @@ iris_heap_lang/lib/spawn.v
 iris_heap_lang/lib/par.v
 iris_heap_lang/lib/assert.v
 iris_heap_lang/lib/lock.v
+iris_heap_lang/lib/rw_lock.v
 iris_heap_lang/lib/spin_lock.v
 iris_heap_lang/lib/ticket_lock.v
+iris_heap_lang/lib/rw_spin_lock.v
 iris_heap_lang/lib/nondet_bool.v
 iris_heap_lang/lib/lazy_coin.v
 iris_heap_lang/lib/clairvoyant_coin.v
@@ -184,7 +190,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

coq-iris.opam

@@ -27,8 +27,8 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.15" & < "8.18~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2023-06-01.0.d1254759") | (= "dev") }
+  "coq" { (>= "8.16" & < "8.19~") | (= "dev") }
+  "coq-stdpp" { (= "dev.2023-09-21.2.7f6df4fa") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]

docs/equalities_and_entailments.md

 # Equalities in Iris
 
-Using Iris involves dealing with a few subtly different equivalence and equality
+Using std++ and Iris involves dealing with a few subtly different equivalence and equality
 relations, especially among propositions.
 This document summarizes these relations and the subtle distinctions among them.
 This is not a general introduction to Iris: instead, we discuss the different
@@ -8,7 +8,7 @@ Iris equalities and the interface to their Coq implementation. In particular, we
 discuss:
 - Equality ("=") in the *on-paper* Iris metatheory
 - Coq's Leibniz equality (`=`) and std++'s setoid equivalence (`≡`);
-- N-equivalence on OFEs (`≡{n}≡`);
+- Iris `n`-equivalence on OFEs (`≡{n}≡`);
 - Iris internal equality (`≡` in `bi_scope`);
 - Iris entailment and bi-entailment (`⊢`, `⊣⊢`).
 
@@ -45,6 +45,52 @@ Here, stdpp adds the following facilities:
   goal `f a ≡ f b` into `a ≡ b` given an appropriate `Proper` instance (here,
   `Proper ((≡) ==> (≡)) f`).
 
+## Defining Proper instances
+
+- For each function `f` that could be used in generalized rewriting (e.g., has
+  setoid, ofe, ordered arguments), there should be a `Params f n` instance. This
+  instance forces Coq's setoid rewriting mechanism not to rewrite in the first
+  `n` arguments of the function `f`. This significantly reduces backtracking
+  during `Proper` search and thus improves performance/avoids failing instance
+  searches that diverge. These first arguments typically include type variables
+  (`A : Type` or `B : A → Type`), type class parameters (`C A`), and Leibniz
+  arguments (`i : nat` or `i : Z`), so they cannot be rewritten or do not need
+  setoid rewriting.
+  Examples:
+  + For `cons : ∀ A, A → list A → list A` we have `Params (@cons) 1`,
+    indicating that the type argument named `A` is not up to rewriting.
+  + For `replicate : ∀ A, nat → A → list A` we have `Params (@replicate) 2`
+    indicating that the type argument `A` is not up to rewriting and that the
+    `nat`-typed argument also does not show up as rewriteable in the `Proper`
+    instance (because rewriting with `=` doesn't need such an instance).
+  + For `lookup : ∀ {Lookup K A M}, K → M → option A` we have
+    `Params (@lookup) 5`: there are 3 Type parameters, 1 type class, and a key
+    (which is Leibniz for all instances).
+- Consequenently, `Proper .. f` instances are always written in such a way
+  that `f` is partially applied with the first `n` arguments from `Params f n`.
+  Note that implicit arguments count here.
+  Further note that `Proper` instances never start with `(=) ==>`.
+  Examples:
+  + `Proper ((≡@{A}) ==> (≡@{list A}) ==> (≡@{list A})) cons`,
+    where `cons` is `@cons A`, matching the 1 in `Params`.
+  + `Proper ((≡@{A}) ==> (≡@{list A})) (replicate n)`,
+    where `replicate n` is `@replicate A n`.
+  + `Proper ((≡@{M}) ==> (≡@{option A})) (lookup k)`,
+    where `lookup k` is `@lookup K A M _ k`, so 5 parameters are fixed, matching
+    the `Params` instance.
+- Lemmas about higher-order functions often need `Params` premises.
+  These are also written using the convention above. Example:
+  ```coq
+  Lemma set_fold_ind `{FinSet A C} {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
+    (∀ x, Proper ((≡) ==> impl) (P x)) → ...
+  ```
+- For premises involving predicates (such as `P` in `set_fold_ind` above), we
+  always write the weakest `Proper`: that is, use `impl` instead of `iff` (and
+  in Iris, write `(⊢)` instead of `(⊣⊢)`). For "simple" `P`s, there should be
+  instances to solve both `impl` and `iff` using `solve_proper`, and for more
+  complicated cases where `solve_proper` fails, an `impl` is much easier to
+  prove by hand than an `iff`.
+
 ## Equivalences on OFEs
 
 On paper, OFEs involve two relations, equality "=" and distance "=_n". In Coq,

docs/style_guide.md

@@ -60,6 +60,19 @@ Use `Lemma`, not `Theorem` (or the other variants: `Fact`, `Corollary`,
 
 **TODO:** Always add `Global` or `Local` to `Hint`, `Arguments`, and `Instance`.
 
+### `Require`
+
+Never put `Require` in the middle of a file. All `Require` must be at the top.
+If you only want to *import* a certain module in some specific place (for instance, in a `Section` or other `Module`), you can do something like:
+
+```coq
+From lib Require component.
+
+(* ... *)
+
+Import component.
+```
+
 ### Ltac
 
 We prefer `first [ t1 | fail 1 "..." ]` to `t1 || fail "..."` because the latter will fail if `t1` doesn't make progress. See https://gitlab.mpi-sws.org/iris/iris/-/issues/216. Note that `first [ t1 | fail "..."]` is simply incorrect; the failure message will never show up and will be replaced with a generic failure.
@@ -208,12 +221,9 @@ theories/base_logic/lib is for constructions in the base logic (using own)
 * Lower-case theorem names, lower-case types, upper-case constructors
 * **TODO:** how should `f (g x) = f' (g' x)` be named?
 * `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.
+* Operations that "extract" from the data structure (`lookup`, `elem_of`, ...) should come before operations that "alter" the data structure (`filter`, `insert`, `union`, `fmap`). For example, use `map_lookup_filter` instead of `map_filter_lookup`.
 * 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 +234,8 @@ 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`.
+* For lemmas `f x = g ...` that give a definition of function `f` in terms of `g`, we use `f_as_g`. For example, `map_compose_as_omap : m ∘ₘ n = omap (m !!.) n`.
 
 ### Naming algebra libraries
 

iris/algebra/agree.v

@@ -178,6 +178,11 @@ Proof.
     exists a. by rewrite elem_of_list_singleton -discrete_iff_0.
 Qed.
 
+Lemma agree_op_inv x y : ✓ (x ⋅ y) → x ≡ y.
+Proof.
+  intros ?. apply equiv_dist=> n. by apply agree_op_invN, cmra_valid_validN.
+Qed.
+
 Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree).
 Proof.
   move=> a b [_] /=. setoid_rewrite elem_of_list_singleton. naive_solver.
@@ -191,7 +196,6 @@ Proof.
   destruct (elem_of_agree x) as [a ?].
   exists a; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver.
 Qed.
-
 Lemma to_agree_uninj x : ✓ x → ∃ a, to_agree a ≡ x.
 Proof.
   rewrite /valid /agree_valid_instance; setoid_rewrite agree_validN_def.
@@ -204,18 +208,21 @@ Proof.
   move=> Hval [z Hy]; move: Hval; rewrite Hy.
   by move=> /agree_op_invN->; rewrite agree_idemp.
 Qed.
+Lemma agree_valid_included x y : ✓ y → x ≼ y → x ≡ y.
+Proof.
+  move=> Hval [z Hy]; move: Hval; rewrite Hy.
+  by move=> /agree_op_inv->; rewrite agree_idemp.
+Qed.
 
 Lemma to_agree_includedN n a b : to_agree a ≼{n} to_agree b ↔ a ≡{n}≡ b.
 Proof.
-  split; last by intros ->. intros [x [_ Hincl]].
-  by destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+.
+  split; last by intros ->.
+  intros. by apply (inj to_agree), agree_valid_includedN.
 Qed.
-
 Lemma to_agree_included a b : to_agree a ≼ to_agree b ↔ a ≡ b.
 Proof.
   split; last by intros ->.
-  intros (x & Heq). apply equiv_dist=>n. destruct (Heq n) as [_ Hincl].
-  by destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+.
+  intros. by apply (inj to_agree), agree_valid_included.
 Qed.
 
 Global Instance agree_cancelable x : Cancelable x.
@@ -232,10 +239,6 @@ Proof.
   by rewrite -EQy -EQz -Hx'y' -Hx'z'.
 Qed.
 
-Lemma agree_op_inv x y : ✓ (x ⋅ y) → x ≡ y.
-Proof.
-  intros ?. apply equiv_dist=>n. by apply agree_op_invN, cmra_valid_validN.
-Qed.
 Lemma to_agree_op_invN a b n : ✓{n} (to_agree a ⋅ to_agree b) → a ≡{n}≡ b.
 Proof. by intros ?%agree_op_invN%(inj to_agree). Qed.
 Lemma to_agree_op_inv a b : ✓ (to_agree a ⋅ to_agree b) → a ≡ b.

iris/algebra/big_op.v

@@ -444,7 +444,7 @@ Section gmap.
     { by rewrite map_filter_empty !big_opM_empty. }
     destruct (decide (φ (k, v))).
     - rewrite map_filter_insert_True //.
-      assert (filter φ m !! k = None) by (apply map_filter_lookup_None; eauto).
+      assert (filter φ m !! k = None) by (apply map_lookup_filter_None; eauto).
       by rewrite !big_opM_insert // decide_True // IH.
     - rewrite map_filter_insert_not' //; last by congruence.
       rewrite !big_opM_insert // decide_False // IH. by rewrite left_id.

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.
@@ -103,6 +106,19 @@ Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_in
 Coercion cmra_ofeO (A : cmra) : ofe := Ofe A (cmra_ofe_mixin A).
 Canonical Structure cmra_ofeO.
 
+(** As explained more thoroughly in iris#539, Coq can run into trouble when
+  [cmra] combinators (such as [optionUR]) are stacked and combined with
+  coercions like [cmra_ofeO]. To partially address this, we give Coq's
+  type-checker some directions for unfolding, with the Strategy command.
+
+  For these structures, we instruct Coq to eagerly _expand_ all projections,
+  except for the coercion to type (in this case, [cmra_car]), since that causes
+  problem with canonical structure inference. Additionally, we make Coq 
+  eagerly expand the coercions that go from one structure to another, like
+  [cmra_ofeO] in this case. *)
+Global Strategy expand [cmra_ofeO cmra_equiv cmra_dist cmra_pcore cmra_op
+                        cmra_valid cmra_validN cmra_ofe_mixin cmra_mixin].
+
 Definition cmra_mixin_of' A {Ac : cmra} (f : Ac → A) : CmraMixin Ac := cmra_mixin Ac.
 Notation cmra_mixin_of A :=
   ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).
@@ -229,6 +245,15 @@ Coercion ucmra_cmraR (A : ucmra) : cmra :=
   Cmra' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
 Canonical Structure ucmra_cmraR.
 
+(** As for CMRAs above, we instruct Coq to eagerly _expand_ all projections,
+  except for the coercion to type (in this case, [ucmra_car]), since that causes
+  problem with canonical structure inference.  Additionally, we make Coq 
+  eagerly expand the coercions that go from one structure to another, like
+  [ucmra_cmraR] and [ucmra_ofeO] in this case. *)
+Global Strategy expand [ucmra_cmraR ucmra_ofeO ucmra_equiv ucmra_dist ucmra_pcore
+                        ucmra_op ucmra_valid ucmra_validN ucmra_unit
+                        ucmra_ofe_mixin ucmra_cmra_mixin].
+
 (** Lifting properties from the mixin *)
 Section ucmra_mixin.
   Context {A : ucmra}.
@@ -634,6 +659,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}.
@@ -664,6 +695,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.
@@ -1377,7 +1409,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.
@@ -1414,6 +1446,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 +1513,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 +1535,43 @@ 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_refl 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.
-  Proof. rewrite Some_included; eauto. Qed.
+  Lemma Some_included_1 a b : Some a ≼ Some b → a ≡ b ∨ a ≼ b.
+  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_refl 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 cmra_validN_Some_includedN n a b : ✓{n} a → Some b ≼{n} Some a → ✓{n} b.
+  Proof. apply: (cmra_validN_includedN _ (Some _) (Some _)). Qed.
+  Lemma cmra_valid_Some_included a b : ✓ a → Some b ≼ Some a → ✓ b.
+  Proof. apply: (cmra_valid_included (Some _) (Some _)). 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.
@@ -1549,6 +1618,12 @@ Section option_prod.
   Lemma Some_pair_includedN n a1 a2 b1 b2 :
     Some (a1,b1) ≼{n} Some (a2,b2) → Some a1 ≼{n} Some a2 ∧ Some b1 ≼{n} Some b2.
   Proof. rewrite !Some_includedN. intros [[??]|[??]%prod_includedN]; eauto. Qed.
+  Lemma Some_pair_includedN_l n a1 a2 b1 b2 :
+    Some (a1,b1) ≼{n} Some (a2,b2) → Some a1 ≼{n} Some a2.
+  Proof. intros. eapply Some_pair_includedN. done. Qed.
+  Lemma Some_pair_includedN_r n a1 a2 b1 b2 :
+    Some (a1,b1) ≼{n} Some (a2,b2) → Some b1 ≼{n} Some b2.
+  Proof. intros. eapply Some_pair_includedN. done. Qed.
   Lemma Some_pair_includedN_total_1 `{CmraTotal A} n a1 a2 b1 b2 :
     Some (a1,b1) ≼{n} Some (a2,b2) → a1 ≼{n} a2 ∧ Some b1 ≼{n} Some b2.
   Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ a1). Qed.
@@ -1559,6 +1634,12 @@ Section option_prod.
   Lemma Some_pair_included a1 a2 b1 b2 :
     Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2 ∧ Some b1 ≼ Some b2.
   Proof. rewrite !Some_included. intros [[??]|[??]%prod_included]; eauto. Qed.
+  Lemma Some_pair_included_l a1 a2 b1 b2 :
+    Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2.
+  Proof. intros. eapply Some_pair_included. done. Qed.
+  Lemma Some_pair_included_r a1 a2 b1 b2 :
+    Some (a1,b1) ≼ Some (a2,b2) → Some b1 ≼ Some b2.
+  Proof. intros. eapply Some_pair_included. done. Qed.
   Lemma Some_pair_included_total_1 `{CmraTotal A} a1 a2 b1 b2 :
     Some (a1,b1) ≼ Some (a2,b2) → a1 ≼ a2 ∧ Some b1 ≼ Some b2.
   Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total a1). Qed.

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

@@ -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)) ==>
-   (dist n) ==> (dist n) ==> (dist n)) (merge (M:=gmap K)).
+  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)).
 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)) ==>
-          (dist n) ==> (dist n) ==>(dist n)) (union_with (M:=gmap K A)).
+  Proper ((dist n ==> dist n ==> dist n) ==>
+          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].
@@ -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.
@@ -361,16 +360,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.
-    apply Some_included. by rewrite Hi.
-  - intros ?. exists y. by rewrite lookup_insert Some_included.
+  - intros (y'&Hi&?). rewrite lookup_insert in Hi. by rewrite Hi.
+  - intros ?. exists y. by rewrite lookup_insert.
 Qed.
-Lemma singleton_mono i x y :
+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_included_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 +524,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 ?.
-  apply local_update_unital=> n mf Hmv Hm; simpl in *.
-  split; auto using insert_validN.
-  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 //.
+  intros Hi ?. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
+  rewrite !lookup_insert Hi. by apply alloc_option_local_update.
 Qed.
 
 Lemma alloc_singleton_local_update m i x :
@@ -544,24 +550,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 *.
-  destruct (Hup n (mf !! i)) as [? Hx']; simpl in *.
-  { move: (Hmv i). by rewrite Hi1. }
-  { 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.
+  intros Hi1 Hi2 Hup. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
+  rewrite !lookup_insert Hi1 Hi2. by apply option_local_update.
 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).
-  apply local_update_total_valid0=>_ _ /singleton_includedN_l [x0 [/dist_Some_inv_r Hlk0 _]].
-  edestruct Hlk0 as [x [Hlk _]]; [done..|].
-  eapply insert_local_update; [|eapply lookup_insert|]; eauto.
+  intros. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
+  rewrite !lookup_singleton lookup_insert.
+  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 +578,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 *.
-  split; auto using delete_validN.
-  rewrite Hm=> j; destruct (decide (i = j)) as [<-|].
-  - 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.
+  intros Hi. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_delete_ne.
+  rewrite !lookup_delete Hi. by apply delete_option_local_update.
 Qed.
 
 Lemma delete_singleton_local_update m i x `{!Exclusive x} :
@@ -596,12 +594,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 *.
-  split; [eauto using delete_validN|].
-  intros j. destruct (decide (i = j)) as [->|].
-  - 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.
+  intros Hi1 Hi2. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_delete_ne.
+  rewrite !lookup_delete Hi1 Hi2. by apply delete_option_local_update_cancelable.
 Qed.
 
 Lemma delete_singleton_local_update_cancelable m i x `{!Cancelable (Some x)} :

iris/algebra/list.v

@@ -51,7 +51,7 @@ Proof. apply Forall2_cons_inv_r. Qed.
 Definition list_ofe_mixin : OfeMixin (list A).
 Proof.
   split.
-  - intros l k. rewrite equiv_Forall2 -Forall2_forall.
+  - intros l k. rewrite list_equiv_Forall2 -Forall2_forall.
     split; induction 1; constructor; intros; try apply equiv_dist; auto.
   - apply _.
   - rewrite /dist /list_dist. eauto using Forall2_impl, dist_le with si_solver.

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|].
-      + right. exists z. apply dist_le with n; auto with lia.
-      + left. apply dist_le with n; auto with lia.
+    - eapply (cmra_includedN_le n); last lia.
+      apply Some_includedN_opM. eauto.
   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)
-      (cmra_discrete_included_iff 0) (discrete_iff 0).
+    rewrite !(cmra_discrete_valid_iff 0) (cmra_discrete_included_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.
-    by rewrite Hx.
+    intros Hup. apply local_update_valid0=> ?? Hincl. apply Hup; auto.
+    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.

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/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 [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.
+
+  (** Pronounced [a] is below [x]. *)
+  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.
+
+  (** 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 ([⋅] 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,
+    {| 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 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 to_mra_included `{!PreOrder R} a b :
+    to_mra a ≼ to_mra b ↔ R a b.
+  Proof.
+    split.
+    - move=> [z Hz]. specialize (Hz a). set_solver.
+    - intros ?; exists (to_mra b). by rewrite to_mra_R_op.
+  Qed.
+
+  Lemma mra_local_update_grow `{!Transitive R} a x b:
+    R a b →
+    (to_mra a, x) ~l~> (to_mra b, to_mra 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 →
+    (to_mra a, ε) ~l~> (to_mra a, to_mra b).
+  Proof.
+    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.
+
+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 [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.
+
+  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 to_mra_rel_inj :
+    Reflexive R →
+    AntiSymm S R →
+    Inj S (≡@{mra R}) (to_mra).
+  Proof.
+    intros ?? a b Hab. move: (Hab a) (Hab b). rewrite !mra_below_to_mra.
+    intros. apply (anti_symm R); naive_solver.
+  Qed.
+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/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.
@@ -1577,7 +1581,7 @@ Section iso_cofe_subtype.
   Context {A B : ofe} `{Cofe A} (P : A → Prop) (f : ∀ x, P x → B) (g : B → A).
   Context (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2).
   Let Hgne : NonExpansive g.
-  Proof. intros n y1 y2. apply g_dist. Qed.
+  Proof. intros n y1 y2. apply g_dist. Defined.
   Local Existing Instance Hgne.
   Context (gf : ∀ x Hx, g (f x Hx) ≡ x).
   Context (Hlimit : ∀ c : chain B, P (compl (chain_map g c))).

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).