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/heap_lang.md

@@ -33,7 +33,7 @@ constructor).
 ## Notation
 
 Notation for writing HeapLang terms is defined in
-[`notation.v`](../theories/heap_lang/notation.v).  There are two scopes, `%E` for
+[`notation.v`](../iris_heap_lang/notation.v).  There are two scopes, `%E` for
 expressions and `%V` for values.  For example, `(a, b)%E` is an expression pair
 and `(a, b)%V` a value pair.  The `e` of a `WP e {{ Q }}` is implicitly in `%E`
 scope.
@@ -55,9 +55,12 @@ that the current goal is of the shape `WP e @ E {{ Q }}`.
 
 Tactics to take one or more pure program steps:
 
-- `wp_pure`: Perform one pure reduction step.  Pure steps are defined by the
-  `PureExec` typeclass and include beta reduction, projections, constructors, as
-  well as unary and binary arithmetic operators.
+- `wp_pure pat credit:"H"`: Perform one pure reduction step. `pat` optionally
+  defines the pattern that the redex has to match; it defaults to `_` (any
+  redex). The `credit:` argument is optional, too; when present, a later credit
+  will be generated in a fresh hypothesis named `"H"`.
+  Pure steps are defined by the `PureExec` typeclass and include beta reduction,
+  projections, constructors, as well as unary and binary arithmetic operators.
 - `wp_pures`: Perform as many pure reduction steps as possible. This
   tactic will **not** reduce lambdas/recs that are hidden behind a definition.
   If the computation reaches a value, the `WP` will be entirely removed and the
@@ -101,9 +104,16 @@ Further tactics:
   particular when accessing invariants, which is only possible when the `WP` in
   the goal is for a single, atomic operation -- `wp_bind` can be used to bring
   the goal into the right shape.
-- `wp_apply pm_trm`: Apply a lemma whose conclusion is a `WP`, automatically
-  applying `wp_bind` as needed.  See the [ProofMode docs](./proof_mode.md) for an
-  explanation of `pm_trm`.
+- `wp_apply pm_trm as (x1 ... xn) "ipat1 ... ipatn"`:
+  Apply a lemma whose conclusion is a `WP`, automatically applying `wp_bind` as
+  needed. The `as` clause is optional and can be used to introduce the
+  postcondition; this works particularly well for Texan triples. See the
+  [ProofMode docs](./proof_mode.md) for an explanation of `pm_trm` and `ipat`.
+- `wp_smart_apply pm_trm as (x1 ... xn) "ipat1 ... ipatn"`:
+  like `wp_apply`, but also performs pure reduction steps to reveal a redex that
+  matches `pm_trm`. To be precise, if applying the lemma fails, `wp_smart_apply`
+  will perform a step of pure reduction (via `wp_pure`), and repeat. (This means
+  that `wp_smart_apply` is not the same as `wp_pures; wp_apply`.)
 
 There is no tactic for `Fork`, just do `wp_apply wp_fork`.
 
@@ -118,7 +128,7 @@ all of the redexes reduced.)
 Sometimes, it is useful to define a derived notion in HeapLang that involves
 thunks.  For example, the parallel composition `e1 ||| e2` is definable in
 HeapLang, but that requires thunking `e1` and `e2` before passing them to
-`par`. (This is defined in [`par.v`](theories/heap_lang/lib/par.v).)  However,
+`par`. (This is defined in [`par.v`](../iris_heap_lang/lib/par.v).)  However,
 this is somewhat subtle because of the distinction between expression lambdas
 and value lambdas.
 

docs/ibus

+;; Usage: copy to ~/.m17n.d/coq.mim
+
+(input-method t coq)
+(description "Input method for Coq")
+(title "Coq")
+
+(map (trans
+
+;; Standard LaTeX math notations
+  ("\\forall"         "∀")
+  ("\\exists"         "∃")
+  ("\\lam"            "λ")
+  ("\\not"            "¬")
+  ("\\/"              "∨")
+  ("/\\"              "∧")
+  ("->"               "→")
+  ("<->"              "↔")
+  ("\\<-"             "←") ;; we add a backslash because the plain <- is used for the rewrite tactic
+  ("\\=="             "≡")
+  ("\\/=="            "≢")
+  ("/="               "≠")
+  ("<="               "≤")
+  ("\\in"             "∈")
+  ("\\notin"          "∉")
+  ("\\cup"            "∪")
+  ("\\cap"            "∩")
+  ("\\setminus"       "∖")
+  ("\\subset"         "⊂")
+  ("\\subseteq"       "⊆")
+  ("\\sqsubseteq"     "⊑")
+  ("\\sqsubseteq"     "⊑")
+  ("\\notsubseteq"    "⊈")
+  ("\\meet"           "⊓")
+  ("\\join"           "⊔")
+  ("\\top"            "⊤")
+  ("\\bottom"         "⊥")
+  ("\\vdash"          "⊢")
+  ("\\dashv"          "⊣")
+  ("\\Vdash"          "⊨")
+  ("\\infty"          "∞")
+  ("\\comp"           "∘")
+  ("\\prf"            "↾")
+  ("\\bind"           "≫=")
+  ("\\mapsto"         "↦")
+  ("\\hookrightarrow" "↪")
+  ("\\uparrow"        "↑")
+
+;; Iris specific
+  ("\\fun"            "λ")
+  ("\\mult"           "⋅")
+  ("\\ent"            "⊢")
+  ("\\valid"          "✓")
+  ("\\diamond"        "◇")
+  ("\\box"            "□")
+  ("\\bbox"           "■")
+  ("\\later"          "▷")
+  ("\\pred"           "φ")
+  ("\\and"            "∧")
+  ("\\or"             "∨")
+  ("\\comp"           "∘")
+  ("\\ccomp"          "◎")
+  ("\\all"            "∀")
+  ("\\ex"             "∃")
+  ("\\to"             "→")
+  ("\\sep"            "∗")
+  ("\\lc"             "⌜")
+  ("\\rc"             "⌝")
+  ("\\Lc"             "⎡")
+  ("\\Rc"             "⎤")
+  ("\\empty"          "∅")
+  ("\\Lam"            "Λ")
+  ("\\Sig"            "Σ")
+  ("\\-"              "∖")
+  ("\\aa"             "●")
+  ("\\af"             "◯")
+  ("\\auth"           "●")
+  ("\\frag"           "◯")
+  ("\\iff"            "↔")
+  ("\\gname"          "γ")
+  ("\\incl"           "≼")
+  ("\\latert"         "▶")
+  ("\\update"         "⇝")
+  ("\\bind"           "≫=")
+
+;; accents (for iLöb)
+  ("\\\"o" "ö")
+
+;; subscripts and superscripts
+  ("^^+" "⁺") ("__+" "₊") ("^^-" "⁻")
+  ("__0" "₀") ("__1" "₁") ("__2" "₂") ("__3" "₃") ("__4" "₄")
+  ("__5" "₅") ("__6" "₆") ("__7" "₇") ("__8" "₈") ("__9" "₉")
+
+  ("__a" "ₐ") ("__e" "ₑ") ("__h" "ₕ") ("__i" "ᵢ") ("__k" "ₖ")
+  ("__l" "ₗ") ("__m" "ₘ") ("__n" "ₙ") ("__o" "ₒ") ("__p" "ₚ")
+  ("__r" "ᵣ") ("__s" "ₛ") ("__t" "ₜ") ("__u" "ᵤ") ("__v" "ᵥ") ("__x" "ₓ")
+
+;; Greek alphabet
+  ("\\Alpha"  "Α")   ("\\alpha"  "α")
+  ("\\Beta"   "Β")   ("\\beta"   "β")
+  ("\\Gamma"  "Γ")   ("\\gamma"  "γ")
+  ("\\Delta"  "Δ")   ("\\delta"  "δ")
+  ("\\Epsilon"  "Ε") ("\\epsilon"  "ε")
+  ("\\Zeta"   "Ζ")   ("\\zeta"   "ζ")
+  ("\\Eta"  "Η")     ("\\eta"  "η")
+  ("\\Theta"  "Θ")   ("\\theta"  "θ")
+  ("\\Iota"   "Ι")   ("\\iota"   "ι")
+  ("\\Kappa"  "Κ")   ("\\kappa"  "κ")
+  ("\\Lamda"  "Λ")   ("\\lamda"  "λ")
+  ("\\Lambda"   "Λ") ("\\lambda"   "λ")
+  ("\\Mu"   "Μ")     ("\\mu"   "μ")
+  ("\\Nu"   "Ν")     ("\\nu"   "ν")
+  ("\\Xi"   "Ξ")     ("\\xi"   "ξ")
+  ("\\Omicron"  "Ο") ("\\omicron"  "ο")
+  ("\\Pi"   "Π")     ("\\pi"   "π")
+  ("\\Rho"  "Ρ")     ("\\rho"  "ρ")
+  ("\\Sigma"  "Σ")   ("\\sigma"  "σ")
+  ("\\Tau"  "Τ")     ("\\tau"  "τ")
+  ("\\Upsilon"  "Υ") ("\\upsilon"  "υ")
+  ("\\Phi"  "Φ")     ("\\phi"  "φ")
+  ("\\Chi"  "Χ")     ("\\chi"  "χ")
+  ("\\Psi"  "Ψ")     ("\\psi"  "ψ")
+  ("\\Omega"  "Ω")   ("\\omega"  "ω")
+))
+(state (init (trans)))

docs/proof_guide.md

@@ -81,7 +81,7 @@ avoided.
 ## Type class resolution control
 
 When you are writing a module that exports some Iris term for others to use
-(e.g., `join_handle` in the [spawn module](../theories/heap_lang/lib/spawn.v)), be
+(e.g., `join_handle` in the [spawn module](../iris_heap_lang/lib/spawn.v)), be
 sure to mark these terms as opaque for type class search at the *end* of your
 module (and outside any section):
 ```coq
@@ -99,7 +99,7 @@ for further details on `libG` classes).  For example, the STS library is
 parameterized by an STS and assumes that the STS state space is inhabited:
 ```coq
 Class stsG Σ (sts : stsT) := {
-  sts_inG :> inG Σ (stsR sts);
+  #[local] sts_inG :: inG Σ (stsR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
 ```

docs/proof_mode.md

@@ -21,7 +21,7 @@ pervasively. These are defined in dedicated sections in this manual.
 
 Many of the tactics below apply to more goals than described in this document
 since the behavior of these tactics can be tuned via instances of the type
-classes in the file [proofmode/classes](iris/proofmode/classes.v). Most notably, many
+classes in the file [proofmode/classes](../iris/proofmode/classes.v). Most notably, many
 of the tactics can be applied when the connective to be introduced or to be eliminated
 appears under a later, an update modality, or in the conclusion of a
 weakest precondition.
@@ -162,11 +162,11 @@ Elimination of logical connectives
     spatial context matching pattern `pat`.
 
   In case all branches of `ipat` start with a `#` (which causes the hypothesis
-  to be moved to the intuitionistic context) or with an `%` (which causes the
-  hypothesis to be moved to the pure Coq context), then one can use all
-  hypotheses for proving the premises of `pm_trm`, as well as for proving the
-  resulting goal. Note that in this case the hypotheses still need to be
-  subdivided among the spatial premises.
+  to be moved to the intuitionistic context), with an `%` (which causes the
+  hypothesis to be moved to the pure Coq context), or with an `->`/`<-` (which
+  performs a rewrite), then one can use all hypotheses for proving the premises
+  of `pm_trm`, as well as for proving the resulting goal. Note that in this case
+  the hypotheses still need to be subdivided among the spatial premises.
 
 Separation logic-specific tactics
 ---------------------------------
@@ -184,10 +184,17 @@ Separation logic-specific tactics
 - `iFrame select (pat)%I` : cancel the last hypothesis of the intuitionistic
   of spatial context that matches pattern `pat`.
 - `iCombine "H1 H2" as "ipat"` : combine `H1 : P1` and `H2 : P2` into `H: P1 ∗
-  P2` or something simplified but equivalent, then destruct the combined
+  P2` or something simplified but equivalent, then `destruct` the combined
   hypothesis using `ipat`. Some examples of simplifications `iCombine` knows
   about are to combine `own γ x` and `own γ y` into `own γ (x ⋅ y)`, and to
   combine `l ↦{1/2} v` and `l ↦{1/2} v` into `l ↦ v`.
+- `iCombine "H1 H2" gives "ipat"` : from `H1 : P1` and `H2 : P2`, find
+  persistent consequences of `P1 ∗ P2`, then `destruct` this consequence with
+  `ipat`. Some examples of persistent consequences `iCombine` knows about are
+  that `own γ x` and `own γ y` gives `✓ (x ⋅ y)`, and that
+  `l ↦{#q1} v1` and `l ↦{#q2} v2` gives `⌜(q1 + q2 ≤ 1) ∧ v1 = v2⌝`.
+- `iCombine "H1 H2" as "ipat1" gives "ipat2"` combines the two functionalities
+  of `iCombine` described above.
 - `iAccu` : solve a goal that is an evar by instantiating it with all
   hypotheses from the spatial context joined together with a separating
   conjunction (or `emp` in case the spatial context is empty). Not commonly
@@ -233,18 +240,26 @@ Induction
   + `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction,
   generalizing over the Coq level variables `x1 ... xn`, the hypotheses given by
   the selection pattern `selpat`, and the spatial context as usual.
-- `iInduction x as cpat "IH" "selpat"` : perform induction on
-  the Coq term `x`. The Coq introduction pattern `cpat` is used to name the introduced
-  variables. The induction hypotheses are inserted into the intuitionistic
-  context and given fresh names prefixed `IH`.
-  + `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction,
+- `iInduction x as cpat` : perform induction on the Coq term `x`. The
+  Coq introduction pattern `cpat` is used to name the introduced variables,
+  including the induction hypotheses which are introduced into the proof mode
+  context. Note that induction hypotheses should not be put into string
+  quotation marks `".."`, e.g., use `iInduction n as [|n IH]` to perform
+  induction on a natural number `n`. An implementation caveat is that the names
+  of the induction hypotheses should be fresh in both the Coq context and the
+  proof mode context.
+  + `iInduction x as cpat forall (x1 ... xn) "selpat"` : perform induction,
     generalizing over the Coq level variables `x1 ... xn`, the hypotheses given by
     the selection pattern `selpat`, and the spatial context.
-  + `iInduction x as cpat "IH" using t` : perform induction using the induction
+  + `iInduction x as cpat using t` : perform induction using the induction
     scheme `t`. Common examples of induction schemes are `map_ind`, `set_ind_L`,
     and `gmultiset_ind` for `gmap`, `gset`, and `gmultiset`.
-  + `iInduction x as cpat "IH" using t forall (x1 ... xn) "selpat"` : the above
+  + `iInduction x as cpat using t forall (x1 ... xn) "selpat"` : the above
     variants combined.
+  + `iInduction x as cpat "IH" "selpat"` : ignore the names of the induction
+    hypotheses from `cpat` and call them `IH`, `IH1`, `IH2`, etc. Here "IH" is
+    a string (in string quotation marks). This is *legacy* syntax that might be
+    deprecated in the future. Similar legacy syntax exists for all variants above.
 
 Rewriting / simplification
 --------------------------
@@ -266,6 +281,10 @@ Rewriting / simplification
 - `iSimpl` / `iSimpl in "selpat"` : perform `simpl` on the proof mode
   goal / hypotheses given by the selection pattern `selpat`. This is a
   shorthand for `iEval (simpl)`.
+- `iUnfold xs` / `iUnfold xs in "selpat"` : perform `unfold xs` on the proof
+  mode goal / hypotheses given by the selection pattern `selpat`. This is a
+  shorthand for `iEval (unfold xs)`. Similar to Coq's `unfold`, the argument
+  `xs` should be a comma-separated non-empty list.
 
 Iris
 ----

docs/resource_algebras.md

@@ -14,12 +14,20 @@ Libraries typically bundle the `inG` they need in a `libG` typeclass, so they do
 not have to expose to clients what exactly their resource algebras are. For
 example, in the [one-shot example](../tests/one_shot.v), we have:
 ```coq
-Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
+Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
+Local Existing Instances one_shot_inG.
 ```
-The `:>` means that the projection `one_shot_inG` is automatically registered as
-an instance for type-class resolution.  If you need several resource algebras,
-just add more `inG` fields.  If you are using another module as part of yours,
-add a field like `one_shot_other :> otherG Σ`.
+Here, the projection `one_shot_inG` is registered as an instance for type-class
+resolution. If you need several resource algebras, just add more `inG` fields.
+If you are using another module as part of yours, add a field like
+`one_shot_other : otherG Σ`. All of these fields should be added to the
+`Local Existing Instances` command.
+
+The code above enables these typeclass instances only in the surrounding file
+where they are used to define the new abstractions by the library. The
+interface of these abstractions will only depend on the `one_shotG` class.
+Since `one_shot_inG` will be hidden from clients, they will not accidentally
+rely on it in their code.
 
 Having defined the type class, we need to provide a way to instantiate it.  This
 is an important step, as not every resource algebra can actually be used: if
@@ -51,12 +59,12 @@ Now you can add `one_shotG` as an assumption to all your module definitions and
 proofs.  We typically use a section for this:
 ```coq
 Section proof.
-Context `{!heapG Σ, !one_shotG Σ}.
+Context `{!heapGS Σ, !one_shotG Σ}.
 ```
-Notice that besides our own assumptions `one_shotG`, we also assume `heapG`,
+Notice that besides our own assumptions `one_shotG`, we also assume `heapGS`,
 which are assumptions that every HeapLang proof makes (they are related to
 defining the `↦` connective as well as the basic Iris infrastructure for
-invariants and WP).  For this purpose, `heapG` contains not only assumptions
+invariants and WP).  For this purpose, `heapGS` contains not only assumptions
 about `Σ`, it also contains some ghost names to refer to particular ghost state
 (see "global ghost state instances" below).
 
@@ -91,10 +99,10 @@ To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
 `inG`, you have to assemble a list of functors of all the involved modules,
 and if your proof relies on some singleton (most do, at least indirectly; also
 see the next section), you have to call the respective initialization or
-adequacy lemma.  [For example](tests/one_shot.v):
+adequacy lemma.  [For example](../tests/one_shot.v):
 ```coq
 Section client.
-  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
+  Context `{!heapGS Σ, !one_shotG Σ, !spawnG Σ}.
 
   Lemma client_safe : WP client {{ _, True }}%I.
   (* ... *)
@@ -118,10 +126,11 @@ class for the generalized heap module, bundles the usual `inG` assumptions
 together with the `gname`:
 ```coq
 Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heapGpreS_heap :> ghost_mapG Σ L V;
+  #[local] gen_heapGpreS_heap :: ghost_mapG Σ L V;
 }.
+
 Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
-  gen_heap_inG :> gen_heapGpreS L V Σ;
+  #[local] gen_heap_inG :: gen_heapGpreS L V Σ;
   gen_heap_name : gname;
 }.
 ```
@@ -132,9 +141,9 @@ would be incompatible with each other.
 
 The `gen_heapGpreS` typeclass (without the singleton data) is relevant for
 initialization, i.e., to create an instance of `gen_heapGS`. This is happening as
-part of [`heap_adequacy`](iris_heap_lang/adequacy.v) using the
+part of [`heap_adequacy`](../iris_heap_lang/adequacy.v) using the
 initialization lemma for `gen_heapGS` from
-[`gen_heap_init`](iris/base_logic/lib/gen_heap.v):
+[`gen_heap_init`](../iris/base_logic/lib/gen_heap.v):
 ```coq
 Lemma gen_heap_init `{gen_heapGpreS L V Σ} σ :
   (|==> ∃ _ : gen_heapGS L V Σ, gen_heap_ctx σ)%I.
@@ -222,9 +231,9 @@ F (X,X⁻) := gmap K (agree (nat * ▶ X))
 To make it convenient to construct such functors and prove their contractivity,
 we provide a number of abstractions:
 
-- [`oFunctor`](iris/algebra/ofe.v): functors from COFEs to OFEs.
-- [`rFunctor`](iris/algebra/cmra.v): functors from COFEs to cameras.
-- [`urFunctor`](iris/algebra/cmra.v): functors from COFEs to unital
+- [`oFunctor`](../iris/algebra/ofe.v): functors from COFEs to OFEs.
+- [`rFunctor`](../iris/algebra/cmra.v): functors from COFEs to cameras.
+- [`urFunctor`](../iris/algebra/cmra.v): functors from COFEs to unital
   cameras.
 
 Besides, there are the classes `oFunctorContractive`, `rFunctorContractive`, and
@@ -249,7 +258,7 @@ Using these combinators, one can easily construct bigger functors in point-free
 style and automatically infer their contractivity, e.g:
 
 ```coq
-F := gmaURF K (agreeRF (prodOF (constOF natO) (laterOF idOF)))
+F := gmapURF K (agreeRF (prodOF (constOF natO) (laterOF idOF)))
 ```
 
 which effectively defines the desired example functor
@@ -273,7 +282,9 @@ Putting it all together, the `libG` typeclass and `libΣ` list of functors for
 your example would look as follows:
 
 ```coq
-Class libG Σ := { lib_inG :> inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
+Class libG Σ :=
+  { #[local] lib_inG :: inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
+
 Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
 Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.
 Proof. solve_inG. Qed.

docs/style_guide.md

+# Iris proof style
+
+**Warning:** this document is still in development and rather incomplete.
+If you run across a question of style (for example, something comes
+up in an MR) and it's not on this list, please do reach out to us on Mattermost
+so we can add it.
+
+## Basic syntax
+
+### Binders
+
+This applies to Context, Implicit Types, and definitions.
+
+- **Put a space on both sides of the colon.**
+
+  Good: `(a : B)` <br>
+  Bad: `(a:B)`, `(a: B)`
+
+- **Prefer `(a : B)` to `a : B`.** (TODO)
+
+
+### Patterns
+
+#### Disjunctions & branches
+
+- **Always mark the disjuncts when destructuring a disjunctive pattern, even if you don't bind anything, to indicate that the proof branches.**
+
+  Good:
+  ```coq
+  Lemma foo : ∀ b : bool, b = true ∨ b = false.
+  Proof.
+    intros [|].
+    ...
+  ```
+
+  Bad:
+  ```coq
+  Lemma foo : ∀ b : bool, b = true ∨ b = false.
+  Proof.
+    intros [].
+    ...
+  ```
+
+#### Uncategorized
+
+- **Use `"[H1 H2]"` when possible otherwise do `"(H1 & H2 & H3)"`.** (TODO)
+
+### Unicode
+
+- **Always use Unicode variants of forall, exists, ->, <=, >=.**
+
+  Good: `∀ ∃ → ≤ ≥`<br>
+  Bad: `forall exists -> <= >=`
+
+### Equivalent vernacular commands
+
+- **Use `Context`, never `Variable`.**
+
+- **Use `Implicit Types`, never `Implicit Type`.** (TODO)
+
+- **Use `Lemma`, not `Theorem` (or the other variants: `Fact`, `Corollary`, `Remark`)**.
+
+- **Always add `Global` or `Local` to `Hint`, `Arguments`, and `Instance`.** (TODO)
+
+### `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
+
+- **Prefer `first [ t1 | fail 1 "..." ]` to `t1 || fail "..."`.** This is better 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.
+
+### Coqdoc comments
+
+- **Module-level comments (covering the entire file) go at the top of the file, before the `Require`.**
+
+### Uncategorized
+
+- **Indent the body of a match by one space.**
+
+  Good:
+  ```coq
+  match foo with
+  | Some x =>
+     long line here using 
+  ```
+  
+  *RJ*: This is odd, usually everything is in (multiples of) 2 spaces, I think.
+  
+  *Tej*: https://gitlab.mpi-sws.org/iris/iris/-/blob/920bc3d97b8830139045e1780f2aff4d05b910cd/iris_heap_lang/proofmode.v#L194
+
+- **Avoid using the extra square brackets around an Ltac match.**
+
+  Good:
+  ```coq
+  match goal with
+  | |- ?g => idtac g
+  
+  ```
+  
+  Bad:
+  ```coq
+  match goal with
+  | [ |- ?g ] => idtac g
+  
+  ```
+
+- **Use coqdoc syntax in comments for Coq identifiers and inline code, e.g. `[cmraT]`.**
+
+- **Put proofs either all on one line (`Proof. reflexivity. Qed.`) or split up the usual way with indentation.**
+
+  Bad:
+  
+  ```coq
+  Lemma foo : 2 + 2 = 4 ∧ 1 + 2 = 3.
+  Proof. split.
+    - reflexivity.
+    - done.
+  Qed.
+  ```
+
+- **Put the entire theorem statement on one line or one premise per line, indented by 2 spaces.**
+
+  Bad:
+  
+  ```coq
+  Lemma foo x y z :
+      x < y → y < z →
+      x < z.
+  ```
+  
+  Good:
+  
+  ```coq
+  Lemma foo x y z : x < y → y < z → x < z.
+  ```
+  
+  Good: (particularly if premises are longer)
+  
+  ```coq
+  Lemma foo x y z :
+    x < y →
+    y < z →
+    x < z.
+  ```
+
+- **If the parameters before the `:` become too long, indent later lines by 4 spaces and always have a newline after `:`.**
+
+  Bad:
+  
+  ```coq
+  Lemma foo (very_long_name : has_a_very_long_type)
+  (even_longer_name : has_an_even_longer_type) : x < y → y < z →
+    x < z.
+  ```
+  
+  Good:
+  
+  ```coq
+  Lemma foo (very_long_name : has_a_very_long_type)
+      (even_longer_name : has_an_even_longer_type) :
+    x < y → y < z → x < z.
+  ```
+
+- **For definitions that don't fit into one line, put `:=` before the linebreak, not after.**
+
+  Bad:
+  
+  ```coq
+  Definition foo (arg1 arg2 arg3 : name_of_the_type)
+    := the body that is very long.
+  ```
+  
+  Good:
+  
+  ```coq
+  Definition foo (arg1 arg2 arg3 : name_of_the_type) :=
+    the body that is very long.
+  ```
+
+- **For tests with output put `Check "theorem name in a string"` before it so that the output from different tests is separated.**
+
+- **For long `t1; t2; t3` and `t; [t1 | t2 | t3]` split them like this, and indent by 2 spaces.**
+
+  Good:
+  ```coq
+  t;
+    [t1
+    |t2
+    |t3].
+  ```
+  
+  ```coq
+  t;
+    t1;
+    t2.
+  ```
+
+
+
+## File organization
+theories/algebra is for primitive ofe/RA/CMRA constructions
+theories/algebra/lib is for derived constructions
+theories/base_logic/lib is for constructions in the base logic (using own)
+
+## Naming
+* `*_ctx` for persistent facts (often an invariant) needed by everything in a library
+* `*_interp` for a function from some representation to iProp
+* If you have lemma `foo` which is an iff and you want single direction versions, name them `foo_1` (forward) and `foo_2` (backward)
+* If you have a lemma `foo` parametrized by an equivalence relation, you might want a version specialized to Leibniz equality for better rewrite support; name that version `foo_L` and state it with plain equality (e.g., `dom_empty_L` in stdpp). You might take an assumption `LeibnizEquiv A` if the original version took an equivalence (say the OFE equivalence) to assume that the provided equivalence is plain equality.
+* 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).
+* 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.
+* For lemmas involving modalities, we usually follow this naming scheme:
+    ```
+    M1_into_M2: M1 P ⊢ M2 P
+    M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
+    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
+
+**TODO:** describe any conclusions we came to with the `mono_nat` library
+
+## Parameter order and implicitness for lemmas
+
+* Parameter order is usually from more higher-order to less higher-order (types, functions, plain values), and otherwise follows the order in which variables appear in the lemma statement.
+* In new lemmas, arguments should be marked as implicit when they can be inferred by unification in all intended usage scenarios. (If an argument can *sometimes* be inferred, we do not have a clear guideline yet -- consider on a case-by-case basis, for now.)
+
+## Lemma statements
+
+### Iris lemmas: `-∗` vs `⊢`
+
+* For low-level lemmas, in particular if there is a high likelihood someone would want to rewrite with it / use them in non-proofmode goals (e.g. modality intro rules), use `⊢`
+  * `P ⊢ |==£> P`
+  * `(|==£> |==£> P) ⊢ |==£> P`
+  * `▷ own γ a ⊢ ◇ ∃ b, own γ b ∧ ▷ (a ≡ b)`
+  * `(P -∗ Q) i ⊢ (P i -∗ Q i)`
+* If a lemma is a Coq implication of Iris entailments (where the entailments are visible, not hidden behind e.g. `Persistent`), then use `⊢`
+  * `(P1 ⊢ P2) → recv l P1 ⊢ recv l P2`
+* Else use -∗
+  * `a1 ⋅ a2 ~~> a' → own γ a1 -∗ own γ a2 ==∗ own γ a'` (curried and hence not rewrite-friendly)
+
+## Metavariables
+**TODO:** move these to the right place
+
+* `P` `Q` for bi:PROP (or specifically `iProp Σ`)
+* `Φ` and `Ψ` for (?A -> iProp), like postconditions
+* `φ` and `ψ` for `Prop`
+* `A` `B` for types, ofeT, or cmraT
+
+Suffixes like O, R, UR (already documented)

docs/vim_ultisnips

+snippet \forall "" i
+∀
+endsnippet
+snippet \exists "" i
+∃
+endsnippet
+snippet \lam "" i
+λ
+endsnippet
+snippet \not "" i
+¬
+endsnippet
+snippet \lor "" i
+∨
+endsnippet
+snippet \land "" i
+∧
+endsnippet
+snippet \/ "" i
+∨
+endsnippet
+snippet /\ "" i
+∧
+endsnippet
+snippet \rightarrow "" i
+→
+endsnippet
+snippet \implies "" i
+→
+endsnippet
+snippet -> "" i
+→
+endsnippet
+snippet \iff "" i
+↔
+endsnippet
+snippet <-> "" i
+↔
+endsnippet
+snippet \<- "" i
+←
+endsnippet
+snippet \cong "" i
+≡
+endsnippet
+snippet \== "" i
+≡
+endsnippet
+snippet \/== "" i
+≢
+endsnippet
+snippet \neq "" i
+≠
+endsnippet
+snippet /= "" i
+≠
+endsnippet
+snippet \less "" i
+≤
+endsnippet
+snippet \le "" i
+≤
+endsnippet
+snippet <= "" i
+≤
+endsnippet
+snippet \in "" i
+∈
+endsnippet
+snippet \notin "" i
+∉
+endsnippet
+snippet \cup "" i
+∪
+endsnippet
+snippet \cap "" i
+∩
+endsnippet
+snippet \setminus "" i
+∖
+endsnippet
+snippet \subset "" i
+⊂
+endsnippet
+snippet \subseteq "" i
+⊆
+endsnippet
+snippet \sqsubseteq "" i
+⊑
+endsnippet
+snippet \sqsubseteq "" i
+⊑
+endsnippet
+snippet \notsubseteq "" i
+⊈
+endsnippet
+snippet \meet "" i
+⊓
+endsnippet
+snippet \join "" i
+⊔
+endsnippet
+snippet \true "" i
+⊤
+endsnippet
+snippet \top "" i
+⊤
+endsnippet
+snippet \false "" i
+⊥
+endsnippet
+snippet \bottom "" i
+⊥
+endsnippet
+snippet \vdash "" i
+⊢
+endsnippet
+snippet \dashv "" i
+⊣
+endsnippet
+snippet \vDash "" i
+⊨
+endsnippet
+snippet \Vdash
+⊩
+endsnippet
+snippet \infty "" i
+∞
+endsnippet
+snippet \comp "" i
+∘
+endsnippet
+snippet \prf "" i
+↾
+endsnippet
+snippet \bind "" i
+≫=
+endsnippet
+snippet \mapsto "" i
+↦
+endsnippet
+snippet \hookrightarrow "" i
+↪
+endsnippet
+snippet \up "" i
+↑
+endsnippet
+snippet \uparrow "" i
+↑
+endsnippet
+
+snippet \fun "" i
+λ
+endsnippet
+snippet \mult "" i
+⋅
+endsnippet
+snippet \ent "" i
+⊢
+endsnippet
+snippet \valid "" i
+✓
+endsnippet
+snippet \diamond "" i
+◇
+endsnippet
+snippet \box "" i
+□
+endsnippet
+snippet \bbox "" i
+■
+endsnippet
+snippet \eval "" i
+▷
+endsnippet
+snippet \rhd "" i
+▷
+endsnippet
+snippet \later "" i
+▷
+endsnippet
+snippet \pred "" i
+φ
+endsnippet
+snippet \and "" i
+∧
+endsnippet
+snippet \or "" i
+∨
+endsnippet
+snippet \circ "" i
+∘
+endsnippet
+snippet \comp "" i
+∘
+endsnippet
+snippet \ccomp "" i
+◎
+endsnippet
+snippet \pound "" i
+£
+endsnippet
+snippet \all "" i
+∀
+endsnippet
+snippet \ex "" i
+∃
+endsnippet
+snippet \to "" i
+→
+endsnippet
+snippet \ast "" i
+∗
+endsnippet
+snippet \sep "" i
+∗
+endsnippet
+snippet \ulc "" i
+⌜
+endsnippet
+snippet \urc "" i
+⌝
+endsnippet
+snippet \lc "" i
+⌜
+endsnippet
+snippet \rc "" i
+⌝
+endsnippet
+snippet \Lc "" i
+⎡
+endsnippet
+snippet \Rc "" i
+⎤
+endsnippet
+snippet \varnothing "" i
+∅
+endsnippet
+snippet \empty "" i
+∅
+endsnippet
+snippet \Lam "" i
+Λ
+endsnippet
+snippet \Sig "" i
+Σ
+endsnippet
+snippet \- "" i
+∖
+endsnippet
+snippet \aa "" i
+●
+endsnippet
+snippet \af "" i
+◯
+endsnippet
+snippet \auth "" i
+●
+endsnippet
+snippet \frag "" i
+◯
+endsnippet
+snippet \iff "" i
+↔
+endsnippet
+snippet \gname "" i
+γ
+endsnippet
+snippet \incl "" i
+≼
+endsnippet
+snippet \latert "" i
+▶
+endsnippet
+snippet \update "" i
+⇝
+endsnippet
+snippet \bind "" i
+≫=
+endsnippet
+
+
+snippet ^^+ "" i
+⁺
+endsnippet
+snippet __+ "" i
+₊
+endsnippet
+snippet ^^- "" i
+⁻
+endsnippet
+snippet __0 "" i
+₀
+endsnippet
+snippet __1 "" i
+₁
+endsnippet
+snippet __2 "" i
+₂
+endsnippet
+snippet __3 "" i
+₃
+endsnippet
+snippet __4 "" i
+₄
+endsnippet
+snippet __5 "" i
+₅
+endsnippet
+snippet __6 "" i
+₆
+endsnippet
+snippet __7 "" i
+₇
+endsnippet
+snippet __8 "" i
+₈
+endsnippet
+snippet __9 "" i
+₉
+endsnippet
+
+snippet __a "" i
+ₐ
+endsnippet
+snippet __e "" i
+ₑ
+endsnippet
+snippet __h "" i
+ₕ
+endsnippet
+snippet __i "" i
+ᵢ
+endsnippet
+snippet __k "" i
+ₖ
+endsnippet
+snippet __l "" i
+ₗ
+endsnippet
+snippet __m "" i
+ₘ
+endsnippet
+snippet __n "" i
+ₙ
+endsnippet
+snippet __o "" i
+ₒ
+endsnippet
+snippet __p "" i
+ₚ
+endsnippet
+snippet __r "" i
+ᵣ
+endsnippet
+snippet __s "" i
+ₛ
+endsnippet
+snippet __t "" i
+ₜ
+endsnippet
+snippet __u "" i
+ᵤ
+endsnippet
+snippet __v "" i
+ᵥ
+endsnippet
+snippet __x "" i
+ₓ
+endsnippet
+
+snippet \Alpha "" i
+Α
+endsnippet
+snippet \alpha "" i
+α
+endsnippet
+snippet \Beta "" i
+Β
+endsnippet
+snippet \beta "" i
+β
+endsnippet
+snippet \Gamma "" i
+Γ
+endsnippet
+snippet \gamma "" i
+γ
+endsnippet
+snippet \Delta "" i
+Δ
+endsnippet
+snippet \delta "" i
+δ
+endsnippet
+snippet \Epsilon "" i
+Ε
+endsnippet
+snippet \epsilon "" i
+ε
+endsnippet
+snippet \Zeta "" i
+Ζ
+endsnippet
+snippet \zeta "" i
+ζ
+endsnippet
+snippet \Eta "" i
+Η
+endsnippet
+snippet \eta "" i
+η
+endsnippet
+snippet \Theta "" i
+Θ
+endsnippet
+snippet \theta "" i
+θ
+endsnippet
+snippet \Iota "" i
+Ι
+endsnippet
+snippet \iota "" i
+ι
+endsnippet
+snippet \Kappa "" i
+Κ
+endsnippet
+snippet \kappa "" i
+κ
+endsnippet
+snippet \Lamda "" i
+Λ
+endsnippet
+snippet \lamda "" i
+λ
+endsnippet
+snippet \Lambda "" i
+Λ
+endsnippet
+snippet \lambda "" i
+λ
+endsnippet
+snippet \Mu "" i
+Μ
+endsnippet
+snippet \mu "" i
+μ
+endsnippet
+snippet \Nu "" i
+Ν
+endsnippet
+snippet \nu "" i
+ν
+endsnippet
+snippet \Xi "" i
+Ξ
+endsnippet
+snippet \xi "" i
+ξ
+endsnippet
+snippet \Omicron "" i
+Ο
+endsnippet
+snippet \omicron "" i
+ο
+endsnippet
+snippet \Pi "" i
+Π
+endsnippet
+snippet \pi "" i
+π
+endsnippet
+snippet \Rho "" i
+Ρ
+endsnippet
+snippet \rho "" i
+ρ
+endsnippet
+snippet \Sigma "" i
+Σ
+endsnippet
+snippet \sigma "" i
+σ
+endsnippet
+snippet \Tau "" i
+Τ
+endsnippet
+snippet \tau "" i
+τ
+endsnippet
+snippet \Upsilon "" i
+Υ
+endsnippet
+snippet \upsilon "" i
+υ
+endsnippet
+snippet \Phi "" i
+Φ
+endsnippet
+snippet \phi "" i
+ϕ
+endsnippet
+snippet \varphi "" i
+φ
+endsnippet
+snippet \Chi "" i
+Χ
+endsnippet
+snippet \chi "" i
+χ
+endsnippet
+snippet \Psi "" i
+Ψ
+endsnippet
+snippet \psi "" i
+ψ
+endsnippet
+snippet \Omega "" i
+Ω
+endsnippet
+snippet \omega "" i
+ω
+endsnippet

docs/vscode

+  "generic-input-methods.input-methods": [
+        {
+            "name": "Iris Math",
+            "commandName": "text.math",
+            "languages": [
+                "coq"
+            ],
+            "triggers": [
+                "\\"
+            ],
+            "dictionary": [
+                // Standard LaTeX math notations
+                { "label": "forall", "body": "∀", "description": "∀" },
+                { "label": "exists", "body": "∃", "description": "∃" },
+                { "label": "lam", "body": "λ", "description": "λ" },
+                { "label": "not", "body": "¬", "description": "¬" },
+                { "label": "->", "body": "→", "description": "→" },
+                { "label": "<->", "body": "↔", "description": "↔" },
+                { "label": "<-", "body": "←", "description": "←" },
+                { "label": "==", "body": "≡", "description": "≡" },
+                { "label": "/==", "body": "≢", "description": "≢" },
+                { "label": "/=", "body": "≠", "description": "≠" },
+                { "label": "neq", "body": "≠", "description": "≠" },
+                { "label": "nequiv", "body": "≢", "description": "≢" },
+                { "label": "<=", "body": "≤", "description": "≤" },
+                { "label": "leq", "body": "≤", "description": "≤" },
+                { "label": "in", "body": "∈", "description": "∈" },
+                { "label": "notin", "body": "∉", "description": "∉" },
+                { "label": "cup", "body": "∪", "description": "∪" },
+                { "label": "cap", "body": "∩", "description": "∩" },
+                { "label": "setminus", "body": "∖", "description": "∖" },
+                { "label": "subset", "body": "⊂", "description": "⊂" },
+                { "label": "subseteq", "body": "⊆", "description": "⊆" },
+                { "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
+                { "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
+                { "label": "notsubseteq", "body": "⊈", "description": "⊈" },
+                { "label": "meet", "body": "⊓", "description": "⊓" },
+                { "label": "join", "body": "⊔", "description": "⊔" },
+                { "label": "top", "body": "⊤", "description": "⊤" },
+                { "label": "bottom", "body": "⊥", "description": "⊥" },
+                { "label": "vdash", "body": "⊢", "description": "⊢" },
+                { "label": "|-", "body": "⊢", "description": "⊢" },
+                { "label": "dashv", "body": "⊣", "description": "⊣" },
+                { "label": "Vdash", "body": "⊨", "description": "⊨" },
+                { "label": "infty", "body": "∞", "description": "∞" },
+                { "label": "comp", "body": "∘", "description": "∘" },
+                { "label": "prf", "body": "↾", "description": "↾" },
+                { "label": "bind", "body": "≫=", "description": "≫=" },
+                { "label": "mapsto", "body": "↦", "description": "↦" },
+                { "label": "hookrightarrow", "body": "↪", "description": "↪" },
+                { "label": "uparrow", "body": "↑", "description": "↑" },
+
+                // Iris specific
+                { "label": "fun", "body": "λ", "description": "λ" },
+                { "label": "mult", "body": "⋅", "description": "⋅" },
+                { "label": "ent", "body": "⊢", "description": "⊢" },
+                { "label": "valid", "body": "✓", "description": "✓" },
+                { "label": "diamond", "body": "◇", "description": "◇" },
+                { "label": "box", "body": "□", "description": "□" },
+                { "label": "bbox", "body": "■", "description": "■" },
+                { "label": "later", "body": "▷", "description": "▷" },
+                { "label": "pred", "body": "φ", "description": "φ" },
+                { "label": "and", "body": "∧", "description": "∧" },
+                { "label": "or", "body": "∨", "description": "∨" },
+                { "label": "comp", "body": "∘", "description": "∘" },
+                { "label": "ccomp", "body": "◎", "description": "◎" },
+                { "label": "all", "body": "∀", "description": "∀" },
+                { "label": "ex", "body": "∃", "description": "∃" },
+                { "label": "to", "body": "→", "description": "→" },
+                { "label": "sep", "body": "∗", "description": "∗" },
+                { "label": "star", "body": "∗", "description": "∗" },
+                { "label": "lc", "body": "⌜", "description": "⌜" },
+                { "label": "rc", "body": "⌝", "description": "⌝" },
+                { "label": "Lc", "body": "⎡", "description": "⎡" },
+                { "label": "Rc", "body": "⎤", "description": "⎤" },
+                { "label": "empty", "body": "∅", "description": "∅" },
+                { "label": "Lam", "body": "Λ", "description": "Λ" },
+                { "label": "Sig", "body": "Σ", "description": "Σ" },
+                { "label": "-", "body": "∖", "description": "∖" },
+                { "label": "aa", "body": "●", "description": "●" },
+                { "label": "af", "body": "◯", "description": "◯" },
+                { "label": "auth", "body": "●", "description": "●" },
+                { "label": "frag", "body": "◯", "description": "◯" },
+                { "label": "iff", "body": "↔", "description": "↔" },
+                { "label": "gname", "body": "γ", "description": "γ" },
+                { "label": "incl", "body": "≼", "description": "≼" },
+                { "label": "latert", "body": "▶", "description": "▶" },
+                { "label": "update", "body": "⇝", "description": "⇝" },
+                { "label": "bind", "body": "≫=", "description": "≫=" },
+
+                // accents (for iLöb)
+                { "label": "\"o", "body": "ö", "description": "ö" },
+
+                // subscripts and superscripts
+                { "label": "^^+", "body": "⁺", "description": "⁺" },
+                { "label": "__+", "body": "₊", "description": "₊" },
+                { "label": "^^-", "body": "⁻", "description": "⁻" },
+                { "label": "__0", "body": "₀", "description": "₀" },
+                { "label": "__1", "body": "₁", "description": "₁" },
+                { "label": "__2", "body": "₂", "description": "₂" },
+                { "label": "__3", "body": "₃", "description": "₃" },
+                { "label": "__4", "body": "₄", "description": "₄" },
+                { "label": "__5", "body": "₅", "description": "₅" },
+                { "label": "__6", "body": "₆", "description": "₆" },
+                { "label": "__7", "body": "₇", "description": "₇" },
+                { "label": "__8", "body": "₈", "description": "₈" },
+                { "label": "__9", "body": "₉", "description": "₉" },
+                { "label": "__a", "body": "ₐ", "description": "ₐ" },
+                { "label": "__e", "body": "ₑ", "description": "ₑ" },
+                { "label": "__h", "body": "ₕ", "description": "ₕ" },
+                { "label": "__i", "body": "ᵢ", "description": "ᵢ" },
+                { "label": "__k", "body": "ₖ", "description": "ₖ" },
+                { "label": "__l", "body": "ₗ", "description": "ₗ" },
+                { "label": "__m", "body": "ₘ", "description": "ₘ" },
+                { "label": "__n", "body": "ₙ", "description": "ₙ" },
+                { "label": "__o", "body": "ₒ", "description": "ₒ" },
+                { "label": "__p", "body": "ₚ", "description": "ₚ" },
+                { "label": "__r", "body": "ᵣ", "description": "ᵣ" },
+                { "label": "__s", "body": "ₛ", "description": "ₛ" },
+                { "label": "__t", "body": "ₜ", "description": "ₜ" },
+                { "label": "__u", "body": "ᵤ", "description": "ᵤ" },
+                { "label": "__v", "body": "ᵥ", "description": "ᵥ" },
+                { "label": "__x", "body": "ₓ", "description": "ₓ" },
+
+                // Greek alphabet
+                { "label": "Alpha", "body": "Α", "description": "Α" },
+                { "label": "alpha", "body": "α", "description": "α" },
+                { "label": "Beta", "body": "Β", "description": "Β" },
+                { "label": "beta", "body": "β", "description": "β" },
+                { "label": "Gamma", "body": "Γ", "description": "Γ" },
+                { "label": "gamma", "body": "γ", "description": "γ" },
+                { "label": "Delta", "body": "Δ", "description": "Δ" },
+                { "label": "delta", "body": "δ", "description": "δ" },
+                { "label": "Epsilon", "body": "Ε", "description": "Ε" },
+                { "label": "epsilon", "body": "ε", "description": "ε" },
+                { "label": "Zeta", "body": "Ζ", "description": "Ζ" },
+                { "label": "zeta", "body": "ζ", "description": "ζ" },
+                { "label": "Eta", "body": "Η", "description": "Η" },
+                { "label": "eta", "body": "η", "description": "η" },
+                { "label": "Theta", "body": "Θ", "description": "Θ" },
+                { "label": "theta", "body": "θ", "description": "θ" },
+                { "label": "Iota", "body": "Ι", "description": "Ι" },
+                { "label": "iota", "body": "ι", "description": "ι" },
+                { "label": "Kappa", "body": "Κ", "description": "Κ" },
+                { "label": "kappa", "body": "κ", "description": "κ" },
+                { "label": "Lamda", "body": "Λ", "description": "Λ" },
+                { "label": "lamda", "body": "λ", "description": "λ" },
+                { "label": "Lambda", "body": "Λ", "description": "Λ" },
+                { "label": "lambda", "body": "λ", "description": "λ" },
+                { "label": "Mu", "body": "Μ", "description": "Μ" },
+                { "label": "mu", "body": "μ", "description": "μ" },
+                { "label": "Nu", "body": "Ν", "description": "Ν" },
+                { "label": "nu", "body": "ν", "description": "ν" },
+                { "label": "Xi", "body": "Ξ", "description": "Ξ" },
+                { "label": "xi", "body": "ξ", "description": "ξ" },
+                { "label": "Omicron", "body": "Ο", "description": "Ο" },
+                { "label": "omicron", "body": "ο", "description": "ο" },
+                { "label": "Pi", "body": "Π", "description": "Π" },
+                { "label": "pi", "body": "π", "description": "π" },
+                { "label": "Rho", "body": "Ρ", "description": "Ρ" },
+                { "label": "rho", "body": "ρ", "description": "ρ" },
+                { "label": "Sigma", "body": "Σ", "description": "Σ" },
+                { "label": "sigma", "body": "σ", "description": "σ" },
+                { "label": "Tau", "body": "Τ", "description": "Τ" },
+                { "label": "tau", "body": "τ", "description": "τ" },
+                { "label": "Upsilon", "body": "Υ", "description": "Υ" },
+                { "label": "upsilon", "body": "υ", "description": "υ" },
+                { "label": "Phi", "body": "Φ", "description": "Φ" },
+                { "label": "phi", "body": "φ", "description": "φ" },
+                { "label": "Chi", "body": "Χ", "description": "Χ" },
+                { "label": "chi", "body": "χ", "description": "χ" },
+                { "label": "Psi", "body": "Ψ", "description": "Ψ" },
+                { "label": "psi", "body": "ψ", "description": "ψ" },
+                { "label": "Omega", "body": "Ω", "description": "Ω" },
+                { "label": "omega", "body": "ω", "description": "ω" }
+            ]
+        }
+    ]

dune

+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   (flags ; Configure the coqc flags.
+    (:standard ; Keeping the default flags.
+     ; Add custom flags (to be kept in sync with _CoqProject).
+     -w -notation-overridden
+     -w -redundant-canonical-projection
+     -w -unknown-warning
+     -w -argument-scope-delimiter
+     -w -notation-incompatible-prefix
+)))))

dune-project

+(lang dune 3.8)
+(using coq 0.8)

iris-bot

@@ -2,11 +2,16 @@
 import sys, os, subprocess
 import requests, argparse
 from datetime import datetime, timezone
+from collections import namedtuple
 
 ################################################################################
 # This script lets you autoamtically trigger some operations on the Iris CI to
 # do further test/analysis on a branch (usually an MR).
 # Set the GITLAB_TOKEN environment variable to a GitLab access token.
+# You can generate such a token at
+# <https://gitlab.mpi-sws.org/-/user_settings/personal_access_tokens>.
+# Select only the "api" scope.
+#
 # Set at least one of IRIS_REV or STDPP_REV to control which branches of these
 # projects to build against (defaults to default git branch). IRIS_REPO and
 # STDPP_REPO can be used to take branches from forks. Setting IRIS to
@@ -26,11 +31,11 @@ PROJECTS = {
     'lambda-rust': { 'name': 'lambda-rust', 'branch': 'master', 'timing': True },
     'lambda-rust-weak': { 'name': 'lambda-rust', 'branch': 'masters/weak_mem' }, # covers GPFSL and ORC11
     'examples': { 'name': 'examples', 'branch': 'master', 'timing': True },
+    'gpfsl': { 'name': 'gpfsl', 'branch': 'master', 'timing': True }, # need separate entry for timing
     'iron': { 'name': 'iron', 'branch': 'master', 'timing': True },
     'reloc': { 'name': 'reloc', 'branch': 'master' },
-    'spygame': { 'name': 'spygame', 'branch': 'master' },
-    'time-credits': { 'name': 'time-credits', 'branch': 'master' },
     'actris': { 'name': 'actris', 'branch': 'master' },
+    'simuliris': { 'name': 'simuliris', 'branch': 'master' },
     'tutorial-popl20': { 'name': 'tutorial-popl20', 'branch': 'master' },
     'tutorial-popl21': { 'name': 'tutorial-popl21', 'branch': 'master' },
 }
@@ -83,6 +88,8 @@ def build(args):
         var = project.upper()
         vars[var+"_REPO"] = repo
         vars[var+"_REV"] = rev
+    if args.coq:
+        vars["NIGHTLY_COQ"] = args.coq
     # Loop over all projects, and trigger build.
     for (name, project) in PROJECTS.items():
         if args.filter in name:
@@ -90,51 +97,77 @@ def build(args):
             pipeline_url = trigger_build(project['name'], project['branch'], vars)['web_url']
             print("    Pipeline running at {}".format(pipeline_url))
 
-def time(args):
-    # Make sure only 'iris' variables are set.
-    for project in BUILD_BRANCHES.keys():
-        if project != 'iris':
-            print("'time' command only supports Iris branches")
-            sys.exit(1)
-    (iris_repo, iris_rev) = BUILD_BRANCHES['iris']
-    # Get project to test and ensure it supports timing
-    project_name = args.project
-    if project_name not in PROJECTS:
-        print("ERROR: no such project: {}".format(project_name))
-        sys.exit(1)
-    project = PROJECTS[project_name]
-    if not project.get('timing'):
-        print("ERROR: {} does not support timing".format(project_name))
-        sys.exit(1)
+TimeJob = namedtuple("TimeJob", "id base_commit base_pipeline test_commit test_pipeline compare")
+
+def time_project(project, iris_repo, iris_rev, test_rev):
     # Obtain a unique ID for this experiment
     id = datetime.now(timezone.utc).strftime("%Y%m%d-%H%M%S")
     # Determine the branch commit to build
     subprocess.run(["git", "fetch", "-q", "https://gitlab.mpi-sws.org/{}".format(iris_repo), iris_rev], check=True)
     test_commit = subprocess.run(["git", "rev-parse", "FETCH_HEAD"], check=True, stdout=subprocess.PIPE).stdout.decode().strip()
     # Determine the base commit in master
-    subprocess.run(["git", "fetch", "-q", "origin", "master"], check=True)
-    base_commit = subprocess.run(["git", "merge-base", test_commit, "origin/master"], check=True, stdout=subprocess.PIPE).stdout.decode().strip()
+    subprocess.run(["git", "fetch", "-q", "https://gitlab.mpi-sws.org/iris/iris.git", "master"], check=True)
+    base_commit = subprocess.run(["git", "merge-base", test_commit, "FETCH_HEAD"], check=True, stdout=subprocess.PIPE).stdout.decode().strip()
     # Trigger the builds
-    print("Triggering timing builds for {} with Iris base commit {} and test commit {} using ad-hoc ID {}...".format(project_name, base_commit[:8], test_commit[:8], id))
     vars = {
         'IRIS_REPO': iris_repo,
         'IRIS_REV': base_commit,
         'TIMING_AD_HOC_ID': id+"-base",
     }
     base_pipeline = trigger_build(project['name'], project['branch'], vars)
-    print("    Base pipeline running at {}".format(base_pipeline['web_url']))
     vars = {
         'IRIS_REPO': iris_repo,
         'IRIS_REV': test_commit,
         'TIMING_AD_HOC_ID': id+"-test",
     }
-    if args.test_rev is None:
+    if test_rev is None:
+        # We hope that this repository did not change since the job we created just above...
         test_pipeline = trigger_build(project['name'], project['branch'], vars)
-        print("    Test pipeline running at {}".format(test_pipeline['web_url']))
     else:
-        test_pipeline = trigger_build(project['name'], args.test_branch, vars)
-        print("    Test pipeline (on non-standard branch {}) running at {}".format(args.test_branch, test_pipeline['web_url']))
-    print("    Once done, timing comparison will be available at https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project={}&var-branch1=@hoc&var-commit1={}&var-config1={}&var-branch2=@hoc&var-commit2={}&var-config2={}".format(project['name'], base_pipeline['sha'], id+"-base", test_pipeline['sha'], id+"-test"))
+        test_pipeline = trigger_build(project['name'], args.test_rev, vars)
+    compare = "https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project={}&var-branch1=@hoc&var-commit1={}&var-config1={}&var-branch2=@hoc&var-commit2={}&var-config2={}".format(project['name'], base_pipeline['sha'], id+"-base", test_pipeline['sha'], id+"-test")
+    return TimeJob(id, base_commit, base_pipeline['web_url'], test_commit, test_pipeline['web_url'], compare)
+
+def time(args):
+    # Make sure only 'iris' variables are set.
+    # One could imagine generalizing to "either Iris or std++", but then if the
+    # ad-hoc timing jobs honor STDPP_REV, how do we make it so that particular
+    # deterministic std++ versions are used for Iris timing? This does not
+    # currently seem worth the effort / hacks.
+    for project in BUILD_BRANCHES.keys():
+        if project != 'iris':
+            print("'time' command only supports Iris branches")
+            sys.exit(1)
+    (iris_repo, iris_rev) = BUILD_BRANCHES['iris']
+    # Special mode: time everything
+    if args.project == 'all':
+        if args.test_rev is not None:
+            print("'time all' does not support '--test-rev'")
+            sys.exit(1)
+        for (name, project) in PROJECTS.items():
+            if not project.get('timing'):
+                continue
+            job = time_project(project, iris_repo, iris_rev, None)
+            print("- [{}]({})".format(name, job.compare))
+        return
+    # Get project to test and ensure it supports timing
+    project_name = args.project
+    if project_name not in PROJECTS:
+        print("ERROR: no such project: {}".format(project_name))
+        sys.exit(1)
+    project = PROJECTS[project_name]
+    if not project.get('timing'):
+        print("ERROR: {} does not support timing".format(project_name))
+        sys.exit(1)
+    # Run it!
+    job = time_project(project, iris_repo, iris_rev, args.test_rev)
+    print("Triggering timing builds for {} with Iris base commit {} and test commit {} using ad-hoc ID {}...".format(project_name, job.base_commit[:8], job.test_commit[:8], job.id))
+    print("    Base pipeline running at {}".format(job.base_pipeline))
+    if args.test_rev is None:
+        print("    Test pipeline running at {}".format(job.test_pipeline))
+    else:
+        print("    Test pipeline (on non-standard branch {}) running at {}".format(args.test_rev, job.test_pipeline))
+    print("    Once done, timing comparison will be available at {}".format(job.compare))
 
 # Dispatch
 if __name__ == "__main__":
@@ -143,10 +176,11 @@ if __name__ == "__main__":
 
     parser_build = subparsers.add_parser('build', help='Build many reverse dependencies against an Iris branch')
     parser_build.set_defaults(func=build)
+    parser_build.add_argument('--coq', help='the (opam) Coq version to use for these tests')
     parser_build.add_argument('filter', nargs='?', default='', help='(optional) restrict build to projects matching the filter')
 
     parser_time = subparsers.add_parser('time', help='Time one reverse dependency against an Iris branch')
-    parser_time.add_argument("project", help="the project to measure the time of")
+    parser_time.add_argument("project", help="the project to measure the time of, or 'all' to measure all of them")
     parser_time.add_argument("--test-rev", help="use different revision on project for the test build (in case the project requires changes to still build)")
     parser_time.set_defaults(func=time)
 

iris/algebra/agree.v

 From iris.algebra Require Export cmra.
 From iris.prelude Require Import options.
 
-Local Arguments validN _ _ _ !_ /.
+Local Arguments validN _ _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
 Local Arguments pcore _ _ !_ /.
@@ -50,7 +50,7 @@ Proof.
 Qed.
 
 Section agree.
-Context {A : ofe}.
+Context {SI : sidx} {A : ofe}.
 Implicit Types a b : A.
 Implicit Types x y : agree A.
 
@@ -72,7 +72,7 @@ Proof.
         destruct (H2 b) as (c&?&?); eauto. by exists c; split; last etrans.
       * intros a ?. destruct (H2' a) as (b&?&?); auto.
         destruct (H1' b) as (c&?&?); eauto. by exists c; split; last etrans.
-  - intros n x y [??]; split; naive_solver eauto using dist_S.
+  - intros n m x y [??]; split; naive_solver eauto using dist_le.
 Qed.
 Canonical Structure agreeO := Ofe (agree A) agree_ofe_mixin.
 
@@ -107,12 +107,14 @@ Qed.
 Lemma agree_idemp x : x ⋅ x ≡ x.
 Proof. intros n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed.
 
-Local Instance agree_validN_ne n : Proper (dist n ==> impl) (@validN (agree A) _ n).
+Local Instance agree_validN_ne n :
+  Proper (dist n ==> impl) (@validN SI (agree A) _ n).
 Proof.
   intros x y [H H']; rewrite /impl !agree_validN_def; intros Hv a b Ha Hb.
   destruct (H' a) as (a'&?&<-); auto. destruct (H' b) as (b'&?&<-); auto.
 Qed.
-Local Instance agree_validN_proper n : Proper (equiv ==> iff) (@validN (agree A) _ n).
+Local Instance agree_validN_proper n :
+  Proper (equiv ==> iff) (@validN SI (agree A) _ n).
 Proof. move=> x y /equiv_dist H. by split; rewrite (H n). Qed.
 
 Local Instance agree_op_ne' x : NonExpansive (op x).
@@ -121,13 +123,19 @@ Proof.
 Qed.
 Local Instance agree_op_ne : NonExpansive2 (@op (agree A) _).
 Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
-Local Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (op (A := agree A)) := ne_proper_2 _.
+Local Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (op (A := agree A)) :=
+  ne_proper_2 _.
 
 Lemma agree_included x y : x ≼ y ↔ y ≡ x ⋅ y.
 Proof.
   split; [|by intros ?; exists y].
   by intros [z Hz]; rewrite Hz assoc agree_idemp.
 Qed.
+Lemma agree_includedN n x y : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y.
+Proof.
+  split; [|by intros ?; exists y].
+  by intros [z Hz]; rewrite Hz assoc agree_idemp.
+Qed.
 
 Lemma agree_op_invN n x1 x2 : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2.
 Proof.
@@ -139,7 +147,7 @@ Qed.
 Definition agree_cmra_mixin : CmraMixin (agree A).
 Proof.
   apply cmra_total_mixin; try apply _ || by eauto.
-  - intros n x; rewrite !agree_validN_def; eauto using dist_S.
+  - intros n m x; rewrite !agree_validN_def; eauto using dist_le.
   - intros x. apply agree_idemp.
   - intros n x y; rewrite !agree_validN_def /=.
     setoid_rewrite elem_of_app; naive_solver.
@@ -178,6 +186,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 +204,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,19 +216,24 @@ 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.
+Lemma to_agree_included_L `{!LeibnizEquiv A}  a b : to_agree a ≼ to_agree b ↔ a = b.
+Proof. unfold_leibniz. apply to_agree_included. Qed.
 
 Global Instance agree_cancelable x : Cancelable x.
 Proof.
@@ -232,10 +249,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.
@@ -259,8 +272,8 @@ Proof. rewrite to_agree_op_valid. by fold_leibniz. Qed.
 End agree.
 
 Global Instance: Params (@to_agree) 1 := {}.
-Global Arguments agreeO : clear implicits.
-Global Arguments agreeR : clear implicits.
+Global Arguments agreeO {_} _.
+Global Arguments agreeR {_} _.
 
 Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
   {| agree_car := f <$> agree_car x |}.
@@ -275,7 +288,7 @@ Lemma agree_map_to_agree {A B} (f : A → B) (x : A) :
 Proof. by apply agree_eq. Qed.
 
 Section agree_map.
-  Context {A B : ofe} (f : A → B) {Hf: NonExpansive f}.
+  Context {SI : sidx} {A B : ofe} (f : A → B) {Hf: NonExpansive f}.
 
   Local Instance agree_map_ne : NonExpansive (agree_map f).
   Proof using Type*.
@@ -305,31 +318,34 @@ Section agree_map.
   Qed.
 End agree_map.
 
-Definition agreeO_map {A B} (f : A -n> B) : agreeO A -n> agreeO B :=
+Definition agreeO_map {SI : sidx} {A B : ofe}
+    (f : A -n> B) : agreeO A -n> agreeO B :=
   OfeMor (agree_map f : agreeO A → agreeO B).
-Global Instance agreeO_map_ne A B : NonExpansive (@agreeO_map A B).
+Global Instance agreeO_map_ne {SI : sidx} A B : NonExpansive (@agreeO_map SI A B).
 Proof.
   intros n f g Hfg x; split=> b /=;
     setoid_rewrite elem_of_list_fmap; naive_solver.
 Qed.
 
-Program Definition agreeRF (F : oFunctor) : rFunctor := {|
+Program Definition agreeRF {SI : sidx} (F : oFunctor) : rFunctor := {|
   rFunctor_car A _ B _ := agreeR (oFunctor_car F A B);
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_map_ne.
+  intros ? ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
+  by apply agreeO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
-  intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
+  intros ? F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
   apply (agree_map_ext _)=>y. by rewrite oFunctor_map_id.
 Qed.
 Next Obligation.
-  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -agree_map_compose.
+  intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl.
+  rewrite -agree_map_compose.
   apply (agree_map_ext _)=>y; apply oFunctor_map_compose.
 Qed.
 
-Global Instance agreeRF_contractive F :
+Global Instance agreeRF_contractive {SI : sidx} F :
   oFunctorContractive F → rFunctorContractive (agreeRF F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.

iris/algebra/auth.v

@@ -5,7 +5,7 @@ From iris.prelude Require Import options.
 (** The authoritative camera with fractional authoritative elements *)
 (** The authoritative camera has 2 types of elements: the authoritative element
 [●{dq} a] and the fragment [◯ b] (of which there can be several). To enable
-sharing of the authoritative element [●{dq} a], it is equiped with a
+sharing of the authoritative element [●{dq} a], it is equipped with a
 discardable fraction [dq]. Updates are only possible with the full
 authoritative element [● a] (syntax for [●{#1} a]]), while fractional
 authoritative elements have agreement, i.e., [✓ (●{dq1} a1 ⋅ ●{dq2} a2) → a1 ≡
@@ -13,39 +13,40 @@ a2]. *)
 
 (** * Definition of the view relation *)
 (** The authoritative camera is obtained by instantiating the view camera. *)
-Definition auth_view_rel_raw {A : ucmra} (n : nat) (a b : A) : Prop :=
+Definition auth_view_rel_raw {SI : sidx} {A : ucmra} (n : SI) (a b : A) : Prop :=
   b ≼{n} a ∧ ✓{n} a.
-Lemma auth_view_rel_raw_mono (A : ucmra) n1 n2 (a1 a2 b1 b2 : A) :
+Lemma auth_view_rel_raw_mono {SI : sidx} (A : ucmra) n1 n2 (a1 a2 b1 b2 : A) :
   auth_view_rel_raw n1 a1 b1 →
   a1 ≡{n2}≡ a2 →
   b2 ≼{n2} b1 →
-  n2 ≤ n1 →
+  (n2 ≤ n1)%sidx →
   auth_view_rel_raw n2 a2 b2.
 Proof.
   intros [??] Ha12 ??. split.
   - trans b1; [done|]. rewrite -Ha12. by apply cmra_includedN_le with n1.
   - rewrite -Ha12. by apply cmra_validN_le with n1.
 Qed.
-Lemma auth_view_rel_raw_valid (A : ucmra) n (a b : A) :
+Lemma auth_view_rel_raw_valid {SI : sidx} (A : ucmra) n (a b : A) :
   auth_view_rel_raw n a b → ✓{n} b.
 Proof. intros [??]; eauto using cmra_validN_includedN. Qed.
-Lemma auth_view_rel_raw_unit (A : ucmra) n :
+Lemma auth_view_rel_raw_unit {SI : sidx} (A : ucmra) n :
   ∃ a : A, auth_view_rel_raw n a ε.
 Proof. exists ε. split; [done|]. apply ucmra_unit_validN. Qed.
-Canonical Structure auth_view_rel {A : ucmra} : view_rel A A :=
+Canonical Structure auth_view_rel {SI : sidx} {A : ucmra} : view_rel A A :=
   ViewRel auth_view_rel_raw (auth_view_rel_raw_mono A)
           (auth_view_rel_raw_valid A) (auth_view_rel_raw_unit A).
 
-Lemma auth_view_rel_unit {A : ucmra} n (a : A) : auth_view_rel n a ε ↔ ✓{n} a.
+Lemma auth_view_rel_unit {SI : sidx} {A : ucmra} n (a : A) :
+  auth_view_rel n a ε ↔ ✓{n} a.
 Proof. split; [by intros [??]|]. split; auto using ucmra_unit_leastN. Qed.
-Lemma auth_view_rel_exists {A : ucmra} n (b : A) :
+Lemma auth_view_rel_exists {SI : sidx} {A : ucmra} n (b : A) :
   (∃ a, auth_view_rel n a b) ↔ ✓{n} b.
 Proof.
   split; [|intros; exists b; by split].
   intros [a Hrel]. eapply auth_view_rel_raw_valid, Hrel.
 Qed.
 
-Global Instance auth_view_rel_discrete {A : ucmra} :
+Global Instance auth_view_rel_discrete {SI : sidx} {A : ucmra} :
   CmraDiscrete A → ViewRelDiscrete (auth_view_rel (A:=A)).
 Proof.
   intros ? n a b [??]; split.
@@ -58,24 +59,23 @@ Qed.
 This way, one can use [auth A] with [A : Type] instead of [A : ucmra], and let
 canonical structure search determine the corresponding camera instance. *)
 Notation auth A := (view (A:=A) (B:=A) auth_view_rel_raw).
-Definition authO (A : ucmra) : ofe := viewO (A:=A) (B:=A) auth_view_rel.
-Definition authR (A : ucmra) : cmra := viewR (A:=A) (B:=A) auth_view_rel.
-Definition authUR (A : ucmra) : ucmra := viewUR (A:=A) (B:=A) auth_view_rel.
+Definition authO {SI : sidx} (A : ucmra) : ofe :=
+  viewO (A:=A) (B:=A) auth_view_rel.
+Definition authR {SI : sidx} (A : ucmra) : cmra :=
+  viewR (A:=A) (B:=A) auth_view_rel.
+Definition authUR {SI : sidx} (A : ucmra) : ucmra :=
+  viewUR (A:=A) (B:=A) auth_view_rel.
 
-Definition auth_auth {A: ucmra} : dfrac → A → auth A := view_auth.
-Definition auth_frag {A: ucmra} : A → auth A := view_frag.
+Definition auth_auth {SI : sidx} {A: ucmra} : dfrac → A → auth A := view_auth.
+Definition auth_frag {SI : sidx} {A: ucmra} : A → auth A := view_frag.
 
-Typeclasses Opaque auth_auth auth_frag.
+Global Typeclasses Opaque auth_auth auth_frag.
 
-Global Instance: Params (@auth_auth) 2 := {}.
-Global Instance: Params (@auth_frag) 1 := {}.
+Global Instance: Params (@auth_auth) 3 := {}.
+Global Instance: Params (@auth_frag) 2 := {}.
 
-(** FIXME: Refactor these notations using custom entries once Coq bug #13654
-has been fixed. *)
-Notation "●{ dq } a" := (auth_auth dq a) (at level 20, format "●{ dq }  a").
-Notation "●{# q } a" := (auth_auth (DfracOwn q) a) (at level 20, format "●{# q }  a").
-Notation "●□ a" := (auth_auth (DfracDiscarded) a) (at level 20).
-Notation "● a" := (auth_auth (DfracOwn 1) a) (at level 20).
+Notation "● dq a" := (auth_auth dq a)
+  (at level 20, dq custom dfrac at level 1, format "● dq  a").
 Notation "◯ a" := (auth_frag a) (at level 20).
 
 (** * Laws of the authoritative camera *)
@@ -83,28 +83,29 @@ Notation "◯ a" := (auth_frag a) (at level 20).
 general version in terms of [●] and [◯], and because such a lemma has never
 been needed in practice. *)
 Section auth.
-  Context {A : ucmra}.
+  Context {SI : sidx} {A : ucmra}.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
   Implicit Types q : frac.
   Implicit Types dq : dfrac.
 
-  Global Instance auth_auth_ne dq : NonExpansive (@auth_auth A dq).
+  Global Instance auth_auth_ne dq : NonExpansive (@auth_auth SI A dq).
   Proof. rewrite /auth_auth. apply _. Qed.
-  Global Instance auth_auth_proper dq : Proper ((≡) ==> (≡)) (@auth_auth A dq).
+  Global Instance auth_auth_proper dq : Proper ((≡) ==> (≡)) (@auth_auth SI A dq).
   Proof. rewrite /auth_auth. apply _. Qed.
-  Global Instance auth_frag_ne : NonExpansive (@auth_frag A).
+  Global Instance auth_frag_ne : NonExpansive (@auth_frag SI A).
   Proof. rewrite /auth_frag. apply _. Qed.
-  Global Instance auth_frag_proper : Proper ((≡) ==> (≡)) (@auth_frag A).
+  Global Instance auth_frag_proper : Proper ((≡) ==> (≡)) (@auth_frag SI A).
   Proof. rewrite /auth_frag. apply _. Qed.
 
-  Global Instance auth_auth_dist_inj n : Inj2 (=) (dist n) (dist n) (@auth_auth A).
+  Global Instance auth_auth_dist_inj n :
+    Inj2 (=) (dist n) (dist n) (@auth_auth SI A).
   Proof. rewrite /auth_auth. apply _. Qed.
-  Global Instance auth_auth_inj : Inj2 (=) (≡) (≡) (@auth_auth A).
+  Global Instance auth_auth_inj : Inj2 (=) (≡) (≡) (@auth_auth SI A).
   Proof. rewrite /auth_auth. apply _. Qed.
-  Global Instance auth_frag_dist_inj n : Inj (dist n) (dist n) (@auth_frag A).
+  Global Instance auth_frag_dist_inj n : Inj (dist n) (dist n) (@auth_frag SI A).
   Proof. rewrite /auth_frag. apply _. Qed.
-  Global Instance auth_frag_inj : Inj (≡) (≡) (@auth_frag A).
+  Global Instance auth_frag_inj : Inj (≡) (≡) (@auth_frag SI A).
   Proof. rewrite /auth_frag. apply _. Qed.
 
   Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete (authO A).
@@ -120,8 +121,6 @@ Section auth.
   (** Operation *)
   Lemma auth_auth_dfrac_op dq1 dq2 a : ●{dq1 ⋅ dq2} a ≡ ●{dq1} a ⋅ ●{dq2} a.
   Proof. apply view_auth_dfrac_op. Qed.
-  Lemma auth_auth_frac_op q1 q2 a : ●{#(q1 + q2)} a ≡ ●{#q1} a ⋅ ●{#q2} a.
-  Proof. apply view_auth_frac_op. Qed.
   Global Instance auth_auth_dfrac_is_op dq dq1 dq2 a :
     IsOp dq dq1 dq2 → IsOp' (●{dq} a) (●{dq1} a) (●{dq2} a).
   Proof. rewrite /auth_auth. apply _. Qed.
@@ -132,15 +131,24 @@ Section auth.
   Proof. apply view_frag_mono. Qed.
   Lemma auth_frag_core a : core (◯ a) = ◯ (core a).
   Proof. apply view_frag_core. Qed.
+  Lemma auth_both_core_discarded a b :
+    core (●□ a ⋅ ◯ b) ≡ ●□ a ⋅ ◯ (core b).
+  Proof. apply view_both_core_discarded. Qed.
+  Lemma auth_both_core_frac q a b :
+    core (●{#q} a ⋅ ◯ b) ≡ ◯ (core b).
+  Proof. apply view_both_core_frac. Qed.
+
   Global Instance auth_auth_core_id a : CoreId (●□ a).
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
   Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_both_core_id a1 a2 : CoreId a2 → CoreId (●□ a1 ⋅ ◯ a2).
+  Proof. rewrite /auth_auth /auth_frag. apply _. Qed.
   Global Instance auth_frag_is_op a b1 b2 :
     IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
   Proof. rewrite /auth_frag. apply _. Qed.
   Global Instance auth_frag_sep_homomorphism :
-    MonoidHomomorphism op op (≡) (@auth_frag A).
+    MonoidHomomorphism op op (≡) (@auth_frag SI A).
   Proof. rewrite /auth_frag. apply _. Qed.
 
   Lemma big_opL_auth_frag {B} (g : nat → B → A) (l : list B) :
@@ -265,7 +273,7 @@ Section auth.
     ✓ (●{dq} a ⋅ ◯ b) ↔ ✓ dq ∧ b ≼ a ∧ ✓ a.
   Proof.
     rewrite auth_both_dfrac_valid. setoid_rewrite <-cmra_discrete_included_iff.
-    naive_solver eauto using O.
+    pose 0ᵢ. naive_solver.
   Qed.
   Lemma auth_both_valid_discrete `{!CmraDiscrete A} a b :
     ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
@@ -329,6 +337,10 @@ Section auth.
   Qed.
   Lemma auth_update_auth_persist dq a : ●{dq} a ~~> ●□ a.
   Proof. apply view_update_auth_persist. Qed.
+  Lemma auth_updateP_auth_unpersist a : ●□ a ~~>: λ k, ∃ q, k = ●{#q} a.
+  Proof. apply view_updateP_auth_unpersist. Qed.
+  Lemma auth_updateP_both_unpersist a b : ●□ a ⋅ ◯ b ~~>: λ k, ∃ q, k = ●{#q} a ⋅ ◯ b.
+  Proof. apply view_updateP_both_unpersist. Qed.
 
   Lemma auth_update_dfrac_alloc dq a b `{!CoreId b} :
     b ≼ a → ●{dq} a ~~> ●{dq} a ⋅ ◯ b.
@@ -348,45 +360,45 @@ Section auth.
 End auth.
 
 (** * Functor *)
-Program Definition authURF (F : urFunctor) : urFunctor := {|
+Program Definition authURF {SI : sidx} (F : urFunctor) : urFunctor := {|
   urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
     viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
 |}.
 Next Obligation.
-  intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
+  intros ? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
   apply viewO_map_ne; by apply urFunctor_map_ne.
 Qed.
 Next Obligation.
-  intros F A ? B ? x; simpl in *. rewrite -{2}(view_map_id x).
+  intros ? F A ? B ? x; simpl in *. rewrite -{2}(view_map_id x).
   apply (view_map_ext _ _ _ _)=> y; apply urFunctor_map_id.
 Qed.
 Next Obligation.
-  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
+  intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
   rewrite -view_map_compose.
   apply (view_map_ext _ _ _ _)=> y; apply urFunctor_map_compose.
 Qed.
 Next Obligation.
-  intros F A1 ? A2 ? B1 ? B2 ? fg; simpl.
+  intros ? F A1 ? A2 ? B1 ? B2 ? fg; simpl.
   apply view_map_cmra_morphism; [apply _..|]=> n a b [??]; split.
   - by apply (cmra_morphism_monotoneN _).
   - by apply (cmra_morphism_validN _).
 Qed.
 
-Global Instance authURF_contractive F :
+Global Instance authURF_contractive {SI : sidx} F :
   urFunctorContractive F → urFunctorContractive (authURF F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
   apply viewO_map_ne; by apply urFunctor_map_contractive.
 Qed.
 
-Program Definition authRF (F : urFunctor) : rFunctor := {|
+Program Definition authRF {SI : sidx} (F : urFunctor) : rFunctor := {|
   rFunctor_car A _ B _ := authR (urFunctor_car F A B);
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
     viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
 |}.
-Solve Obligations with apply authURF.
+Solve Obligations with apply @authURF.
 
-Global Instance authRF_contractive F :
+Global Instance authRF_contractive {SI : sidx} F :
   urFunctorContractive F → rFunctorContractive (authRF F).
 Proof. apply authURF_contractive. Qed.

iris/algebra/big_op.v

@@ -20,14 +20,15 @@ Since these big operators are like quantifiers, they have the same precedence as
 [∀] and [∃]. *)
 
 (** * Big ops over lists *)
-Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M :=
+Fixpoint big_opL {SI : sidx} {M : ofe}
+    {o : M → M → M} `{!Monoid o} {A} (f : nat → A → M) (xs : list A) : M :=
   match xs with
   | [] => monoid_unit
   | x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
   end.
-Global Instance: Params (@big_opL) 4 := {}.
-Global Arguments big_opL {M} o {_ A} _ !_ /.
-Typeclasses Opaque big_opL.
+Global Instance: Params (@big_opL) 5 := {}.
+Global Arguments big_opL {SI} {M} o {_ A} _ !_ /.
+Global Typeclasses Opaque big_opL.
 Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
   (at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
    format "[^ o  list]  k ↦ x  ∈  l ,  P") : stdpp_scope.
@@ -35,13 +36,15 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
   (at level 200, o at level 1, l at level 10, x at level 1, right associativity,
    format "[^ o  list]  x  ∈  l ,  P") : stdpp_scope.
 
-Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K → A → M)
+Local Definition big_opM_def {SI : sidx} {M : ofe}
+  {o : M → M → M}  `{!Monoid o} `{Countable K} {A} (f : K → A → M)
   (m : gmap K A) : M := big_opL o (λ _, uncurry f) (map_to_list m).
-Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
+Local Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
 Definition big_opM := big_opM_aux.(unseal).
-Global Arguments big_opM {M} o {_ K _ _ A} _ _.
-Definition big_opM_eq : @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
-Global Instance: Params (@big_opM) 7 := {}.
+Global Arguments big_opM {SI} {M} o {_ K _ _ A} _ _.
+Local Definition big_opM_unseal :
+  @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
+Global Instance: Params (@big_opM) 8 := {}.
 Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
   (at level 200, o at level 1, m at level 10, k, x at level 1, right associativity,
    format "[^  o  map]  k ↦ x  ∈  m ,  P") : stdpp_scope.
@@ -49,31 +52,35 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
   (at level 200, o at level 1, m at level 10, x at level 1, right associativity,
    format "[^ o  map]  x  ∈  m ,  P") : stdpp_scope.
 
-Definition big_opS_def `{Monoid M o} `{Countable A} (f : A → M)
+Local Definition big_opS_def {SI : sidx} {M : ofe}
+  {o : M → M → M} `{!Monoid o} `{Countable A} (f : A → M)
   (X : gset A) : M := big_opL o (λ _, f) (elements X).
-Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
+Local Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
 Definition big_opS := big_opS_aux.(unseal).
-Global Arguments big_opS {M} o {_ A _ _} _ _.
-Definition big_opS_eq : @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
-Global Instance: Params (@big_opS) 6 := {}.
+Global Arguments big_opS {SI} {M} o {_ A _ _} _ _.
+Local Definition big_opS_unseal :
+  @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
+Global Instance: Params (@big_opS) 7 := {}.
 Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
   (at level 200, o at level 1, X at level 10, x at level 1, right associativity,
    format "[^ o  set]  x  ∈  X ,  P") : stdpp_scope.
 
-Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A → M)
+Local Definition big_opMS_def {SI : sidx} {M : ofe}
+  {o : M → M → M} `{!Monoid o} `{Countable A} (f : A → M)
   (X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
-Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
+Local Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
 Definition big_opMS := big_opMS_aux.(unseal).
-Global Arguments big_opMS {M} o {_ A _ _} _ _.
-Definition big_opMS_eq : @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
-Global Instance: Params (@big_opMS) 6 := {}.
+Global Arguments big_opMS {SI} {M} o {_ A _ _} _ _.
+Local Definition big_opMS_unseal :
+  @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
+Global Instance: Params (@big_opMS) 8 := {}.
 Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
   (at level 200, o at level 1, X at level 10, x at level 1, right associativity,
    format "[^ o  mset]  x  ∈  X ,  P") : stdpp_scope.
 
 (** * Properties about big ops *)
 Section big_op.
-Context `{Monoid M o}.
+Context {SI : sidx} {M : ofe} {o : M → M → M} `{!Monoid o}.
 Implicit Types xs : list M.
 Infix "`o`" := o (at level 50, left associativity).
 
@@ -104,6 +111,16 @@ Section list.
   Lemma big_opL_unit l : ([^o list] k↦y ∈ l, monoid_unit) ≡ (monoid_unit : M).
   Proof. induction l; rewrite /= ?left_id //. Qed.
 
+  Lemma big_opL_take_drop Φ l n :
+    ([^o list] k ↦ x ∈ l, Φ k x) ≡
+    ([^o list] k ↦ x ∈ take n l, Φ k x) `o` ([^o list] k ↦ x ∈ drop n l, Φ (n + k) x).
+  Proof.
+    rewrite -{1}(take_drop n l) big_opL_app length_take.
+    destruct (decide (length l ≤ n)).
+    - rewrite drop_ge //=.
+    - rewrite Nat.min_l //=; lia.
+  Qed.
+
   Lemma big_opL_gen_proper_2 {B} (R : relation M) f (g : nat → B → M)
         l1 (l2 : list B) :
     R monoid_unit monoid_unit →
@@ -210,6 +227,18 @@ Section list.
     revert f g; induction l as [|x l IH]=> f g /=; first by rewrite left_id.
     by rewrite IH -!assoc (assoc _ (g _ _)) [(g _ _ `o` _)]comm -!assoc.
   Qed.
+
+  (** Shows that some property [P] is closed under [big_opL]. Examples of [P]
+  are [Persistent], [Affine], [Timeless]. *)
+  Lemma big_opL_closed (P : M → Prop) f l :
+    P monoid_unit →
+    (∀ x y, P x → P y → P (x `o` y)) →
+    (∀ k x, l !! k = Some x → P (f k x)) →
+    P ([^o list] k↦x ∈ l, f k x).
+  Proof.
+    intros Hunit Hop. revert f. induction l as [|x l IH]=> f Hf /=; [done|].
+    apply Hop; first by auto. apply IH=> k. apply (Hf (S k)).
+  Qed.
 End list.
 
 Lemma big_opL_bind {A B} (h : A → list B) (f : B → M) l :
@@ -242,12 +271,12 @@ Proof. by apply big_opL_sep_zip_with. Qed.
 
 Lemma big_opM_empty `{Countable K} {B} (f : K → B → M) :
   ([^o map] k↦x ∈ ∅, f k x) = monoid_unit.
-Proof. by rewrite big_opM_eq /big_opM_def map_to_list_empty. Qed.
+Proof. by rewrite big_opM_unseal /big_opM_def map_to_list_empty. Qed.
 
 Lemma big_opM_insert `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x :
   m !! i = None →
   ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ m, f k y.
-Proof. intros ?. by rewrite big_opM_eq /big_opM_def map_to_list_insert. Qed.
+Proof. intros ?. by rewrite big_opM_unseal /big_opM_def map_to_list_insert. Qed.
 
 Lemma big_opM_delete `{Countable K} {B} (f : K → B → M) (m : gmap K B) i x :
   m !! i = Some x →
@@ -294,7 +323,7 @@ Section gmap.
     (∀ k x, m !! k = Some x → R (f k x) (g k x)) →
     R ([^o map] k ↦ x ∈ m, f k x) ([^o map] k ↦ x ∈ m, g k x).
   Proof.
-    intros ?? Hf. rewrite big_opM_eq. apply (big_opL_gen_proper R); auto.
+    intros ?? Hf. rewrite big_opM_unseal. apply (big_opL_gen_proper R); auto.
     intros k [i x] ?%elem_of_list_lookup_2. by apply Hf, elem_of_map_to_list.
   Qed.
 
@@ -343,7 +372,14 @@ Section gmap.
   [setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
   Lemma big_opM_map_to_list f m :
     ([^o map] k↦x ∈ m, f k x) ≡ [^o list] xk ∈ map_to_list m, f (xk.1) (xk.2).
-  Proof. rewrite big_opM_eq. apply big_opL_proper'; [|done]. by intros ? [??]. Qed.
+  Proof. rewrite big_opM_unseal. apply big_opL_proper'; [|done]. by intros ? [??]. Qed.
+  Lemma big_opM_list_to_map f l :
+    NoDup l.*1 →
+    ([^o map] k↦x ∈ list_to_map l, f k x) ≡ [^o list] xk ∈ l, f (xk.1) (xk.2).
+  Proof.
+    intros. rewrite big_opM_map_to_list.
+    by apply big_opL_permutation, map_to_list_to_map.
+  Qed.
 
   Lemma big_opM_singleton f i x : ([^o map] k↦y ∈ {[i:=x]}, f k y) ≡ f i x.
   Proof.
@@ -353,13 +389,13 @@ Section gmap.
 
   Lemma big_opM_unit m : ([^o map] k↦y ∈ m, monoid_unit) ≡ (monoid_unit : M).
   Proof.
-    by induction m using map_ind; rewrite /= ?big_opM_insert ?left_id // big_opM_eq.
+    by induction m using map_ind; rewrite /= ?big_opM_insert ?left_id // big_opM_unseal.
   Qed.
 
   Lemma big_opM_fmap {B} (h : A → B) (f : K → B → M) m :
     ([^o map] k↦y ∈ h <$> m, f k y) ≡ ([^o map] k↦y ∈ m, f k (h y)).
   Proof.
-    rewrite big_opM_eq /big_opM_def map_to_list_fmap big_opL_fmap.
+    rewrite big_opM_unseal /big_opM_def map_to_list_fmap big_opL_fmap.
     by apply big_opL_proper=> ? [??].
   Qed.
 
@@ -411,8 +447,8 @@ Section gmap.
     induction m as [|k v m ? IH] using map_ind.
     { by rewrite map_filter_empty !big_opM_empty. }
     destruct (decide (φ (k, v))).
-    - rewrite map_filter_insert //.
-      assert (filter φ m !! k = None) by (apply map_filter_lookup_None; eauto).
+    - rewrite map_filter_insert_True //.
+      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.
@@ -435,7 +471,23 @@ Section gmap.
     ([^o map] k↦x ∈ m, f k x `o` g k x)
     ≡ ([^o map] k↦x ∈ m, f k x) `o` ([^o map] k↦x ∈ m, g k x).
   Proof.
-    rewrite big_opM_eq /big_opM_def -big_opL_op. by apply big_opL_proper=> ? [??].
+    rewrite big_opM_unseal /big_opM_def -big_opL_op. by apply big_opL_proper=> ? [??].
+  Qed.
+
+  (** Shows that some property [P] is closed under [big_opM]. Examples of [P]
+  are [Persistent], [Affine], [Timeless]. *)
+  Lemma big_opM_closed (P : M → Prop) f m :
+    Proper ((≡) ==> iff) P →
+    P monoid_unit →
+    (∀ x y, P x → P y → P (x `o` y)) →
+    (∀ k x, m !! k = Some x → P (f k x)) →
+    P ([^o map] k↦x ∈ m, f k x).
+  Proof.
+    intros ?? Hop Hf. induction m as [|k x ?? IH] using map_ind.
+    { by rewrite big_opM_empty. }
+    rewrite big_opM_insert //. apply Hop.
+    { apply Hf. by rewrite lookup_insert. }
+    apply IH=> k' x' ?. apply Hf. rewrite lookup_insert_ne; naive_solver.
   Qed.
 End gmap.
 
@@ -473,7 +525,7 @@ Section gset.
     (∀ x, x ∈ X → R (f x) (g x)) →
     R ([^o set] x ∈ X, f x) ([^o set] x ∈ X, g x).
   Proof.
-    rewrite big_opS_eq. intros ?? Hf. apply (big_opL_gen_proper R); auto.
+    rewrite big_opS_unseal. intros ?? Hf. apply (big_opL_gen_proper R); auto.
     intros k x ?%elem_of_list_lookup_2. by apply Hf, elem_of_elements.
   Qed.
 
@@ -504,10 +556,10 @@ Section gset.
   [setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
   Lemma big_opS_elements f X :
     ([^o set] x ∈ X, f x) ≡ [^o list] x ∈ elements X, f x.
-  Proof. by rewrite big_opS_eq. Qed.
+  Proof. by rewrite big_opS_unseal. Qed.
 
   Lemma big_opS_empty f : ([^o set] x ∈ ∅, f x) = monoid_unit.
-  Proof. by rewrite big_opS_eq /big_opS_def elements_empty. Qed.
+  Proof. by rewrite big_opS_unseal /big_opS_def elements_empty. Qed.
 
   Lemma big_opS_insert f X x :
     x ∉ X → ([^o set] y ∈ {[ x ]} ∪ X, f y) ≡ (f x `o` [^o set] y ∈ X, f y).
@@ -547,7 +599,7 @@ Section gset.
 
   Lemma big_opS_unit X : ([^o set] y ∈ X, monoid_unit) ≡ (monoid_unit : M).
   Proof.
-    by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_eq.
+    by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_unseal.
   Qed.
 
   Lemma big_opS_filter' (φ : A → Prop) `{∀ x, Decision (φ x)} f X :
@@ -577,6 +629,22 @@ Section gset.
     - rewrite /= big_opS_union; last set_solver.
       by rewrite big_opS_singleton IHl.
   Qed.
+
+  (** Shows that some property [P] is closed under [big_opS]. Examples of [P]
+  are [Persistent], [Affine], [Timeless]. *)
+  Lemma big_opS_closed (P : M → Prop) f X :
+    Proper ((≡) ==> iff) P →
+    P monoid_unit →
+    (∀ x y, P x → P y → P (x `o` y)) →
+    (∀ x, x ∈ X → P (f x)) →
+    P ([^o set] x ∈ X, f x).
+  Proof.
+    intros ?? Hop Hf. induction X as [|x X ? IH] using set_ind_L.
+    { by rewrite big_opS_empty. }
+    rewrite big_opS_insert //. apply Hop.
+    { apply Hf. set_solver. }
+    apply IH=> x' ?. apply Hf. set_solver.
+  Qed.
 End gset.
 
 Lemma big_opS_set_map `{Countable A, Countable B} (h : A → B) (X : gset A) (f : B → M) :
@@ -592,12 +660,18 @@ Proof.
 Qed.
 
 Lemma big_opM_dom `{Countable K} {A} (f : K → M) (m : gmap K A) :
-  ([^o map] k↦_ ∈ m, f k) ≡ ([^o set] k ∈ dom _ m, f k).
+  ([^o map] k↦_ ∈ m, f k) ≡ ([^o set] k ∈ dom m, f k).
 Proof.
   induction m as [|i x ?? IH] using map_ind.
-  { by rewrite big_opM_eq big_opS_eq dom_empty_L. }
+  { by rewrite big_opM_unseal big_opS_unseal dom_empty_L. }
   by rewrite dom_insert_L big_opM_insert // IH big_opS_insert ?not_elem_of_dom.
 Qed.
+Lemma big_opM_gset_to_gmap `{Countable K} {A} (f : K → A → M) (X : gset K) c :
+  ([^o map] k↦a ∈ gset_to_gmap c X, f k a) ≡ ([^o set] k ∈ X, f k c).
+Proof.
+  rewrite -{2}(dom_gset_to_gmap X c) -big_opM_dom.
+  apply big_opM_proper. by intros k ? [_ ->]%lookup_gset_to_gmap_Some.
+Qed.
 
 (** ** Big ops over finite msets *)
 Section gmultiset.
@@ -610,7 +684,7 @@ Section gmultiset.
     (∀ x, x ∈ X → R (f x) (g x)) →
     R ([^o mset] x ∈ X, f x) ([^o mset] x ∈ X, g x).
   Proof.
-    rewrite big_opMS_eq. intros ?? Hf. apply (big_opL_gen_proper R); auto.
+    rewrite big_opMS_unseal. intros ?? Hf. apply (big_opL_gen_proper R); auto.
     intros k x ?%elem_of_list_lookup_2. by apply Hf, gmultiset_elem_of_elements.
   Qed.
 
@@ -641,18 +715,18 @@ Section gmultiset.
   [setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
   Lemma big_opMS_elements f X :
     ([^o mset] x ∈ X, f x) ≡ [^o list] x ∈ elements X, f x.
-  Proof. by rewrite big_opMS_eq. Qed.
+  Proof. by rewrite big_opMS_unseal. Qed.
 
   Lemma big_opMS_empty f : ([^o mset] x ∈ ∅, f x) = monoid_unit.
-  Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. Qed.
+  Proof. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_empty. Qed.
 
   Lemma big_opMS_disj_union f X Y :
     ([^o mset] y ∈ X ⊎ Y, f y) ≡ ([^o mset] y ∈ X, f y) `o` [^o mset] y ∈ Y, f y.
-  Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
+  Proof. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
 
   Lemma big_opMS_singleton f x : ([^o mset] y ∈ {[+ x +]}, f y) ≡ f x.
   Proof.
-    intros. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_singleton /= right_id.
+    intros. by rewrite big_opMS_unseal /big_opMS_def gmultiset_elements_singleton /= right_id.
   Qed.
 
   Lemma big_opMS_insert f X x :
@@ -669,12 +743,28 @@ Section gmultiset.
   Lemma big_opMS_unit X : ([^o mset] y ∈ X, monoid_unit) ≡ (monoid_unit : M).
   Proof.
     by induction X using gmultiset_ind;
-      rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id // big_opMS_eq.
+      rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id // big_opMS_unseal.
   Qed.
 
   Lemma big_opMS_op f g X :
     ([^o mset] y ∈ X, f y `o` g y) ≡ ([^o mset] y ∈ X, f y) `o` ([^o mset] y ∈ X, g y).
-  Proof. by rewrite big_opMS_eq /big_opMS_def -big_opL_op. Qed.
+  Proof. by rewrite big_opMS_unseal /big_opMS_def -big_opL_op. Qed.
+
+  (** Shows that some property [P] is closed under [big_opMS]. Examples of [P]
+  are [Persistent], [Affine], [Timeless]. *)
+  Lemma big_opMS_closed (P : M → Prop) f X :
+    Proper ((≡) ==> iff) P →
+    P monoid_unit →
+    (∀ x y, P x → P y → P (x `o` y)) →
+    (∀ x, x ∈ X → P (f x)) →
+    P ([^o mset] x ∈ X, f x).
+  Proof.
+    intros ?? Hop Hf. induction X as [|x X IH] using gmultiset_ind.
+    { by rewrite big_opMS_empty. }
+    rewrite big_opMS_insert //. apply Hop.
+    { apply Hf. set_solver. }
+    apply IH=> x' ?. apply Hf. set_solver.
+  Qed.
 End gmultiset.
 
 (** Commuting lemmas *)
@@ -773,7 +863,8 @@ Proof. repeat setoid_rewrite big_opMS_elements. by rewrite big_opL_opL. Qed.
 End big_op.
 
 Section homomorphisms.
-  Context `{Monoid M1 o1, Monoid M2 o2}.
+  Context {SI : sidx} {M1 M2 : ofe}.
+  Context {o1 : M1 → M1 → M1} {o2 : M2 → M2 → M2} `{!Monoid o1, !Monoid o2}.
   Infix "`o1`" := o1 (at level 50, left associativity).
   Infix "`o2`" := o2 (at level 50, left associativity).
   (** The ssreflect rewrite tactic only works for relations that have a

iris/algebra/cmra.v

 From stdpp Require Import finite.
 From iris.algebra Require Export ofe monoid.
 From iris.prelude Require Import options.
+Local Set Primitive Projections.
+
+Local Open Scope sidx_scope.
 
 Class PCore (A : Type) := pcore : A → option A.
 Global Hint Mode PCore ! : typeclass_instances.
@@ -16,16 +19,25 @@ 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 `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
+Definition included {A} `{!Equiv A, !Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
 Infix "≼" := included (at level 70) : stdpp_scope.
 Notation "(≼)" := included (only parsing) : stdpp_scope.
 Global Hint Extern 0 (_ ≼ _) => reflexivity : core.
 Global Instance: Params (@included) 3 := {}.
 
-Class ValidN (A : Type) := validN : nat → A → Prop.
-Global Hint Mode ValidN ! : typeclass_instances.
-Global Instance: Params (@validN) 3 := {}.
+(** [opM] is used in some lemma statements where [A] has not yet been shown to
+be a CMRA, so we define it directly in terms of [Op]. *)
+Definition opM `{!Op A} (x : A) (my : option A) :=
+  match my with Some y => x ⋅ y | None => x end.
+Infix "⋅?" := opM (at level 50, left associativity) : stdpp_scope.
+
+Class ValidN {SI : sidx} (A : Type) := validN : SI → A → Prop.
+Global Hint Mode ValidN - ! : typeclass_instances.
+Global Instance: Params (@validN) 4 := {}.
 Notation "✓{ n } x" := (validN n x)
   (at level 20, n at next level, format "✓{ n }  x").
 
@@ -34,15 +46,16 @@ Global Hint Mode Valid ! : typeclass_instances.
 Global Instance: Params (@valid) 2 := {}.
 Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
 
-Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
+Definition includedN {SI : sidx} `{!Dist A, Op A} (n : SI) (x y : A) :=
+  ∃ z, y ≡{n}≡ x ⋅ z.
 Notation "x ≼{ n } y" := (includedN n x y)
   (at level 70, n at next level, format "x  ≼{ n }  y") : stdpp_scope.
-Global Instance: Params (@includedN) 4 := {}.
+Global Instance: Params (@includedN) 5 := {}.
 Global Hint Extern 0 (_ ≼{_} _) => reflexivity : core.
 
 Section mixin.
-  Local Set Primitive Projections.
-  Record CmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
+  Record CmraMixin {SI : sidx} A
+      `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A} := {
     (* setoids *)
     mixin_cmra_op_ne (x : A) : NonExpansive (op x);
     mixin_cmra_pcore_ne n (x y : A) cx :
@@ -50,7 +63,7 @@ Section mixin.
     mixin_cmra_validN_ne n : Proper (dist (A := A) n ==> impl) (validN n);
     (* valid *)
     mixin_cmra_valid_validN (x : A) : ✓ x ↔ ∀ n, ✓{n} x;
-    mixin_cmra_validN_S n (x : A) : ✓{S n} x → ✓{n} x;
+    mixin_cmra_validN_le n n' (x : A) : ✓{n} x → n' ≤ n → ✓{n'} x;
     (* monoid *)
     mixin_cmra_assoc : Assoc (≡@{A}) (⋅);
     mixin_cmra_comm : Comm (≡@{A}) (⋅);
@@ -66,7 +79,9 @@ Section mixin.
 End mixin.
 
 (** Bundled version *)
-Structure cmra := Cmra' {
+#[projections(primitive=no)] (* FIXME: making this primitive leads to strange
+TC resolution failures in view.v *)
+Structure cmra {SI : sidx} := Cmra' {
   cmra_car :> Type;
   cmra_equiv : Equiv cmra_car;
   cmra_dist : Dist cmra_car;
@@ -77,7 +92,7 @@ Structure cmra := Cmra' {
   cmra_ofe_mixin : OfeMixin cmra_car;
   cmra_mixin : CmraMixin cmra_car;
 }.
-Global Arguments Cmra' _ {_ _ _ _ _ _} _ _.
+Global Arguments Cmra' {_} _ {_ _ _ _ _ _} _ _.
 (* Given [m : CmraMixin A], the notation [Cmra A m] provides a smart
 constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
 the type [A], so that it does not have to be given manually. *)
@@ -98,28 +113,42 @@ Global Hint Extern 0 (PCore _) => refine (cmra_pcore _); shelve : typeclass_inst
 Global Hint Extern 0 (Op _) => refine (cmra_op _); shelve : typeclass_instances.
 Global Hint Extern 0 (Valid _) => refine (cmra_valid _); shelve : typeclass_instances.
 Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_instances.
-Coercion cmra_ofeO (A : cmra) : ofe := Ofe A (cmra_ofe_mixin A).
+Coercion cmra_ofeO {SI : sidx} (A : cmra) : ofe := Ofe A (cmra_ofe_mixin A).
 Canonical Structure cmra_ofeO.
 
-Definition cmra_mixin_of' A {Ac : cmra} (f : Ac → A) : CmraMixin Ac := cmra_mixin Ac.
+(** 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' {SI : sidx} 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).
 
 (** Lifting properties from the mixin *)
 Section cmra_mixin.
-  Context {A : cmra}.
+  Context {SI : sidx} {A : cmra}.
   Implicit Types x y : A.
   Global Instance cmra_op_ne (x : A) : NonExpansive (op x).
   Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
   Lemma cmra_pcore_ne n x y cx :
     x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy.
   Proof. apply (mixin_cmra_pcore_ne _ (cmra_mixin A)). Qed.
-  Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
+  Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN _ A _ n).
   Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
   Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
   Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
-  Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x.
-  Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
+  Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x.
+  Proof. apply (mixin_cmra_validN_le _ (cmra_mixin A)). Qed.
   Global Instance cmra_assoc : Assoc (≡) (@op A _).
   Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed.
   Global Instance cmra_comm : Comm (≡) (@op A _).
@@ -139,44 +168,42 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
 End cmra_mixin.
 
-Definition opM {A : cmra} (x : A) (my : option A) :=
-  match my with Some y => x ⋅ y | None => x end.
-Infix "⋅?" := opM (at level 50, left associativity) : stdpp_scope.
-
 (** * CoreId elements *)
-Class CoreId {A : cmra} (x : A) := core_id : pcore x ≡ Some x.
-Global Arguments core_id {_} _ {_}.
-Global Hint Mode CoreId + ! : typeclass_instances.
-Global Instance: Params (@CoreId) 1 := {}.
+Class CoreId {SI : sidx} {A : cmra} (x : A) := core_id : pcore x ≡ Some x.
+Global Arguments core_id {_ _} _ {_}.
+Global Hint Mode CoreId - + ! : typeclass_instances.
+Global Instance: Params (@CoreId) 2 := {}.
 
 (** * Exclusive elements (i.e., elements that cannot have a frame). *)
-Class Exclusive {A : cmra} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False.
-Global Arguments exclusive0_l {_} _ {_} _ _.
-Global Hint Mode Exclusive + ! : typeclass_instances.
-Global Instance: Params (@Exclusive) 1 := {}.
+Class Exclusive {SI : sidx} {A : cmra} (x : A) :=
+  exclusive0_l y : ✓{0ᵢ} (x ⋅ y) → False.
+Global Arguments exclusive0_l {_ _} _ {_} _ _.
+Global Hint Mode Exclusive - + ! : typeclass_instances.
+Global Instance: Params (@Exclusive) 2 := {}.
 
 (** * Cancelable elements. *)
-Class Cancelable {A : cmra} (x : A) :=
-  cancelableN n y z : ✓{n}(x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.
-Global Arguments cancelableN {_} _ {_} _ _ _ _.
-Global Hint Mode Cancelable + ! : typeclass_instances.
-Global Instance: Params (@Cancelable) 1 := {}.
+Class Cancelable {SI : sidx} {A : cmra} (x : A) :=
+  cancelableN n y z : ✓{n} (x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.
+Global Arguments cancelableN {_ _} _ {_} _ _ _ _.
+Global Hint Mode Cancelable - + ! : typeclass_instances.
+Global Instance: Params (@Cancelable) 2 := {}.
 
 (** * Identity-free elements. *)
-Class IdFree {A : cmra} (x : A) :=
-  id_free0_r y : ✓{0}x → x ⋅ y ≡{0}≡ x → False.
-Global Arguments id_free0_r {_} _ {_} _ _.
-Global Hint Mode IdFree + ! : typeclass_instances.
-Global Instance: Params (@IdFree) 1 := {}.
+Class IdFree {SI : sidx} {A : cmra} (x : A) :=
+  id_free0_r y : ✓{0ᵢ} x → x ⋅ y ≡{0ᵢ}≡ x → False.
+Global Arguments id_free0_r {_ _} _ {_} _ _.
+Global Hint Mode IdFree - + ! : typeclass_instances.
+Global Instance: Params (@IdFree) 2 := {}.
 
 (** * CMRAs whose core is total *)
-Class CmraTotal (A : cmra) := cmra_total (x : A) : is_Some (pcore x).
-Global Hint Mode CmraTotal ! : typeclass_instances.
+Class CmraTotal {SI : sidx} (A : cmra) :=
+  cmra_total (x : A) : is_Some (pcore x).
+Global Hint Mode CmraTotal - ! : typeclass_instances.
 
 (** The function [core] returns a dummy when used on CMRAs without total
 core. We only ever use this for [CmraTotal] CMRAs, but it is more convenient
 to not require that proof to be able to call this function. *)
-Definition core `{PCore A} (x : A) : A := default x (pcore x).
+Definition core {A} `{!PCore A} (x : A) : A := default x (pcore x).
 Global Instance: Params (@core) 2 := {}.
 
 (** * CMRAs with a unit element *)
@@ -184,13 +211,16 @@ Class Unit (A : Type) := ε : A.
 Global Hint Mode Unit ! : typeclass_instances.
 Global Arguments ε {_ _}.
 
-Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
+Record UcmraMixin {SI : sidx} A
+    `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !Unit A} := {
   mixin_ucmra_unit_valid : ✓ (ε : A);
   mixin_ucmra_unit_left_id : LeftId (≡@{A}) ε (⋅);
   mixin_ucmra_pcore_unit : pcore ε ≡@{option A} Some ε
 }.
 
-Structure ucmra := Ucmra' {
+#[projections(primitive=no)] (* FIXME: making this primitive leads to strange
+TC resolution failures in view.v *)
+Structure ucmra {SI : sidx} := Ucmra' {
   ucmra_car :> Type;
   ucmra_equiv : Equiv ucmra_car;
   ucmra_dist : Dist ucmra_car;
@@ -203,7 +233,7 @@ Structure ucmra := Ucmra' {
   ucmra_cmra_mixin : CmraMixin ucmra_car;
   ucmra_mixin : UcmraMixin ucmra_car;
 }.
-Global Arguments Ucmra' _ {_ _ _ _ _ _ _} _ _ _.
+Global Arguments Ucmra' {_} _ {_ _ _ _ _ _ _} _ _ _.
 Notation Ucmra A m :=
   (Ucmra' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
 Global Arguments ucmra_car : simpl never.
@@ -219,15 +249,24 @@ Global Arguments ucmra_mixin : simpl never.
 Add Printing Constructor ucmra.
 (* FIXME(Coq #6294) : we need the new unification algorithm here. *)
 Global Hint Extern 0 (Unit _) => refine (ucmra_unit _); shelve : typeclass_instances.
-Coercion ucmra_ofeO (A : ucmra) : ofe := Ofe A (ucmra_ofe_mixin A).
+Coercion ucmra_ofeO {SI : sidx} (A : ucmra) : ofe := Ofe A (ucmra_ofe_mixin A).
 Canonical Structure ucmra_ofeO.
-Coercion ucmra_cmraR (A : ucmra) : cmra :=
+Coercion ucmra_cmraR {SI : sidx} (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}.
+  Context {SI : sidx} {A : ucmra}.
   Implicit Types x y : A.
   Lemma ucmra_unit_valid : ✓ (ε : A).
   Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
@@ -238,27 +277,29 @@ Section ucmra_mixin.
 End ucmra_mixin.
 
 (** * Discrete CMRAs *)
-Class CmraDiscrete (A : cmra) := {
-  cmra_discrete_ofe_discrete :> OfeDiscrete A;
-  cmra_discrete_valid (x : A) : ✓{0} x → ✓ x
+#[projections(primitive=no)] (* FIXME: making this primitive means we cannot use
+the projections with eauto any more (see https://github.com/coq/coq/issues/17561) *)
+Class CmraDiscrete {SI : sidx} (A : cmra) := {
+  #[global] cmra_discrete_ofe_discrete :: OfeDiscrete A;
+  cmra_discrete_valid (x : A) : ✓{0ᵢ} x → ✓ x
 }.
-Global Hint Mode CmraDiscrete ! : typeclass_instances.
+Global Hint Mode CmraDiscrete - ! : typeclass_instances.
 
 (** * Morphisms *)
-Class CmraMorphism {A B : cmra} (f : A → B) := {
-  cmra_morphism_ne :> NonExpansive f;
+Class CmraMorphism {SI : sidx} {A B : cmra} (f : A → B) := {
+  #[global] cmra_morphism_ne :: NonExpansive f;
   cmra_morphism_validN n x : ✓{n} x → ✓{n} f x;
   cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
   cmra_morphism_op x y : f (x ⋅ y) ≡ f x ⋅ f y
 }.
-Global Hint Mode CmraMorphism - - ! : typeclass_instances.
-Global Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
-Global Arguments cmra_morphism_pcore {_ _} _ {_} _.
-Global Arguments cmra_morphism_op {_ _} _ {_} _ _.
+Global Hint Mode CmraMorphism - - - ! : typeclass_instances.
+Global Arguments cmra_morphism_validN {_ _ _} _ {_} _ _ _.
+Global Arguments cmra_morphism_pcore {_ _ _} _ {_} _.
+Global Arguments cmra_morphism_op {_ _ _} _ {_} _ _.
 
 (** * Properties **)
 Section cmra.
-Context {A : cmra}.
+Context {SI : sidx} {A : cmra}.
 Implicit Types x y z : A.
 Implicit Types xs ys zs : list A.
 
@@ -273,7 +314,7 @@ Qed.
 Lemma cmra_pcore_proper x y cx :
   x ≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡ cy.
 Proof.
-  intros. destruct (cmra_pcore_ne 0 x y cx) as (cy&?&?); auto.
+  intros. destruct (cmra_pcore_ne 0ᵢ x y cx) as (cy&?&?); auto.
   exists cy; split; [done|apply equiv_dist=> n].
   destruct (cmra_pcore_ne n x y cx) as (cy'&?&?); naive_solver.
 Qed.
@@ -283,9 +324,9 @@ Global Instance cmra_op_ne' : NonExpansive2 (@op A _).
 Proof. intros n x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
 Global Instance cmra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
 Proof. apply (ne_proper_2 _). Qed.
-Global Instance cmra_validN_ne' n : Proper (dist n ==> iff) (@validN A _ n) | 1.
+Global Instance cmra_validN_ne' n : Proper (dist n ==> iff) (@validN SI A _ n) | 1.
 Proof. by split; apply cmra_validN_ne. Qed.
-Global Instance cmra_validN_proper n : Proper ((≡) ==> iff) (@validN A _ n) | 1.
+Global Instance cmra_validN_proper n : Proper ((≡) ==> iff) (@validN SI A _ n) | 1.
 Proof. by intros x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
 
 Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (@valid A _).
@@ -294,13 +335,13 @@ Proof.
   by split=> ? n; [rewrite -Hxy|rewrite Hxy].
 Qed.
 Global Instance cmra_includedN_ne n :
-  Proper (dist n ==> dist n ==> iff) (@includedN A _ _ n) | 1.
+  Proper (dist n ==> dist n ==> iff) (@includedN SI A _ _ n) | 1.
 Proof.
   intros x x' Hx y y' Hy.
   by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
 Qed.
 Global Instance cmra_includedN_proper n :
-  Proper ((≡) ==> (≡) ==> iff) (@includedN A _ _ n) | 1.
+  Proper ((≡) ==> (≡) ==> iff) (@includedN SI A _ _ n) | 1.
 Proof.
   intros x x' Hx y y' Hy; revert Hx Hy; rewrite !equiv_dist=> Hx Hy.
   by rewrite (Hx n) (Hy n).
@@ -311,18 +352,18 @@ Proof.
   intros x x' Hx y y' Hy.
   by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
 Qed.
-Global Instance cmra_opM_ne : NonExpansive2 (@opM A).
+Global Instance cmra_opM_ne : NonExpansive2 (@opM A _).
 Proof. destruct 2; by ofe_subst. Qed.
-Global Instance cmra_opM_proper : Proper ((≡) ==> (≡) ==> (≡)) (@opM A).
+Global Instance cmra_opM_proper : Proper ((≡) ==> (≡) ==> (≡)) (@opM A _).
 Proof. destruct 2; by setoid_subst. Qed.
 
-Global Instance CoreId_proper : Proper ((≡) ==> iff) (@CoreId A).
+Global Instance CoreId_proper : Proper ((≡) ==> iff) (@CoreId SI A).
 Proof. solve_proper. Qed.
-Global Instance Exclusive_proper : Proper ((≡) ==> iff) (@Exclusive A).
+Global Instance Exclusive_proper : Proper ((≡) ==> iff) (@Exclusive SI A).
 Proof. intros x y Hxy. rewrite /Exclusive. by setoid_rewrite Hxy. Qed.
-Global Instance Cancelable_proper : Proper ((≡) ==> iff) (@Cancelable A).
+Global Instance Cancelable_proper : Proper ((≡) ==> iff) (@Cancelable SI A).
 Proof. intros x y Hxy. rewrite /Cancelable. by setoid_rewrite Hxy. Qed.
-Global Instance IdFree_proper : Proper ((≡) ==> iff) (@IdFree A).
+Global Instance IdFree_proper : Proper ((≡) ==> iff) (@IdFree SI A).
 Proof. intros x y Hxy. rewrite /IdFree. by setoid_rewrite Hxy. Qed.
 
 (** ** Op *)
@@ -330,8 +371,8 @@ Lemma cmra_op_opM_assoc x y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz).
 Proof. destruct mz; by rewrite /= -?assoc. Qed.
 
 (** ** Validity *)
-Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x.
-Proof. induction 2; eauto using cmra_validN_S. Qed.
+Lemma cmra_validN_lt n n' x : ✓{n} x → n' < n → ✓{n'} x.
+Proof. eauto using cmra_validN_le, SIdx.lt_le_incl. Qed.
 Lemma cmra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x.
 Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed.
 Lemma cmra_validN_op_r n x y : ✓{n} (x ⋅ y) → ✓{n} y.
@@ -363,11 +404,11 @@ Qed.
 
 (** ** Exclusive elements *)
 Lemma exclusiveN_l n x `{!Exclusive x} y : ✓{n} (x ⋅ y) → False.
-Proof. intros. eapply (exclusive0_l x y), cmra_validN_le; eauto with lia. Qed.
+Proof. intros. by eapply (exclusive0_l x y), cmra_validN_le, SIdx.le_0_l. Qed.
 Lemma exclusiveN_r n x `{!Exclusive x} y : ✓{n} (y ⋅ x) → False.
 Proof. rewrite comm. by apply exclusiveN_l. Qed.
 Lemma exclusive_l x `{!Exclusive x} y : ✓ (x ⋅ y) → False.
-Proof. by move /cmra_valid_validN /(_ 0) /exclusive0_l. Qed.
+Proof. by move /cmra_valid_validN /(_ 0ᵢ) /exclusive0_l. Qed.
 Lemma exclusive_r x `{!Exclusive x} y : ✓ (y ⋅ x) → False.
 Proof. rewrite comm. by apply exclusive_l. Qed.
 Lemma exclusiveN_opM n x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None.
@@ -380,7 +421,7 @@ Proof. intros [? ->]. by apply exclusive_l. Qed.
 (** ** Order *)
 Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.
 Proof. intros [z ->]. by exists z. Qed.
-Global Instance cmra_includedN_trans n : Transitive (@includedN A _ _ n).
+Global Instance cmra_includedN_trans n : Transitive (@includedN SI A _ _ n).
 Proof.
   intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). by rewrite assoc -Hy -Hz.
 Qed.
@@ -395,10 +436,10 @@ Proof. intros Hyv [z ?]; ofe_subst y; eauto using cmra_validN_op_l. Qed.
 Lemma cmra_validN_included n x y : ✓{n} y → x ≼ y → ✓{n} x.
 Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
 
-Lemma cmra_includedN_S n x y : x ≼{S n} y → x ≼{n} y.
-Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
-Lemma cmra_includedN_le n n' x y : x ≼{n} y → n' ≤ n → x ≼{n'} y.
-Proof. induction 2; auto using cmra_includedN_S. Qed.
+Lemma cmra_includedN_le n m x y : x ≼{n} y → m ≤ n → x ≼{m} y.
+Proof. by intros [z Hz] H; exists z; eapply dist_le. Qed.
+Lemma cmra_includedN_S n x y : x ≼{Sᵢ n} y → x ≼{n} y.
+Proof. intros ?. by eapply cmra_includedN_le, SIdx.le_succ_diag_r. Qed.
 
 Lemma cmra_includedN_l n x y : x ≼{n} x ⋅ y.
 Proof. by exists y. Qed.
@@ -473,7 +514,7 @@ Qed.
 (** ** Total core *)
 Section total_core.
   Local Set Default Proof Using "Type*".
-  Context `{CmraTotal A}.
+  Context `{!CmraTotal A}.
 
   Lemma cmra_pcore_core x : pcore x = Some (core x).
   Proof.
@@ -520,15 +561,16 @@ Section total_core.
   Lemma core_id_core x `{!CoreId x} : core x ≡ x.
   Proof. by apply core_id_total. Qed.
 
+  (** Not an instance since TC search cannot solve the premise. *)
+  Lemma cmra_pcore_core_id x y : pcore x = Some y → CoreId y.
+  Proof. rewrite /CoreId. eauto using cmra_pcore_idemp. Qed.
+
   Global Instance cmra_core_core_id x : CoreId (core x).
-  Proof.
-    destruct (cmra_total x) as [cx Hcx].
-    rewrite /CoreId /core /= Hcx /=. eauto using cmra_pcore_idemp.
-  Qed.
+  Proof. eapply cmra_pcore_core_id. rewrite cmra_pcore_core. done. Qed.
 
   Lemma cmra_included_core x : core x ≼ x.
   Proof. by exists x; rewrite cmra_core_l. Qed.
-  Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
+  Global Instance cmra_includedN_preorder n : PreOrder (@includedN SI A _ _ n).
   Proof.
     split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
   Qed.
@@ -544,45 +586,45 @@ Section total_core.
 End total_core.
 
 (** ** Discrete *)
-Lemma cmra_discrete_included_l x y : Discrete x → ✓{0} y → x ≼{0} y → x ≼ y.
+Lemma cmra_discrete_included_l x y : Discrete x → ✓{0ᵢ} y → x ≼{0ᵢ} y → x ≼ y.
 Proof.
   intros ?? [x' ?].
-  destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
-  by exists z'; rewrite Hy (discrete x z).
-Qed.
-Lemma cmra_discrete_included_r x y : Discrete y → x ≼{0} y → x ≼ y.
-Proof. intros ? [x' ?]. exists x'. by apply (discrete y). Qed.
+  destruct (cmra_extend 0ᵢ y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
+  by exists z'; rewrite Hy (discrete_0 x z).
+Qed. 
+Lemma cmra_discrete_included_r x y : Discrete y → x ≼{0ᵢ} y → x ≼ y.
+Proof. intros ? [x' ?]. exists x'. by apply (discrete_0 y). Qed.
 Lemma cmra_op_discrete x1 x2 :
-  ✓{0} (x1 ⋅ x2) → Discrete x1 → Discrete x2 → Discrete (x1 ⋅ x2).
+  ✓{0ᵢ} (x1 ⋅ x2) → Discrete x1 → Discrete x2 → Discrete (x1 ⋅ x2).
 Proof.
   intros ??? z Hz.
-  destruct (cmra_extend 0 z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
+  destruct (cmra_extend 0ᵢ z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
   { rewrite -?Hz. done. }
-  by rewrite Hz' (discrete x1 y1) // (discrete x2 y2).
+  by rewrite Hz' (discrete_0 x1 y1) // (discrete_0 x2 y2).
 Qed.
 
 (** ** Discrete *)
-Lemma cmra_discrete_valid_iff `{CmraDiscrete A} n x : ✓ x ↔ ✓{n} x.
+Lemma cmra_discrete_valid_iff `{!CmraDiscrete A} n x : ✓ x ↔ ✓{n} x.
 Proof.
   split; first by rewrite cmra_valid_validN.
-  eauto using cmra_discrete_valid, cmra_validN_le with lia.
+  eauto using cmra_discrete_valid, cmra_validN_le, SIdx.le_0_l.
 Qed.
-Lemma cmra_discrete_valid_iff_0 `{CmraDiscrete A} n x : ✓{0} x ↔ ✓{n} x.
+Lemma cmra_discrete_valid_iff_0 `{!CmraDiscrete A} n x : ✓{0ᵢ} x ↔ ✓{n} x.
 Proof. by rewrite -!cmra_discrete_valid_iff. Qed.
-Lemma cmra_discrete_included_iff `{OfeDiscrete A} n x y : x ≼ y ↔ x ≼{n} y.
+Lemma cmra_discrete_included_iff `{!OfeDiscrete A} n x y : x ≼ y ↔ x ≼{n} y.
 Proof.
   split; first by apply cmra_included_includedN.
   intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
 Qed.
-Lemma cmra_discrete_included_iff_0 `{OfeDiscrete A} n x y : x ≼{0} y ↔ x ≼{n} y.
+Lemma cmra_discrete_included_iff_0 `{!OfeDiscrete A} n x y : x ≼{0ᵢ} y ↔ x ≼{n} y.
 Proof. by rewrite -!cmra_discrete_included_iff. Qed.
 
 (** Cancelable elements  *)
-Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
+Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable SI A).
 Proof. unfold Cancelable. intros x x' EQ. by setoid_rewrite EQ. Qed.
 Lemma cancelable x `{!Cancelable x} y z : ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z.
 Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
-Lemma discrete_cancelable x `{CmraDiscrete A}:
+Lemma discrete_cancelable x `{!CmraDiscrete A}:
   (∀ y z, ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z) → Cancelable x.
 Proof. intros ????. rewrite -!discrete_iff -cmra_discrete_valid_iff. auto. Qed.
 Global Instance cancelable_op x y :
@@ -597,25 +639,25 @@ Global Instance exclusive_cancelable (x : A) : Exclusive x → Cancelable x.
 Proof. intros ? n z z' []%(exclusiveN_l _ x). Qed.
 
 (** Id-free elements  *)
-Global Instance id_free_ne n : Proper (dist n ==> iff) (@IdFree A).
+Global Instance id_free_ne n : Proper (dist n ==> iff) (@IdFree SI A).
 Proof.
-  intros x x' EQ%(dist_le _ 0); last lia. rewrite /IdFree.
+  intros x x' EQ%(dist_le _ 0ᵢ); [|apply SIdx.le_0_l]. rewrite /IdFree.
   split=> y ?; (rewrite -EQ || rewrite EQ); eauto.
 Qed.
-Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree A).
-Proof. by move=> P Q /equiv_dist /(_ 0)=> ->. Qed.
+Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree SI A).
+Proof. by move=> P Q /equiv_dist /(_ 0ᵢ)=> ->. Qed.
 Lemma id_freeN_r n n' x `{!IdFree x} y : ✓{n}x → x ⋅ y ≡{n'}≡ x → False.
-Proof. eauto using cmra_validN_le, dist_le with lia. Qed.
+Proof. eauto using cmra_validN_le, dist_le, SIdx.le_0_l. Qed.
 Lemma id_freeN_l n n' x `{!IdFree x} y : ✓{n}x → y ⋅ x ≡{n'}≡ x → False.
 Proof. rewrite comm. eauto using id_freeN_r. Qed.
 Lemma id_free_r x `{!IdFree x} y : ✓x → x ⋅ y ≡ x → False.
 Proof. move=> /cmra_valid_validN ? /equiv_dist. eauto. Qed.
 Lemma id_free_l x `{!IdFree x} y : ✓x → y ⋅ x ≡ x → False.
 Proof. rewrite comm. eauto using id_free_r. Qed.
-Lemma discrete_id_free x `{CmraDiscrete A}:
+Lemma discrete_id_free x `{!CmraDiscrete A}:
   (∀ y, ✓ x → x ⋅ y ≡ x → False) → IdFree x.
 Proof.
-  intros Hx y ??. apply (Hx y), (discrete _); eauto using cmra_discrete_valid.
+  intros Hx y ??. apply (Hx y), (discrete_0 _); eauto using cmra_discrete_valid.
 Qed.
 Global Instance id_free_op_r x y : IdFree y → Cancelable x → IdFree (x ⋅ y).
 Proof.
@@ -625,12 +667,18 @@ Qed.
 Global Instance id_free_op_l x y : IdFree x → Cancelable y → IdFree (x ⋅ y).
 Proof. intros. rewrite comm. apply _. Qed.
 Global Instance exclusive_id_free x : Exclusive x → IdFree x.
-Proof. intros ? z ? Hid. apply (exclusiveN_l 0 x z). by rewrite Hid. Qed.
+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}.
+  Context {SI : sidx} {A : ucmra}.
   Implicit Types x y z : A.
 
   Lemma ucmra_unit_validN n : ✓{n} (ε:A).
@@ -658,11 +706,12 @@ 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.
   Local Set Default Proof Using "Type*".
-  Context {A : cmra} `{!LeibnizEquiv A}.
+  Context {SI : sidx} {A : cmra} `{!LeibnizEquiv A}.
   Implicit Types x y : A.
 
   Global Instance cmra_assoc_L : Assoc (=) (@op A _).
@@ -690,7 +739,7 @@ Section cmra_leibniz.
 
   (** ** Total core *)
   Section total_core.
-    Context `{CmraTotal A}.
+    Context `{!CmraTotal A}.
 
     Lemma cmra_core_r_L x : x ⋅ core x = x.
     Proof. unfold_leibniz. apply cmra_core_r. Qed.
@@ -709,7 +758,7 @@ End cmra_leibniz.
 
 Section ucmra_leibniz.
   Local Set Default Proof Using "Type*".
-  Context {A : ucmra} `{!LeibnizEquiv A}.
+  Context {SI : sidx} {A : ucmra} `{!LeibnizEquiv A}.
   Implicit Types x y z : A.
 
   Global Instance ucmra_unit_left_id_L : LeftId (=) ε (@op A _).
@@ -720,13 +769,13 @@ End ucmra_leibniz.
 
 (** * Constructing a CMRA with total core *)
 Section cmra_total.
-  Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
+  Context {SI : sidx} A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A}.
   Context (total : ∀ x : A, is_Some (pcore x)).
   Context (op_ne : ∀ x : A, NonExpansive (op x)).
   Context (core_ne : NonExpansive (@core A _)).
-  Context (validN_ne : ∀ n, Proper (dist n ==> impl) (@validN A _ n)).
+  Context (validN_ne : ∀ n, Proper (dist n ==> impl) (@validN SI A _ n)).
   Context (valid_validN : ∀ (x : A), ✓ x ↔ ∀ n, ✓{n} x).
-  Context (validN_S : ∀ n (x : A), ✓{S n} x → ✓{n} x).
+  Context (validN_le : ∀ n n' (x : A), ✓{n} x → n' ≤ n → ✓{n'} x).
   Context (op_assoc : Assoc (≡) (@op A _)).
   Context (op_comm : Comm (≡) (@op A _)).
   Context (core_l : ∀ x : A, core x ⋅ x ≡ x).
@@ -750,7 +799,7 @@ Section cmra_total.
 End cmra_total.
 
 (** * Properties about morphisms *)
-Global Instance cmra_morphism_id {A : cmra} : CmraMorphism (@id A).
+Global Instance cmra_morphism_id {SI : sidx} {A : cmra} : CmraMorphism (@id A).
 Proof.
   split => /=.
   - apply _.
@@ -758,9 +807,11 @@ Proof.
   - intros. by rewrite option_fmap_id.
   - done.
 Qed.
-Global Instance cmra_morphism_proper {A B : cmra} (f : A → B) `{!CmraMorphism f} :
+Global Instance cmra_morphism_proper {SI : sidx}
+    {A B : cmra} (f : A → B) `{!CmraMorphism f} :
   Proper ((≡) ==> (≡)) f := ne_proper _.
-Global Instance cmra_morphism_compose {A B C : cmra} (f : A → B) (g : B → C) :
+Global Instance cmra_morphism_compose {SI : sidx}
+    {A B C : cmra} (f : A → B) (g : B → C) :
   CmraMorphism f → CmraMorphism g → CmraMorphism (g ∘ f).
 Proof.
   split.
@@ -772,7 +823,7 @@ Qed.
 
 Section cmra_morphism.
   Local Set Default Proof Using "Type*".
-  Context {A B : cmra} (f : A → B) `{!CmraMorphism f}.
+  Context {SI : sidx} {A B : cmra} (f : A → B) `{!CmraMorphism f}.
   Lemma cmra_morphism_core x : f (core x) ≡ core (f x).
   Proof. unfold core. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
   Lemma cmra_morphism_monotone x y : x ≼ y → f x ≼ f y.
@@ -784,7 +835,7 @@ Section cmra_morphism.
 End cmra_morphism.
 
 (** COFE → CMRA Functors *)
-Record rFunctor := RFunctor {
+Record rFunctor {SI : sidx} := RFunctor {
   rFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, cmra;
   rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
@@ -800,83 +851,86 @@ Record rFunctor := RFunctor {
     CmraMorphism (rFunctor_map fg)
 }.
 Global Existing Instances rFunctor_map_ne rFunctor_mor.
-Global Instance: Params (@rFunctor_map) 9 := {}.
+Global Instance: Params (@rFunctor_map) 10 := {}.
 
 Declare Scope rFunctor_scope.
 Delimit Scope rFunctor_scope with RF.
 Bind Scope rFunctor_scope with rFunctor.
 
-Class rFunctorContractive (F : rFunctor) :=
-  rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
-    Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
-Global Hint Mode rFunctorContractive ! : typeclass_instances.
+Class rFunctorContractive {SI : sidx} (F : rFunctor) :=
+  #[global] rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} ::
+    Contractive (@rFunctor_map SI F A1 _ A2 _ B1 _ B2 _).
+Global Hint Mode rFunctorContractive - ! : typeclass_instances.
 
-Definition rFunctor_apply (F: rFunctor) (A: ofe) `{!Cofe A} : cmra :=
+Definition rFunctor_apply {SI : sidx} (F: rFunctor) (A: ofe) `{!Cofe A} : cmra :=
   rFunctor_car F A A.
 
-Program Definition rFunctor_to_oFunctor (F: rFunctor) : oFunctor := {|
+Program Definition rFunctor_to_oFunctor {SI : sidx} (F: rFunctor) : oFunctor := {|
   oFunctor_car A _ B _ := rFunctor_car F A B;
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := rFunctor_map F fg
 |}.
 Next Obligation.
-  intros F A ? B ? x. simpl in *. apply rFunctor_map_id.
+  intros ? F A ? B ? x. simpl in *. apply rFunctor_map_id.
 Qed.
 Next Obligation.
-  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
+  intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
   apply rFunctor_map_compose.
 Qed.
 
-Global Instance rFunctor_to_oFunctor_contractive F :
+Global Instance rFunctor_to_oFunctor_contractive {SI : sidx} F :
   rFunctorContractive F → oFunctorContractive (rFunctor_to_oFunctor F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg. apply rFunctor_map_contractive. done.
 Qed.
 
-Program Definition rFunctor_oFunctor_compose (F1 : rFunctor) (F2 : oFunctor)
-  `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : rFunctor := {|
+Program Definition rFunctor_oFunctor_compose
+    {SI : sidx} (F1 : rFunctor) (F2 : oFunctor)
+    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} : rFunctor := {|
   rFunctor_car A _ B _ := rFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
   rFunctor_map A1 _ A2 _ B1 _ B2 _ 'fg :=
     rFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
+  intros ? F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
   apply rFunctor_map_ne; split; apply oFunctor_map_ne; by split.
 Qed.
 Next Obligation.
-  intros F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(rFunctor_map_id F1 x).
+  intros ? F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(rFunctor_map_id F1 x).
   apply equiv_dist=> n. apply rFunctor_map_ne.
   split=> y /=; by rewrite !oFunctor_map_id.
 Qed.
 Next Obligation.
-  intros F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
+  intros ? F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
   rewrite -rFunctor_map_compose. apply equiv_dist=> n. apply rFunctor_map_ne.
   split=> y /=; by rewrite !oFunctor_map_compose.
 Qed.
-Global Instance rFunctor_oFunctor_compose_contractive_1 (F1 : rFunctor) (F2 : oFunctor)
-    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+Global Instance rFunctor_oFunctor_compose_contractive_1
+    {SI : sidx} (F1 : rFunctor) (F2 : oFunctor)
+    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
   rFunctorContractive F1 → rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
   f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
 Qed.
-Global Instance rFunctor_oFunctor_compose_contractive_2 (F1 : rFunctor) (F2 : oFunctor)
-    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+Global Instance rFunctor_oFunctor_compose_contractive_2 
+    {SI : sidx} (F1 : rFunctor) (F2 : oFunctor)
+    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
   oFunctorContractive F2 → rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
   f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
 Qed.
 
-Program Definition constRF (B : cmra) : rFunctor :=
+Program Definition constRF {SI : sidx} (B : cmra) : rFunctor :=
   {| rFunctor_car A1 _ A2 _ := B; rFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
 Coercion constRF : cmra >-> rFunctor.
 
-Global Instance constRF_contractive B : rFunctorContractive (constRF B).
+Global Instance constRF_contractive {SI : sidx} B : rFunctorContractive (constRF B).
 Proof. rewrite /rFunctorContractive; apply _. Qed.
 
 (** COFE → UCMRA Functors *)
-Record urFunctor := URFunctor {
+Record urFunctor {SI : sidx} := URFunctor {
   urFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ucmra;
   urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
@@ -892,91 +946,95 @@ Record urFunctor := URFunctor {
     CmraMorphism (urFunctor_map fg)
 }.
 Global Existing Instances urFunctor_map_ne urFunctor_mor.
-Global Instance: Params (@urFunctor_map) 9 := {}.
+Global Instance: Params (@urFunctor_map) 10 := {}.
 
 Declare Scope urFunctor_scope.
 Delimit Scope urFunctor_scope with URF.
 Bind Scope urFunctor_scope with urFunctor.
 
-Class urFunctorContractive (F : urFunctor) :=
-  urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
-    Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
-Global Hint Mode urFunctorContractive ! : typeclass_instances.
+Class urFunctorContractive {SI : sidx} (F : urFunctor) :=
+  #[global] urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} ::
+    Contractive (@urFunctor_map SI F A1 _ A2 _ B1 _ B2 _).
+Global Hint Mode urFunctorContractive - ! : typeclass_instances.
 
-Definition urFunctor_apply (F: urFunctor) (A: ofe) `{!Cofe A} : ucmra :=
+Definition urFunctor_apply {SI : sidx} (F: urFunctor) (A: ofe) `{!Cofe A} : ucmra :=
   urFunctor_car F A A.
 
-Program Definition urFunctor_to_rFunctor (F: urFunctor) : rFunctor := {|
+Program Definition urFunctor_to_rFunctor {SI : sidx} (F: urFunctor) : rFunctor := {|
   rFunctor_car A _ B _ := urFunctor_car F A B;
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := urFunctor_map F fg
 |}.
 Next Obligation.
-  intros F A ? B ? x. simpl in *. apply urFunctor_map_id.
+  intros ? F A ? B ? x. simpl in *. apply urFunctor_map_id.
 Qed.
 Next Obligation.
-  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
+  intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. simpl in *.
   apply urFunctor_map_compose.
 Qed.
 
-Global Instance urFunctor_to_rFunctor_contractive F :
+Global Instance urFunctor_to_rFunctor_contractive {SI : sidx} F :
   urFunctorContractive F → rFunctorContractive (urFunctor_to_rFunctor F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg. apply urFunctor_map_contractive. done.
 Qed.
 
-Program Definition urFunctor_oFunctor_compose (F1 : urFunctor) (F2 : oFunctor)
-  `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} : urFunctor := {|
+Program Definition urFunctor_oFunctor_compose
+    {SI : sidx} (F1 : urFunctor) (F2 : oFunctor)
+    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} : urFunctor := {|
   urFunctor_car A _ B _ := urFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
   urFunctor_map A1 _ A2 _ B1 _ B2 _ 'fg :=
     urFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
+  intros ? F1 F2 ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] [??]; simpl in *.
   apply urFunctor_map_ne; split; apply oFunctor_map_ne; by split.
 Qed.
 Next Obligation.
-  intros F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(urFunctor_map_id F1 x).
+  intros ? F1 F2 ? A ? B ? x; simpl in *. rewrite -{2}(urFunctor_map_id F1 x).
   apply equiv_dist=> n. apply urFunctor_map_ne.
   split=> y /=; by rewrite !oFunctor_map_id.
 Qed.
 Next Obligation.
-  intros F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
+  intros ? F1 F2 ? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
   rewrite -urFunctor_map_compose. apply equiv_dist=> n. apply urFunctor_map_ne.
   split=> y /=; by rewrite !oFunctor_map_compose.
 Qed.
-Global Instance urFunctor_oFunctor_compose_contractive_1 (F1 : urFunctor) (F2 : oFunctor)
-    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+Global Instance urFunctor_oFunctor_compose_contractive_1
+    {SI : sidx} (F1 : urFunctor) (F2 : oFunctor)
+    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
   urFunctorContractive F1 → urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
   f_contractive; destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
 Qed.
-Global Instance urFunctor_oFunctor_compose_contractive_2 (F1 : urFunctor) (F2 : oFunctor)
-    `{!∀ `{Cofe A, Cofe B}, Cofe (oFunctor_car F2 A B)} :
+Global Instance urFunctor_oFunctor_compose_contractive_2
+    {SI : sidx} (F1 : urFunctor) (F2 : oFunctor)
+    `{!∀ `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F2 A B)} :
   oFunctorContractive F2 → urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n [f1 g1] [f2 g2] Hfg; simpl in *.
   f_equiv; split; simpl in *; f_contractive; destruct Hfg; by split.
 Qed.
 
-Program Definition constURF (B : ucmra) : urFunctor :=
+Program Definition constURF {SI : sidx} (B : ucmra) : urFunctor :=
   {| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
 Coercion constURF : ucmra >-> urFunctor.
 
-Global Instance constURF_contractive B : urFunctorContractive (constURF B).
+Global Instance constURF_contractive {SI : sidx} B :
+  urFunctorContractive (constURF B).
 Proof. rewrite /urFunctorContractive; apply _. Qed.
 
 (** * Transporting a CMRA equality *)
-Definition cmra_transport {A B : cmra} (H : A = B) (x : A) : B :=
+Definition cmra_transport {SI : sidx} {A B : cmra} (H : A = B) (x : A) : B :=
   eq_rect A id x _ H.
 
-Lemma cmra_transport_trans {A B C : cmra} (H1 : A = B) (H2 : B = C) x :
+Lemma cmra_transport_trans {SI : sidx} {A B C : cmra} (H1 : A = B) (H2 : B = C) x :
   cmra_transport H2 (cmra_transport H1 x) = cmra_transport (eq_trans H1 H2) x.
 Proof. by destruct H2. Qed.
 
 Section cmra_transport.
-  Context {A B : cmra} (H : A = B).
+  Context {SI : sidx} {A B : cmra} (H : A = B).
   Notation T := (cmra_transport H).
   Global Instance cmra_transport_ne : NonExpansive T.
   Proof. by intros ???; destruct H. Qed.
@@ -1016,7 +1074,8 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
 
 Section discrete.
   Local Set Default Proof Using "Type*".
-  Context `{Equiv A, PCore A, Op A, Valid A} (Heq : @Equivalence A (≡)).
+  Context {SI : sidx} `{!Equiv A, !PCore A, !Op A, !Valid A}.
+  Context (Heq : @Equivalence A (≡)).
   Context (ra_mix : RAMixin A).
   Existing Instances discrete_dist.
 
@@ -1024,7 +1083,7 @@ Section discrete.
   Definition discrete_cmra_mixin : CmraMixin A.
   Proof.
     destruct ra_mix; split; try done.
-    - intros x; split; first done. by move=> /(_ 0).
+    - intros x; split; first done. by move=> /(_ 0ᵢ).
     - intros n x y1 y2 ??; by exists y1, y2.
   Qed.
 
@@ -1068,6 +1127,7 @@ End ra_total.
 
 (** ** CMRA for the unit type *)
 Section unit.
+  Context {SI : sidx}.
   Local Instance unit_valid_instance : Valid () := λ x, True.
   Local Instance unit_validN_instance : ValidN () := λ n x, True.
   Local Instance unit_pcore_instance : PCore () := λ x, Some x.
@@ -1091,6 +1151,7 @@ End unit.
 
 (** ** CMRA for the empty type *)
 Section empty.
+  Context {SI : sidx}.
   Local Instance Empty_set_valid_instance : Valid Empty_set := λ x, False.
   Local Instance Empty_set_validN_instance : ValidN Empty_set := λ n x, False.
   Local Instance Empty_set_pcore_instance : PCore Empty_set := λ x, Some x.
@@ -1109,7 +1170,7 @@ End empty.
 
 (** ** Product *)
 Section prod.
-  Context {A B : cmra}.
+  Context {SI : sidx} {A B : cmra}.
   Local Arguments pcore _ _ !_ /.
   Local Arguments cmra_pcore _ !_/.
 
@@ -1155,7 +1216,7 @@ Section prod.
     - intros x; split.
       + intros [??] n; split; by apply cmra_valid_validN.
       + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
-    - by intros n x [??]; split; apply cmra_validN_S.
+    - intros n m x [??]; split; by eapply cmra_validN_le.
     - by split; rewrite /= assoc.
     - by split; rewrite /= comm.
     - intros x y [??]%prod_pcore_Some;
@@ -1222,19 +1283,19 @@ Section prod.
   Proof. intros ???[][][][]. constructor; simpl in *; by eapply cancelableN. Qed.
 
   Global Instance pair_id_free_l x y : IdFree x → IdFree (x,y).
-  Proof. move=>? [??] [? _] [/=? _]. eauto. Qed.
+  Proof. move=> Hx [a b] [? _] [/=? _]. apply (Hx a); eauto. Qed.
   Global Instance pair_id_free_r x y : IdFree y → IdFree (x,y).
-  Proof. move=>? [??] [_ ?] [_ /=?]. eauto. Qed.
+  Proof. move=> Hy [a b] [_ ?] [_ /=?]. apply (Hy b); eauto. Qed.
 End prod.
 
 (* Registering as [Hint Extern] with new unification. *)
 Global Hint Extern 4 (CoreId _) =>
   notypeclasses refine (pair_core_id _ _ _ _) : typeclass_instances.
 
-Global Arguments prodR : clear implicits.
+Global Arguments prodR {_} _ _.
 
 Section prod_unit.
-  Context {A B : ucmra}.
+  Context {SI : sidx} {A B : ucmra}.
 
   Local Instance prod_unit_instance `{Unit A, Unit B} : Unit (A * B) := (ε, ε).
   Lemma prod_ucmra_mixin : UcmraMixin (A * B).
@@ -1268,39 +1329,40 @@ Section prod_unit.
   Proof. unfold_leibniz. apply pair_op_2. Qed.
 End prod_unit.
 
-Global Arguments prodUR : clear implicits.
+Global Arguments prodUR {_} _ _.
 
-Global Instance prod_map_cmra_morphism {A A' B B' : cmra} (f : A → A') (g : B → B') :
+Global Instance prod_map_cmra_morphism
+    {SI : sidx} {A A' B B' : cmra} (f : A → A') (g : B → B') :
   CmraMorphism f → CmraMorphism g → CmraMorphism (prod_map f g).
 Proof.
   split; first apply _.
   - by intros n x [??]; split; simpl; apply cmra_morphism_validN.
-  - intros x. etrans; last apply (reflexivity (mbind _ _)).
-    etrans; first apply (reflexivity (_ <$> mbind _ _)). simpl.
-    assert (Hf := cmra_morphism_pcore f (x.1)).
-    destruct (pcore (f (x.1))), (pcore (x.1)); inversion_clear Hf=>//=.
-    assert (Hg := cmra_morphism_pcore g (x.2)).
-    destruct (pcore (g (x.2))), (pcore (x.2)); inversion_clear Hg=>//=.
+  - intros [x1 x2]. rewrite /= !pair_pcore /=.
+    pose proof (Hf := cmra_morphism_pcore f (x1)).
+    destruct (pcore (f (x1))), (pcore (x1)); inv Hf=>//=.
+    pose proof (Hg := cmra_morphism_pcore g (x2)).
+    destruct (pcore (g (x2))), (pcore (x2)); inv Hg=>//=.
     by setoid_subst.
   - intros. by rewrite /prod_map /= !cmra_morphism_op.
 Qed.
 
-Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
+Program Definition prodRF {SI : sidx} (F1 F2 : rFunctor) : rFunctor := {|
   rFunctor_car A _ B _ := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
     prodO_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply rFunctor_map_ne.
+  intros ? F1 F2 A1 ? A2 ? B1 ? B2 ? n ???.
+  by apply prodO_map_ne; apply rFunctor_map_ne.
 Qed.
-Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_map_id. Qed.
+Next Obligation. by intros ? F1 F2 A ? B ? [??]; rewrite /= !rFunctor_map_id. Qed.
 Next Obligation.
-  intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
+  intros ? F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
   by rewrite !rFunctor_map_compose.
 Qed.
 Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.
 
-Global Instance prodRF_contractive F1 F2 :
+Global Instance prodRF_contractive {SI : sidx} F1 F2 :
   rFunctorContractive F1 → rFunctorContractive F2 →
   rFunctorContractive (prodRF F1 F2).
 Proof.
@@ -1308,22 +1370,23 @@ Proof.
     by apply prodO_map_ne; apply rFunctor_map_contractive.
 Qed.
 
-Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
+Program Definition prodURF {SI : sidx} (F1 F2 : urFunctor) : urFunctor := {|
   urFunctor_car A _ B _ := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
     prodO_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply urFunctor_map_ne.
+  intros ? F1 F2 A1 ? A2 ? B1 ? B2 ? n ???.
+  by apply prodO_map_ne; apply urFunctor_map_ne.
 Qed.
-Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_map_id. Qed.
+Next Obligation. by intros ? F1 F2 A ? B ? [??]; rewrite /= !urFunctor_map_id. Qed.
 Next Obligation.
-  intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
+  intros ? F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
   by rewrite !urFunctor_map_compose.
 Qed.
 Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope.
 
-Global Instance prodURF_contractive F1 F2 :
+Global Instance prodURF_contractive {SI : sidx} F1 F2 :
   urFunctorContractive F1 → urFunctorContractive F2 →
   urFunctorContractive (prodURF F1 F2).
 Proof.
@@ -1333,7 +1396,7 @@ Qed.
 
 (** ** CMRA for the option type *)
 Section option.
-  Context {A : cmra}.
+  Context {SI : sidx} {A : cmra}.
   Implicit Types a b : A.
   Implicit Types ma mb : option A.
   Local Arguments core _ _ !_ /.
@@ -1343,15 +1406,19 @@ Section option.
     match ma with Some a => ✓ a | None => True end.
   Local Instance option_validN_instance : ValidN (option A) := λ n ma,
     match ma with Some a => ✓{n} a | None => True end.
-  Local Instance option_pcore_instance : PCore (option A) := λ ma, Some (ma ≫= pcore).
+  Local Instance option_pcore_instance : PCore (option A) := λ ma,
+    Some (ma ≫= pcore).
   Local Arguments option_pcore_instance !_ /.
-  Local Instance option_op_instance : Op (option A) := union_with (λ a b, Some (a ⋅ b)).
+  Local Instance option_op_instance : Op (option A) :=
+    union_with (λ a b, Some (a ⋅ b)).
 
   Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
   Definition Some_validN a n : ✓{n} Some a ↔ ✓{n} a := reflexivity _.
   Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl.
-  Lemma Some_core `{CmraTotal A} a : Some (core a) = core (Some a).
+  Lemma Some_core `{!CmraTotal A} a : Some (core a) = core (Some a).
   Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
+  Lemma pcore_Some a : pcore (Some a) = Some (pcore a).
+  Proof. done. Qed.
   Lemma Some_op_opM a ma : Some a ⋅ ma = Some (a ⋅? ma).
   Proof. by destruct ma. Qed.
 
@@ -1363,7 +1430,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.
@@ -1378,7 +1445,8 @@ Section option.
   Qed.
 
   Lemma option_includedN n ma mb :
-    ma ≼{n} mb ↔ ma = None ∨ ∃ x y, ma = Some x ∧ mb = Some y ∧ (x ≡{n}≡ y ∨ x ≼{n} y).
+    ma ≼{n} mb ↔ ma = None ∨
+                 ∃ x y, ma = Some x ∧ mb = Some y ∧ (x ≡{n}≡ y ∨ x ≼{n} y).
   Proof.
     split.
     - intros [mc Hmc].
@@ -1399,6 +1467,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.
@@ -1407,7 +1477,8 @@ Section option.
     - destruct 1; by ofe_subst.
     - by destruct 1; rewrite /validN /option_validN_instance //=; ofe_subst.
     - intros [a|]; [apply cmra_valid_validN|done].
-    - intros n [a|]; unfold validN, option_validN_instance; eauto using cmra_validN_S.
+    - intros n m [a|];
+        unfold validN, option_validN_instance; eauto using cmra_validN_le.
     - intros [a|] [b|] [c|]; constructor; rewrite ?assoc; auto.
     - intros [a|] [b|]; constructor; rewrite 1?comm; auto.
     - intros [a|]; simpl; auto.
@@ -1455,12 +1526,16 @@ Section option.
 
   Lemma cmra_opM_opM_assoc a mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? (mb ⋅ mc).
   Proof. destruct mb, mc; by rewrite /= -?assoc. Qed.
-  Lemma cmra_opM_opM_assoc_L `{!LeibnizEquiv A} a mb mc : a ⋅? mb ⋅? mc = a ⋅? (mb ⋅ mc).
+  Lemma cmra_opM_opM_assoc_L `{!LeibnizEquiv A} a mb mc :
+    a ⋅? mb ⋅? mc = a ⋅? (mb ⋅ mc).
   Proof. unfold_leibniz. apply cmra_opM_opM_assoc. Qed.
   Lemma cmra_opM_opM_swap a mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? mc ⋅? mb.
   Proof. by rewrite !cmra_opM_opM_assoc (comm _ mb). Qed.
-  Lemma cmra_opM_opM_swap_L `{!LeibnizEquiv A} a mb mc : a ⋅? mb ⋅? mc = a ⋅? mc ⋅? mb.
+  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.
@@ -1481,14 +1556,47 @@ 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.
+  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.
-  Lemma Some_included_total `{CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
+  Lemma Some_included_total `{!CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
   Proof. rewrite Some_included. split; [|by eauto]. by intros [->|?]. Qed.
 
   Lemma Some_includedN_exclusive n a `{!Exclusive a} b :
@@ -1508,10 +1616,10 @@ Section option.
   Proof.
     intros Hirr ? n [b|] [c|] ? EQ; inversion_clear EQ.
     - constructor. by apply (cancelableN a).
-    - destruct (Hirr b); [|eauto using dist_le with lia].
-      by eapply (cmra_validN_op_l 0 a b), (cmra_validN_le n); last lia.
-    - destruct (Hirr c); [|symmetry; eauto using dist_le with lia].
-      by eapply (cmra_validN_le n); last lia.
+    - destruct (Hirr b); [|eauto using dist_le, SIdx.le_0_l].
+      by eapply (cmra_validN_op_l 0ᵢ a b), (cmra_validN_le n), SIdx.le_0_l.
+    - destruct (Hirr c); [|symmetry; eauto using dist_le, SIdx.le_0_l].
+      by eapply (cmra_validN_le n), SIdx.le_0_l.
     - done.
   Qed.
 
@@ -1520,36 +1628,48 @@ Section option.
   Proof. destruct ma; apply _. Qed.
 End option.
 
-Global Arguments optionR : clear implicits.
-Global Arguments optionUR : clear implicits.
+Global Arguments optionR {_} _.
+Global Arguments optionUR {_} _.
 
 Section option_prod.
-  Context {A B : cmra}.
+  Context {SI : sidx} {A B : cmra}.
   Implicit Types a : A.
   Implicit Types b : B.
 
   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_total_1 `{CmraTotal A} n a1 a2 b1 b2 :
+  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.
-  Lemma Some_pair_includedN_total_2 `{CmraTotal B} n a1 a2 b1 b2 :
+  Lemma Some_pair_includedN_total_2 `{!CmraTotal B} n a1 a2 b1 b2 :
     Some (a1,b1) ≼{n} Some (a2,b2) → Some a1 ≼{n} Some a2 ∧ b1 ≼{n} b2.
   Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ b1). Qed.
 
   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_total_1 `{CmraTotal A} a1 a2 b1 b2 :
+  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.
-  Lemma Some_pair_included_total_2 `{CmraTotal B} a1 a2 b1 b2 :
+  Lemma Some_pair_included_total_2 `{!CmraTotal B} a1 a2 b1 b2 :
     Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2 ∧ b1 ≼ b2.
   Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
 End option_prod.
 
-Lemma option_fmap_mono {A B : cmra} (f : A → B) (ma mb : option A) :
+Lemma option_fmap_mono {SI : sidx} {A B : cmra} (f : A → B) (ma mb : option A) :
   Proper ((≡) ==> (≡)) f →
   (∀ a b, a ≼ b → f a ≼ f b) →
   ma ≼ mb → f <$> ma ≼ f <$> mb.
@@ -1557,7 +1677,8 @@ Proof.
   intros ??. rewrite !option_included; intros [->|(a&b&->&->&?)]; naive_solver.
 Qed.
 
-Global Instance option_fmap_cmra_morphism {A B : cmra} (f: A → B) `{!CmraMorphism f} :
+Global Instance option_fmap_cmra_morphism {SI : sidx}
+    {A B : cmra} (f: A → B) `{!CmraMorphism f} :
   CmraMorphism (fmap f : option A → option B).
 Proof.
   split; first apply _.
@@ -1566,55 +1687,65 @@ Proof.
   - move=> [a|] [b|] //=. by rewrite (cmra_morphism_op f).
 Qed.
 
-Program Definition optionURF (F : rFunctor) : urFunctor := {|
+Program Definition optionURF {SI : sidx} (F : rFunctor) : urFunctor := {|
   urFunctor_car A _ B _ := optionUR (rFunctor_car F A B);
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_ne.
+  intros ? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
+  by apply optionO_map_ne, rFunctor_map_ne.
 Qed.
 Next Obligation.
-  intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
+  intros ? F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
   apply option_fmap_equiv_ext=>y; apply rFunctor_map_id.
 Qed.
 Next Obligation.
-  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
+  intros ? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x.
+  rewrite /= -option_fmap_compose.
   apply option_fmap_equiv_ext=>y; apply rFunctor_map_compose.
 Qed.
 
-Global Instance optionURF_contractive F :
+Global Instance optionURF_contractive {SI : sidx} F :
   rFunctorContractive F → urFunctorContractive (optionURF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
+  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
+  by apply optionO_map_ne, rFunctor_map_contractive.
 Qed.
 
-Program Definition optionRF (F : rFunctor) : rFunctor := {|
+Program Definition optionRF {SI : sidx} (F : rFunctor) : rFunctor := {|
   rFunctor_car A _ B _ := optionR (rFunctor_car F A B);
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
 |}.
-Solve Obligations with apply optionURF.
+Solve Obligations with apply @optionURF.
 
-Global Instance optionRF_contractive F :
+Global Instance optionRF_contractive {SI : sidx} F :
   rFunctorContractive F → rFunctorContractive (optionRF F).
 Proof. apply optionURF_contractive. Qed.
 
 (* Dependently-typed functions over a discrete domain *)
 Section discrete_fun_cmra.
-  Context `{B : A → ucmra}.
+  Context {SI : sidx} {A: Type} {B : A → ucmra}.
   Implicit Types f g : discrete_fun B.
 
-  Local Instance discrete_fun_op_instance : Op (discrete_fun B) := λ f g x, f x ⋅ g x.
-  Local Instance discrete_fun_pcore_instance : PCore (discrete_fun B) := λ f, Some (λ x, core (f x)).
-  Local Instance discrete_fun_valid_instance : Valid (discrete_fun B) := λ f, ∀ x, ✓ f x.
-  Local Instance discrete_fun_validN_instance : ValidN (discrete_fun B) := λ n f, ∀ x, ✓{n} f x.
+  Local Instance discrete_fun_op_instance : Op (discrete_fun B) := λ f g x,
+    f x ⋅ g x.
+  Local Instance discrete_fun_pcore_instance : PCore (discrete_fun B) := λ f,
+    Some (λ x, core (f x)).
+  Local Instance discrete_fun_valid_instance : Valid (discrete_fun B) := λ f,
+    ∀ x, ✓ f x.
+  Local Instance discrete_fun_validN_instance : ValidN (discrete_fun B) := λ n f,
+    ∀ x, ✓{n} f x.
 
   Definition discrete_fun_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.
   Definition discrete_fun_lookup_core f x : (core f) x = core (f x) := eq_refl.
 
   Lemma discrete_fun_included_spec_1 (f g : discrete_fun B) x : f ≼ g → f x ≼ g x.
-  Proof. by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op_instance (Hh x). Qed.
+  Proof.
+    by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op_instance (Hh x).
+  Qed.
 
-  Lemma discrete_fun_included_spec `{Hfin : Finite A} (f g : discrete_fun B) : f ≼ g ↔ ∀ x, f x ≼ g x.
+  Lemma discrete_fun_included_spec `{Finite A} (f g : discrete_fun B) :
+    f ≼ g ↔ ∀ x, f x ≼ g x.
   Proof.
     split; [by intros; apply discrete_fun_included_spec_1|].
     intros [h ?]%finite_choice; by exists h.
@@ -1624,29 +1755,31 @@ Section discrete_fun_cmra.
   Proof.
     apply cmra_total_mixin.
     - eauto.
-    - by intros n f1 f2 f3 Hf x; rewrite discrete_fun_lookup_op (Hf x).
-    - by intros n f1 f2 Hf x; rewrite discrete_fun_lookup_core (Hf x).
-    - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
+    - intros n f1 f2 f3 Hf x. by rewrite discrete_fun_lookup_op (Hf x).
+    - intros n f1 f2 Hf x. by rewrite discrete_fun_lookup_core (Hf x).
+    - intros n f1 f2 Hf ? x. by rewrite -(Hf x).
     - intros g; split.
       + intros Hg n i; apply cmra_valid_validN, Hg.
       + intros Hg i; apply cmra_valid_validN=> n; apply Hg.
-    - intros n f Hf x; apply cmra_validN_S, Hf.
-    - by intros f1 f2 f3 x; rewrite discrete_fun_lookup_op assoc.
-    - by intros f1 f2 x; rewrite discrete_fun_lookup_op comm.
-    - by intros f x; rewrite discrete_fun_lookup_op discrete_fun_lookup_core cmra_core_l.
-    - by intros f x; rewrite discrete_fun_lookup_core cmra_core_idemp.
+    - intros n n' f Hf ? x. eauto using cmra_validN_le.
+    - intros f1 f2 f3 x. by rewrite discrete_fun_lookup_op assoc.
+    - intros f1 f2 x. by rewrite discrete_fun_lookup_op comm.
+    - intros f x.
+      by rewrite discrete_fun_lookup_op discrete_fun_lookup_core cmra_core_l.
+    - intros f x. by rewrite discrete_fun_lookup_core cmra_core_idemp.
     - intros f1 f2 Hf12. exists (core f2)=>x. rewrite discrete_fun_lookup_op.
       apply (discrete_fun_included_spec_1 _ _ x), (cmra_core_mono (f1 x)) in Hf12.
       rewrite !discrete_fun_lookup_core. destruct Hf12 as [? ->].
       rewrite assoc -cmra_core_dup //.
-    - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
+    - intros n f1 f2 Hf x. apply cmra_validN_op_l with (f2 x), Hf.
     - intros n f f1 f2 Hf Hf12.
       assert (FUN := λ x, cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
       exists (λ x, projT1 (FUN x)), (λ x, proj1_sig (projT2 (FUN x))).
       split; [|split]=>x; [rewrite discrete_fun_lookup_op| |];
-      by destruct (FUN x) as (?&?&?&?&?).
+        by destruct (FUN x) as (?&?&?&?&?).
   Qed.
-  Canonical Structure discrete_funR := Cmra (discrete_fun B) discrete_fun_cmra_mixin.
+  Canonical Structure discrete_funR :=
+    Cmra (discrete_fun B) discrete_fun_cmra_mixin.
 
   Local Instance discrete_fun_unit_instance : Unit (discrete_fun B) := λ x, ε.
   Definition discrete_fun_lookup_empty x : ε x = ε := eq_refl.
@@ -1654,130 +1787,222 @@ Section discrete_fun_cmra.
   Lemma discrete_fun_ucmra_mixin : UcmraMixin (discrete_fun B).
   Proof.
     split.
-    - intros x; apply ucmra_unit_valid.
-    - by intros f x; rewrite discrete_fun_lookup_op left_id.
+    - intros x. apply ucmra_unit_valid.
+    - intros f x. by rewrite discrete_fun_lookup_op left_id.
     - constructor=> x. apply core_id_core, _.
   Qed.
-  Canonical Structure discrete_funUR := Ucmra (discrete_fun B) discrete_fun_ucmra_mixin.
+  Canonical Structure discrete_funUR :=
+    Ucmra (discrete_fun B) discrete_fun_ucmra_mixin.
 
   Global Instance discrete_fun_unit_discrete :
     (∀ i, Discrete (ε : B i)) → Discrete (ε : discrete_fun B).
   Proof. intros ? f Hf x. by apply: discrete. Qed.
 End discrete_fun_cmra.
 
-Global Arguments discrete_funR {_} _.
-Global Arguments discrete_funUR {_} _.
+Global Arguments discrete_funR {_ _} _.
+Global Arguments discrete_funUR {_ _} _.
 
-Global Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A → ucmra} (f : ∀ x, B1 x → B2 x) :
+Global Instance discrete_fun_map_cmra_morphism
+    {SI : sidx} {A} {B1 B2 : A → ucmra} (f : ∀ x, B1 x → B2 x) :
   (∀ x, CmraMorphism (f x)) → CmraMorphism (discrete_fun_map f).
 Proof.
   split; first apply _.
-  - intros n g Hg x; rewrite /discrete_fun_map; apply (cmra_morphism_validN (f _)), Hg.
+  - intros n g Hg x. rewrite /discrete_fun_map.
+    apply (cmra_morphism_validN (f _)), Hg.
   - intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
-  - intros g1 g2 i. by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op.
+  - intros g1 g2 i.
+    by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op.
 Qed.
 
-Program Definition discrete_funURF {C} (F : C → urFunctor) : urFunctor := {|
+Program Definition discrete_funURF
+    {SI : sidx} {C} (F : C → urFunctor) : urFunctor := {|
   urFunctor_car A _ B _ := discrete_funUR (λ c, urFunctor_car (F c) A B);
-  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := discrete_funO_map (λ c, urFunctor_map (F c) fg)
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
+    discrete_funO_map (λ c, urFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_map_ne=>?; apply urFunctor_map_ne.
+  intros ? C F A1 ? A2 ? B1 ? B2 ? n ?? g.
+  by apply discrete_funO_map_ne=>?; apply urFunctor_map_ne.
 Qed.
 Next Obligation.
-  intros C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
+  intros ? C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
   apply discrete_fun_map_ext=> y; apply urFunctor_map_id.
 Qed.
 Next Obligation.
-  intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. rewrite /=-discrete_fun_map_compose.
+  intros ? C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g.
+  rewrite /=-discrete_fun_map_compose.
   apply discrete_fun_map_ext=>y; apply urFunctor_map_compose.
 Qed.
-Global Instance discrete_funURF_contractive {C} (F : C → urFunctor) :
+Global Instance discrete_funURF_contractive {SI : sidx} {C} (F : C → urFunctor) :
   (∀ c, urFunctorContractive (F c)) → urFunctorContractive (discrete_funURF F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
-  by apply discrete_funO_map_ne=>c; apply urFunctor_map_contractive.
+  by apply discrete_funO_map_ne=> c; apply urFunctor_map_contractive.
 Qed.
 
-(** * Constructing a camera [B] through a bijection with [A] that
-is mostly an isomorphism but restricts validity. *)
-Lemma iso_cmra_mixin_restrict {A : cmra} {B : Type}
-  `{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
-  (f : A → B) (g : B → A)
-  (* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
-  (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
+(** * Constructing a camera [B] through a mapping into [A]
+
+The mapping may restrict the domain (i.e., we have an injection from [B] to [A],
+not a bijection) and validity. These two restrictions work on opposite "ends" of
+[A] according to [≼]: domain restriction must prove that when an element is in
+the domain, so is its composition with other elements; validity restriction must
+prove that if the composition of two elements is valid, then so are both of the
+elements. The "domain" is the image of [g] in [A], or equivalently the part of
+[A] where [f] returns [Some]. *)
+Lemma inj_cmra_mixin_restrict_validity {SI : sidx} {A : cmra} {B : ofe}
+  `{!PCore B, !Op B, !Valid B, !ValidN B}
+  (f : A → option B) (g : B → A)
+  (* [g] is proper/non-expansive and injective w.r.t. OFE equality *)
   (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
-  (* [g] is surjective (and [f] its inverse) *)
-  (gf : ∀ x, g (f x) ≡ x)
-  (* [g] commutes with [pcore] and [op] *)
-  (g_pcore : ∀ y, pcore (g y) ≡ g <$> pcore y)
-  (g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
+  (* [g] is surjective into the part of [A] where [is_Some ∘ f] holds
+  (and [f] its inverse) *)
+  (gf_dist : ∀ (x : A) (y : B) n, f x ≡{n}≡ Some y ↔ g y ≡{n}≡ x)
+  (* [g] commutes with [pcore] (on the part where it is defined) and [op] *)
+  (g_pcore_dist : ∀ (y cy : B) n,
+    pcore y ≡{n}≡ Some cy ↔ pcore (g y) ≡{n}≡ Some (g cy))
+  (g_op : ∀ (y1 y2 : B), g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
+  (* [g] also commutes with [opM] when the right-hand side is produced by [f],
+  and cancels the [f]. In particular this axiom implies that when taking an
+  element in the domain ([g y]), its composition with *any* [x : A] is still in
+  the domain, and [f] computes the preimage properly.
+  Note that just requiring "the composition of two elements from the domain
+  is in the domain" is insufficient for this lemma to hold. [g_op] already shows
+  that this is the case, but the issue is that in [pcore_mono] we obtain a
+  [g y1 ≼ g y2], and the existentially quantified "remainder" in the [≼] has no
+  reason to be in the domain, so [g_op] is too weak to turn this into some
+  relation between [y1] and [y2] in [B]. At the same time, [g_opM_f] does not
+  impl [g_op] since we need [g_op] to prove that [⋅] in [B] respects [≡].
+  Therefore both [g_op] and [g_opM_f] are required for this lemma to work. *)
+  (g_opM_f : ∀ (x : A) (y : B), g (y ⋅? f x) ≡ g y ⋅ x)
   (* The validity predicate on [B] restricts the one on [A] *)
-  (g_validN : ∀ n y, ✓{n} y → ✓{n} (g y))
+  (g_validN : ∀ n (y : B), ✓{n} y → ✓{n} (g y))
   (* The validity predicate on [B] satisfies the laws of validity *)
   (valid_validN_ne : ∀ n, Proper (dist n ==> impl) (validN (A:=B) n))
   (valid_rvalidN : ∀ y : B, ✓ y ↔ ∀ n, ✓{n} y)
-  (validN_S : ∀ n (y : B), ✓{S n} y → ✓{n} y)
+  (validN_le : ∀ n n' (y : B), ✓{n} y → n' ≤ n → ✓{n'} y)
   (validN_op_l : ∀ n (y1 y2 : B), ✓{n} (y1 ⋅ y2) → ✓{n} y1) :
   CmraMixin B.
 Proof.
+  (* Some general derived facts that will be useful later. *)
+  assert (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2).
+  { intros ??. rewrite !equiv_dist. naive_solver. }
+  assert (g_pcore : ∀ (y cy : B),
+    pcore y ≡ Some cy ↔ pcore (g y) ≡ Some (g cy)).
+  { intros. rewrite !equiv_dist. naive_solver. }
+  assert (gf : ∀ x y, f x ≡ Some y ↔ g y ≡ x).
+  { intros. rewrite !equiv_dist. naive_solver. }
+  assert (fg : ∀ y, f (g y) ≡ Some y).
+  { intros. apply gf. done. }
+  assert (g_ne : NonExpansive g).
+  { intros n ???. apply g_dist. done. }
+  (* Some of the CMRA properties are useful in proving the others. *)
+  assert (b_pcore_l' : ∀ y cy : B, pcore y ≡ Some cy → cy ⋅ y ≡ y).
+  { intros y cy Hy. apply g_equiv. rewrite g_op. apply cmra_pcore_l'.
+    apply g_pcore. done. }
+  assert (b_pcore_idemp : ∀ y cy : B, pcore y ≡ Some cy → pcore cy ≡ Some cy).
+  { intros y cy Hy. eapply g_pcore, cmra_pcore_idemp', g_pcore. done. }
+  (* Now prove all the mixin laws. *)
   split.
   - intros y n z1 z2 Hz%g_dist. apply g_dist. by rewrite !g_op Hz.
   - intros n y1 y2 cy Hy%g_dist Hy1.
     assert (g <$> pcore y2 ≡{n}≡ Some (g cy))
-      as (cx&(cy'&->&->)%fmap_Some_1&?%g_dist)%dist_Some_inv_r'; [|by eauto].
-    by rewrite -g_pcore -Hy g_pcore Hy1.
+      as (cx & (cy'&->&->)%fmap_Some_1 & ?%g_dist)%dist_Some_inv_r'; [|by eauto].
+    assert (Hgcy : pcore (g y1) ≡ Some (g cy)).
+    { apply g_pcore. rewrite Hy1. done. }
+    rewrite equiv_dist in Hgcy. specialize (Hgcy n).
+    rewrite Hy in Hgcy. apply g_pcore_dist in Hgcy. rewrite Hgcy. done.
   - done.
   - done.
   - done.
   - intros y1 y2 y3. apply g_equiv. by rewrite !g_op assoc.
   - intros y1 y2. apply g_equiv. by rewrite !g_op comm.
-  - intros y cy Hy. apply g_equiv. rewrite g_op. apply cmra_pcore_l'.
-    by rewrite g_pcore Hy.
-  - intros y cy Hy.
-    assert (g <$> pcore cy ≡ Some (g cy)) as (cy'&->&?)%fmap_Some_equiv.
-    { rewrite -g_pcore.
-      apply cmra_pcore_idemp' with (g y). by rewrite g_pcore Hy. }
-    constructor. by apply g_equiv.
+  - intros y cy Hcy. apply b_pcore_l'. by rewrite Hcy.
+  - intros y cy Hcy. eapply b_pcore_idemp. by rewrite -Hcy.
   - intros y1 y2 cy [z Hy2] Hy1.
     destruct (cmra_pcore_mono' (g y1) (g y2) (g cy)) as (cx&Hcgy2&[x Hcx]).
     { exists (g z). rewrite -g_op. by apply g_equiv. }
-    { by rewrite g_pcore Hy1. }
-    assert (g <$> pcore y2 ≡ Some cx) as (cy'&->&?)%fmap_Some_equiv.
-    { by rewrite -g_pcore Hcgy2. }
-    exists cy'; split; [done|].
-    exists (f x). apply g_equiv. by rewrite g_op gf -Hcx.
+    { apply g_pcore. rewrite Hy1 //. }
+    apply (reflexive_eq (R:=equiv)) in Hcgy2.
+    rewrite -g_opM_f in Hcx. rewrite Hcx in Hcgy2.
+    apply g_pcore in Hcgy2.
+    apply Some_equiv_eq in Hcgy2 as [cy' [-> Hcy']].
+    eexists. split; first done.
+    destruct (f x) as [y|].
+    + exists y. done.
+    + exists cy. apply (reflexive_eq (R:=equiv)), b_pcore_idemp, b_pcore_l' in Hy1.
+      rewrite Hy1 //.
   - done.
   - intros n y z1 z2 ?%g_validN ?.
-    destruct (cmra_extend n (g y) (g z1) (g z2)) as (x1&x2&Hgy&?&?).
+    destruct (cmra_extend n (g y) (g z1) (g z2)) as (x1&x2&Hgy&Hx1&Hx2).
     { done. }
     { rewrite -g_op. by apply g_dist. }
-    exists (f x1), (f x2). split_and!.
-    + apply g_equiv. by rewrite Hgy g_op !gf.
-    + apply g_dist. by rewrite gf.
-    + apply g_dist. by rewrite gf.
+    symmetry in Hx1, Hx2.
+    apply gf_dist in Hx1, Hx2.
+    destruct (f x1) as [y1|] eqn:Hy1; last first.
+    { exfalso. inversion Hx1. }
+    destruct (f x2) as [y2|] eqn:Hy2; last first.
+    { exfalso. inversion Hx2. }
+    exists y1, y2. split_and!.
+    + apply g_equiv. rewrite Hgy g_op.
+      f_equiv; symmetry; apply gf; rewrite ?Hy1 ?Hy2 //.
+    + apply g_dist. apply (inj Some) in Hx1. rewrite Hx1 //.
+    + apply g_dist. apply (inj Some) in Hx2. rewrite Hx2 //.
 Qed.
 
-(** * Constructing a camera through an isomorphism *)
-Lemma iso_cmra_mixin {A : cmra} {B : Type}
-  `{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
+(** Constructing a CMRA through an isomorphism that may restrict validity. *)
+Lemma iso_cmra_mixin_restrict_validity {SI : sidx} {A : cmra} {B : ofe}
+  `{!PCore B, !Op B, !Valid B, !ValidN B}
   (f : A → B) (g : B → A)
   (* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
-  (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
   (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
   (* [g] is surjective (and [f] its inverse) *)
-  (gf : ∀ x, g (f x) ≡ x)
+  (gf : ∀ x : A, g (f x) ≡ x)
+  (* [g] commutes with [pcore] and [op] *)
+  (g_pcore : ∀ y : B, pcore (g y) ≡ g <$> pcore y)
+  (g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
+  (* The validity predicate on [B] restricts the one on [A] *)
+  (g_validN : ∀ n y, ✓{n} y → ✓{n} (g y))
+  (* The validity predicate on [B] satisfies the laws of validity *)
+  (valid_validN_ne : ∀ n, Proper (dist n ==> impl) (validN (A:=B) n))
+  (valid_rvalidN : ∀ y : B, ✓ y ↔ ∀ n, ✓{n} y)
+  (validN_le: ∀ n m (y : B), ✓{n} y → m ≤ n → ✓{m} y)
+  (validN_op_l : ∀ n (y1 y2 : B), ✓{n} (y1 ⋅ y2) → ✓{n} y1) :
+  CmraMixin B.
+Proof.
+  assert (g_ne : NonExpansive g).
+  { intros n ???. apply g_dist. done. }
+  assert (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2).
+  { intros ??.
+    split; intros ?; apply equiv_dist; intros; apply g_dist, equiv_dist; done. }
+  apply (inj_cmra_mixin_restrict_validity (λ x, Some (f x)) g); try done.
+  - intros. split.
+    + intros Hy%(inj Some). rewrite -Hy gf //.
+    + intros ?. f_equiv. apply g_dist. rewrite gf. done.
+  - intros. rewrite g_pcore. split.
+    + intros ->. done.
+    + intros (? & -> & ->%g_dist)%fmap_Some_dist. done.
+  - intros ??. simpl. rewrite g_op gf //.
+Qed.
+
+(** * Constructing a camera through an isomorphism *)
+Lemma iso_cmra_mixin {SI : sidx} {A : cmra} {B : ofe}
+  `{!PCore B, !Op B, !Valid B, !ValidN B}
+  (f : A → B) (g : B → A)
+  (* [g] is proper/non-expansive and injective w.r.t. OFE equality *)
+  (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
+  (* [g] is surjective (and [f] its inverse) *)
+  (gf : ∀ x : A, g (f x) ≡ x)
   (* [g] commutes with [pcore], [op], [valid], and [validN] *)
-  (g_pcore : ∀ y, pcore (g y) ≡ g <$> pcore y)
+  (g_pcore : ∀ y : B, pcore (g y) ≡ g <$> pcore y)
   (g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
   (g_valid : ∀ y, ✓ (g y) ↔ ✓ y)
   (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y) :
   CmraMixin B.
 Proof.
-  apply (iso_cmra_mixin_restrict f g); auto.
+  apply (iso_cmra_mixin_restrict_validity f g); auto.
   - by intros n y ?%g_validN.
   - intros n y1 y2 Hy%g_dist Hy1. by rewrite -g_validN -Hy g_validN.
   - intros y. rewrite -g_valid cmra_valid_validN. naive_solver.
-  - intros n y. rewrite -!g_validN. apply cmra_validN_S.
+  - intros n m y. rewrite -!g_validN. apply cmra_validN_le.
   - intros n y1 y2. rewrite -!g_validN g_op. apply cmra_validN_op_l.
 Qed.

iris/algebra/cmra_big_op.v

@@ -3,30 +3,33 @@ From iris.algebra Require Export big_op cmra.
 From iris.prelude Require Import options.
 
 (** Option *)
-Lemma big_opL_None {M : cmra} {A} (f : nat → A → option M) l :
+Lemma big_opL_None {SI : sidx} {M : cmra} {A} (f : nat → A → option M) l :
   ([^op list] k↦x ∈ l, f k x) = None ↔ ∀ k x, l !! k = Some x → f k x = None.
 Proof.
   revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split.
   - intros [??] [|k] y ?; naive_solver.
   - intros Hl. split; [by apply (Hl 0)|]. intros k. apply (Hl (S k)).
 Qed.
-Lemma big_opM_None {M : cmra} `{Countable K} {A} (f : K → A → option M) m :
+Lemma big_opM_None {SI : sidx}
+    {M : cmra} `{Countable K} {A} (f : K → A → option M) m :
   ([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
 Proof.
-  induction m as [|i x m ? IH] using map_ind=> /=; first by rewrite big_opM_eq.
+  induction m as [|i x m ? IH] using map_ind=> /=.
+  { by rewrite big_opM_empty. }
   rewrite -None_equiv_eq big_opM_insert // None_equiv_eq op_None IH. split.
   { intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
   intros Hm; split.
   - apply (Hm i). by simplify_map_eq.
   - intros k y ?. apply (Hm k). by simplify_map_eq.
 Qed.
-Lemma big_opS_None {M : cmra} `{Countable A} (f : A → option M) X :
+Lemma big_opS_None {SI : sidx} {M : cmra} `{Countable A} (f : A → option M) X :
   ([^op set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
 Proof.
-  induction X as [|x X ? IH] using set_ind_L; [by rewrite big_opS_eq |].
+  induction X as [|x X ? IH] using set_ind_L.
+  { by rewrite big_opS_empty. }
   rewrite -None_equiv_eq big_opS_insert // None_equiv_eq op_None IH. set_solver.
 Qed.
-Lemma big_opMS_None {M : cmra} `{Countable A} (f : A → option M) X :
+Lemma big_opMS_None {SI : sidx} {M : cmra} `{Countable A} (f : A → option M) X :
   ([^op mset] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
 Proof.
   induction X as [|x X IH] using gmultiset_ind.

iris/algebra/coPset.v

@@ -7,6 +7,7 @@ generalize the construction without breaking canonical structures. *)
 
 (* The union CMRA *)
 Section coPset.
+  Context {SI : sidx}.
   Implicit Types X Y : coPset.
 
   Canonical Structure coPsetO := discreteO coPset.
@@ -47,7 +48,7 @@ Section coPset.
   Canonical Structure coPsetUR := Ucmra coPset coPset_ucmra_mixin.
 
   Lemma coPset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
-  Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
+  Proof using SI. destruct mY; by rewrite /= ?right_id_L. Qed.
 
   Lemma coPset_update X Y : X ~~> Y.
   Proof. done. Qed.
@@ -60,22 +61,23 @@ Section coPset.
   Qed.
 End coPset.
 
-(* The disjoiny union CMRA *)
+(* The disjoint union CMRA *)
 Inductive coPset_disj :=
   | CoPset : coPset → coPset_disj
-  | CoPsetBot : coPset_disj.
+  | CoPsetInvalid : coPset_disj.
 
 Section coPset_disj.
+  Context {SI : sidx}.
   Local Arguments op _ _ !_ !_ /.
   Canonical Structure coPset_disjO := leibnizO coPset_disj.
 
   Local Instance coPset_disj_valid_instance : Valid coPset_disj := λ X,
-    match X with CoPset _ => True | CoPsetBot => False end.
+    match X with CoPset _ => True | CoPsetInvalid => False end.
   Local Instance coPset_disj_unit_instance : Unit coPset_disj := CoPset ∅.
   Local Instance coPset_disj_op_instance : Op coPset_disj := λ X Y,
     match X, Y with
-    | CoPset X, CoPset Y => if decide (X ## Y) then CoPset (X ∪ Y) else CoPsetBot
-    | _, _ => CoPsetBot
+    | CoPset X, CoPset Y => if decide (X ## Y) then CoPset (X ∪ Y) else CoPsetInvalid
+    | _, _ => CoPsetInvalid
     end.
   Local Instance coPset_disj_pcore_instance : PCore coPset_disj := λ _, Some ε.
 

iris/algebra/cofe_solver.v

 From iris.algebra Require Export ofe.
+From iris.algebra Require Export stepindex_finite.
 From iris.prelude Require Import options.
 
+(** * Solver for recursive domain equations over Cofes for FINITE step-indices *)
+(** This file implements a solver for recursive equations of the form [F X ≃ X],
+where [F] is a locally contractive functor of Cofes. As such, it is an
+implementation of America and Rutten's theorem. More details can be found in the
+Iris Reference.
+
+This implementation only works for the [nat] index type. Importing this file
+will globally fix the index type to [nat]. *)
+
+(* Note that [Inhabited] is not derivable. Take [F X := ▶ X], then a possible
+solution is [Empty_set]. *)
 Record solution (F : oFunctor) := Solution {
   solution_car :> ofe;
+  solution_inhabited : Inhabited solution_car;
   solution_cofe : Cofe solution_car;
   solution_iso :> ofe_iso (oFunctor_apply F solution_car) solution_car;
 }.
-Global Existing Instance solution_cofe.
+Global Existing Instances solution_inhabited solution_cofe.
 
 Module solver. Section solver.
-Context (F : oFunctor) `{Fcontr : oFunctorContractive F}.
+Context (F : oFunctor) `{Fcontr : !oFunctorContractive F}.
 Context `{Fcofe : ∀ (T : ofe) `{!Cofe T}, Cofe (oFunctor_apply F T)}.
 Context `{Finh : Inhabited (oFunctor_apply F unitO)}.
 Notation map := (oFunctor_map F).
@@ -17,7 +30,7 @@ Notation map := (oFunctor_map F).
 Fixpoint A' (k : nat) : { C : ofe & Cofe C } :=
   match k with
   | 0 => existT (P:=Cofe) unitO _
-  | S k => existT (P:=Cofe) (@oFunctor_apply F (projT1 (A' k)) (projT2 (A' k))) _
+  | S k => existT (P:=Cofe) (@oFunctor_apply _ F (projT1 (A' k)) (projT2 (A' k))) _
   end.
 Notation A k := (projT1 (A' k)).
 Local Instance A_cofe k : Cofe (A k) := projT2 (A' k).
@@ -54,21 +67,22 @@ Global Instance tower_equiv : Equiv tower := λ X Y, ∀ k, X k ≡ Y k.
 Global Instance tower_dist : Dist tower := λ n X Y, ∀ k, X k ≡{n}≡ Y k.
 Definition tower_ofe_mixin : OfeMixin tower.
 Proof.
-  split.
+  apply ofe_mixin_finite.
   - intros X Y; split; [by intros HXY n k; apply equiv_dist|].
     intros HXY k; apply equiv_dist; intros n; apply HXY.
   - intros k; split.
     + by intros X n.
     + by intros X Y ? n.
     + by intros X Y Z ?? n; trans (Y n).
-  - intros k X Y HXY n; apply dist_S.
-    by rewrite -(g_tower X) (HXY (S n)) g_tower.
+  - intros k X Y HXY n. specialize (HXY (S n)).
+    apply (dist_le _ k) in HXY; [|apply SIdx.le_succ_diag_r].
+    by rewrite -(g_tower X) HXY g_tower.
 Qed.
 Definition T : ofe := Ofe tower tower_ofe_mixin.
 
 Program Definition tower_chain (c : chain T) (k : nat) : chain (A k) :=
   {| chain_car i := c i k |}.
-Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
+Next Obligation. intros c k n i ?; by apply (chain_cauchy c n). Qed.
 Program Definition tower_compl : Compl T := λ c,
   {| tower_car n := compl (tower_chain c n) |}.
 Next Obligation.
@@ -76,10 +90,9 @@ Next Obligation.
   by rewrite (conv_compl n (tower_chain c k))
     (conv_compl n (tower_chain c (S k))) /= (g_tower (c _) k).
 Qed.
-Global Program Instance tower_cofe : Cofe T := { compl := tower_compl }.
+Global Program Instance tower_cofe : Cofe T := cofe_finite tower_compl _.
 Next Obligation.
-  intros n c k; rewrite /= (conv_compl n (tower_chain c k)).
-  apply (chain_cauchy c); lia.
+  intros n c k; rewrite /= (conv_compl n (tower_chain c k)). done.
 Qed.
 
 Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
@@ -177,10 +190,12 @@ Proof.
   - rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
 Qed.
 
+Global Instance tower_inhabited : Inhabited tower := populate (embed 0 ()).
+
 Program Definition unfold_chain (X : T) : chain (oFunctor_apply F T) :=
   {| chain_car n := map (project n,embed' n) (X (S n)) |}.
 Next Obligation.
-  intros X n i Hi.
+  simpl; intros X n i Hi.
   assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
   induction k as [|k IH]; simpl; first done.
   rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
@@ -206,7 +221,7 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
 
 Theorem result : solution F.
 Proof using Type*.
-  refine (Solution F T _ (OfeIso (OfeMor fold) (OfeMor unfold) _ _)).
+  refine (Solution F T _ _ (OfeIso (OfeMor fold) (OfeMor unfold) _ _)).
   - move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
     rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
     trans (map (ff n, gg n) (X (S (n + k)))).
@@ -229,7 +244,7 @@ Proof using Type*.
     rewrite (map_ff_gg _ _ _ H).
     apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
   - intros X; rewrite equiv_dist=> n /=.
-    rewrite /unfold /= (conv_compl' n (unfold_chain (fold X))) /=.
+    rewrite /unfold /= (conv_compl_S n (unfold_chain (fold X))) /=.
     rewrite g_S -!oFunctor_map_compose -{2}[X]oFunctor_map_id.
     apply (contractive_ne map); split => Y /=.
     + rewrite f_tower. apply dist_S. by rewrite embed_tower.

iris/algebra/csum.v

@@ -4,22 +4,22 @@ From iris.prelude Require Import options.
 
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.
-Local Arguments validN _ _ _ !_ /.
+Local Arguments validN _ _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
-Local Arguments cmra_validN _ _ !_ /.
+Local Arguments cmra_validN _ _ _ !_ /.
 Local Arguments cmra_valid _  !_ /.
 
 Inductive csum (A B : Type) :=
   | Cinl : A → csum A B
   | Cinr : B → csum A B
-  | CsumBot : csum A B.
+  | CsumInvalid : csum A B.
 Global Arguments Cinl {_ _} _.
 Global Arguments Cinr {_ _} _.
-Global Arguments CsumBot {_ _}.
+Global Arguments CsumInvalid {_ _}.
 
 Global Instance: Params (@Cinl) 2 := {}.
 Global Instance: Params (@Cinr) 2 := {}.
-Global Instance: Params (@CsumBot) 2 := {}.
+Global Instance: Params (@CsumInvalid) 2 := {}.
 
 Global Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
   match x with Cinl a => Some a | _ => None end.
@@ -27,7 +27,7 @@ Global Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
   match x with Cinr b => Some b | _ => None end.
 
 Section ofe.
-Context {A B : ofe}.
+Context {SI : sidx} {A B : ofe}.
 Implicit Types a : A.
 Implicit Types b : B.
 
@@ -35,12 +35,12 @@ Implicit Types b : B.
 Inductive csum_equiv : Equiv (csum A B) :=
   | Cinl_equiv a a' : a ≡ a' → Cinl a ≡ Cinl a'
   | Cinr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b'
-  | CsumBot_equiv : CsumBot ≡ CsumBot.
+  | CsumInvalid_equiv : CsumInvalid ≡ CsumInvalid.
 Local Existing Instance csum_equiv.
 Inductive csum_dist : Dist (csum A B) :=
   | Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a'
   | Cinr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
-  | CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
+  | CsumInvalid_dist n : CsumInvalid ≡{n}≡ CsumInvalid.
 Local Existing Instance csum_dist.
 
 Global Instance Cinl_ne : NonExpansive (@Cinl A B).
@@ -65,13 +65,13 @@ Proof.
   split.
   - intros mx my; split.
     + by destruct 1; constructor; try apply equiv_dist.
-    + intros Hxy; feed inversion (Hxy 0); subst; constructor; try done;
-      apply equiv_dist=> n; by feed inversion (Hxy n).
+    + intros Hxy; oinversion (Hxy 0ᵢ); subst; constructor; try done;
+      apply equiv_dist=> n; by oinversion (Hxy n).
   - intros n; split.
     + by intros [|a|]; constructor.
     + by destruct 1; constructor.
     + destruct 1; inversion_clear 1; constructor; etrans; eauto.
-  - by inversion_clear 1; constructor; apply dist_S.
+  - inversion_clear 1; intros Hlt; constructor; eauto using dist_le.
 Qed.
 Canonical Structure csumO : ofe := Ofe (csum A B) csum_ofe_mixin.
 
@@ -81,36 +81,71 @@ Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
 Program Definition csum_chain_r (c : chain csumO) (b : B) : chain B :=
   {| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}.
 Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Definition csum_compl `{Cofe A, Cofe B} : Compl csumO := λ c,
-  match c 0 with
+Definition csum_compl `{!Cofe A, !Cofe B} : Compl csumO := λ c,
+  match c 0ᵢ with
   | Cinl a => Cinl (compl (csum_chain_l c a))
   | Cinr b => Cinr (compl (csum_chain_r c b))
-  | CsumBot => CsumBot
+  | CsumInvalid => CsumInvalid
   end.
-Global Program Instance csum_cofe `{Cofe A, Cofe B} : Cofe csumO :=
-  {| compl := csum_compl |}.
+
+Program Definition csum_bchain_l {α} (c : bchain csumO α) (a : A) : bchain A α :=
+  {| bchain_car β Hβ := match c β Hβ return _ with Cinl a' => a' | _ => a end |}.
+Next Obligation.
+  intros α c a β γ Hle Hβ Hγ. simpl.
+  by destruct (bchain_cauchy _ c β γ Hle Hβ Hγ).
+Qed.
+Program Definition csum_bchain_r {α} (c : bchain csumO α) (b : B) : bchain B α :=
+  {| bchain_car β Hβ := match c β Hβ return _ with Cinr b' => b' | _ => b end |}.
+Next Obligation.
+  intros α c b β γ Hle Hβ Hγ. simpl.
+  by destruct (bchain_cauchy _ c β γ Hle Hβ Hγ).
+Qed.
+Definition csum_lbcompl `{!Cofe A, !Cofe B} : LBCompl csumO := λ n Hn c,
+  match c _ (SIdx.limit_lt_0 _ Hn) with
+  | Cinl a => Cinl (lbcompl Hn (csum_bchain_l c a))
+  | Cinr b => Cinr (lbcompl Hn (csum_bchain_r c b))
+  | CsumInvalid => CsumInvalid
+  end.
+
+Global Program Instance csum_cofe `{!Cofe A, !Cofe B} : Cofe csumO :=
+  {| compl := csum_compl; lbcompl := csum_lbcompl |}.
 Next Obligation.
   intros ?? n c; rewrite /compl /csum_compl.
-  feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
-  + rewrite (conv_compl n (csum_chain_l c _)) /=. destruct (c n); naive_solver.
-  + rewrite (conv_compl n (csum_chain_r c _)) /=. destruct (c n); naive_solver.
+  oinversion (chain_cauchy c 0ᵢ n); first apply SIdx.le_0_l; constructor.
+  - rewrite (conv_compl n (csum_chain_l c _)) /=. destruct (c n); naive_solver.
+  - rewrite (conv_compl n (csum_chain_r c _)) /=. destruct (c n); naive_solver.
+Qed.
+Next Obligation.
+  intros ?? n Hn c m Hm. rewrite /lbcompl /csum_lbcompl.
+  oinversion (bchain_cauchy _ c 0ᵢ m (SIdx.limit_lt_0 _ Hn) Hm);
+    [apply SIdx.le_0_l|..]; f_equiv.
+  - rewrite (conv_lbcompl Hn (csum_bchain_l c _) Hm) /=.
+    destruct (c m); naive_solver.
+  - rewrite (conv_lbcompl Hn (csum_bchain_r c _) Hm) /=.
+    destruct (c m); naive_solver.
+Qed.
+Next Obligation.
+  intros ?? n Hn c1 c2 m Hc. rewrite /lbcompl /csum_lbcompl.
+  destruct (Hc 0ᵢ (SIdx.limit_lt_0 _ Hn)); f_equiv.
+  - apply lbcompl_ne=> p Hp /=. by destruct (Hc p Hp).
+  - apply lbcompl_ne=> p Hp /=. by destruct (Hc p Hp).
 Qed.
 
 Global Instance csum_ofe_discrete :
   OfeDiscrete A → OfeDiscrete B → OfeDiscrete csumO.
-Proof. by inversion_clear 3; constructor; apply (discrete _). Qed.
+Proof. by inversion_clear 3; constructor; apply (discrete_0 _). Qed.
 Global Instance csum_leibniz :
   LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv csumO.
 Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.
 
 Global Instance Cinl_discrete a : Discrete a → Discrete (Cinl a).
-Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
+Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
 Global Instance Cinr_discrete b : Discrete b → Discrete (Cinr b).
-Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
+Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
 
 End ofe.
 
-Global Arguments csumO : clear implicits.
+Global Arguments csumO {_} _ _.
 
 (* Functor on COFEs *)
 Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
@@ -118,7 +153,7 @@ Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
   match x with
   | Cinl a => Cinl (fA a)
   | Cinr b => Cinr (fB b)
-  | CsumBot => CsumBot
+  | CsumInvalid => CsumInvalid
   end.
 Global Instance: Params (@csum_map) 4 := {}.
 
@@ -128,22 +163,22 @@ Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'')
                        (g : B → B') (g' : B' → B'') (x : csum A B) :
   csum_map (f' ∘ f) (g' ∘ g) x = csum_map f' g' (csum_map f g x).
 Proof. by destruct x. Qed.
-Lemma csum_map_ext {A A' B B' : ofe} (f f' : A → A') (g g' : B → B') x :
+Lemma csum_map_ext {SI : sidx} {A A' B B' : ofe} (f f' : A → A') (g g' : B → B') x :
   (∀ x, f x ≡ f' x) → (∀ x, g x ≡ g' x) → csum_map f g x ≡ csum_map f' g' x.
 Proof. by destruct x; constructor. Qed.
-Global Instance csum_map_cmra_ne {A A' B B' : ofe} n :
+Global Instance csum_map_cmra_ne {SI : sidx} {A A' B B' : ofe} n :
   Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
          (@csum_map A A' B B').
 Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
-Definition csumO_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
+Definition csumO_map {SI : sidx} {A A' B B'} (f : A -n> A') (g : B -n> B') :
   csumO A B -n> csumO A' B' :=
   OfeMor (csum_map f g).
-Global Instance csumO_map_ne A A' B B' :
-  NonExpansive2 (@csumO_map A A' B B').
+Global Instance csumO_map_ne {SI : sidx} A A' B B' :
+  NonExpansive2 (@csumO_map SI A A' B B').
 Proof. by intros n f f' Hf g g' Hg []; constructor. Qed.
 
 Section cmra.
-Context {A B : cmra}.
+Context {SI : sidx} {A B : cmra}.
 Implicit Types a : A.
 Implicit Types b : B.
 
@@ -152,25 +187,25 @@ Local Instance csum_valid_instance : Valid (csum A B) := λ x,
   match x with
   | Cinl a => ✓ a
   | Cinr b => ✓ b
-  | CsumBot => False
+  | CsumInvalid => False
   end.
 Local Instance csum_validN_instance : ValidN (csum A B) := λ n x,
   match x with
   | Cinl a => ✓{n} a
   | Cinr b => ✓{n} b
-  | CsumBot => False
+  | CsumInvalid => False
   end.
 Local Instance csum_pcore_instance : PCore (csum A B) := λ x,
   match x with
   | Cinl a => Cinl <$> pcore a
   | Cinr b => Cinr <$> pcore b
-  | CsumBot => Some CsumBot
+  | CsumInvalid => Some CsumInvalid
   end.
 Local Instance csum_op_instance : Op (csum A B) := λ x y,
   match x, y with
   | Cinl a, Cinl a' => Cinl (a ⋅ a')
   | Cinr b, Cinr b' => Cinr (b ⋅ b')
-  | _, _ => CsumBot
+  | _, _ => CsumInvalid
   end.
 
 Lemma Cinl_op a a' : Cinl (a ⋅ a') = Cinl a ⋅ Cinl a'.
@@ -184,14 +219,14 @@ Lemma Cinr_valid b : ✓ (Cinr b) ↔ ✓ b.
 Proof. done. Qed.
 
 Lemma csum_included x y :
-  x ≼ y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼ a')
+  x ≼ y ↔ y = CsumInvalid ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼ a')
                       ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼ b').
 Proof.
   split.
   - unfold included. intros [[a'|b'|] Hy]; destruct x as [a|b|];
       inversion_clear Hy; eauto 10.
   - intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
-    + destruct x; exists CsumBot; constructor.
+    + destruct x; exists CsumInvalid; constructor.
     + exists (Cinl c); by constructor.
     + exists (Cinr c); by constructor.
 Qed.
@@ -199,16 +234,19 @@ 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 CsumInvalid_included x : x ≼ CsumInvalid.
+Proof. exists CsumInvalid. by destruct x. Qed.
+(** We register a hint for [CsumInvalid_included] below. *)
 
 Lemma csum_includedN n x y :
-  x ≼{n} y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼{n} a')
+  x ≼{n} y ↔ y = CsumInvalid ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼{n} a')
                          ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼{n} b').
 Proof.
   split.
   - unfold includedN. intros [[a'|b'|] Hy]; destruct x as [a|b|];
       inversion_clear Hy; eauto 10.
   - intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
-    + destruct x; exists CsumBot; constructor.
+    + destruct x; exists CsumInvalid; constructor.
     + exists (Cinl c); by constructor.
     + exists (Cinr c); by constructor.
 Qed.
@@ -225,8 +263,8 @@ Proof.
       destruct (cmra_pcore_ne n b b' cb) as (cb'&->&?); auto.
       exists (Cinr cb'); by repeat constructor.
   - intros ? [a|b|] [a'|b'|] H; inversion_clear H; ofe_subst; done.
-  - intros [a|b|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
-  - intros n [a|b|]; simpl; auto using cmra_validN_S.
+  - pose 0ᵢ. intros [a|b|]; rewrite /= ?cmra_valid_validN; naive_solver.
+  - intros n m [a|b|]; simpl; eauto using cmra_validN_le.
   - intros [a1|b1|] [a2|b2|] [a3|b3|]; constructor; by rewrite ?assoc.
   - intros [a1|b1|] [a2|b2|]; constructor; by rewrite 1?comm.
   - intros [a|b|] ? [=]; subst; auto.
@@ -236,11 +274,11 @@ Proof.
       constructor; eauto using cmra_pcore_l.
   - intros [a|b|] ? [=]; subst; auto.
     + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
-      feed inversion (cmra_pcore_idemp a ca); repeat constructor; auto.
+      oinversion (cmra_pcore_idemp a ca); repeat constructor; auto.
     + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
-      feed inversion (cmra_pcore_idemp b cb); repeat constructor; auto.
+      oinversion (cmra_pcore_idemp b cb); repeat constructor; auto.
   - intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=].
-    + exists CsumBot. rewrite csum_included; eauto.
+    + exists CsumInvalid. rewrite csum_included; eauto.
     + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
       destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto.
       exists (Cinl ca'). rewrite csum_included; eauto 10.
@@ -255,7 +293,7 @@ Proof.
     + destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'.
       destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); [done|apply (inj Cinr), Hx'|].
       exists (Cinr z1), (Cinr z2). by repeat constructor.
-    + by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'.
+    + by exists CsumInvalid, CsumInvalid; destruct y1, y2; inversion_clear Hx'.
 Qed.
 Canonical Structure csumR := Cmra (csum A B) csum_cmra_mixin.
 
@@ -295,7 +333,7 @@ Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
 (** Interaction with [option] *)
 Lemma Some_csum_includedN x y n :
   Some x ≼{n} Some y ↔
-    y = CsumBot ∨
+    y = CsumInvalid ∨
     (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ Some a ≼{n} Some a') ∨
     (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ Some b ≼{n} Some b').
 Proof.
@@ -305,7 +343,7 @@ Proof.
 Qed.
 Lemma Some_csum_included x y :
   Some x ≼ Some y ↔
-    y = CsumBot ∨
+    y = CsumInvalid ∨
     (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ Some a ≼ Some a') ∨
     (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ Some b ≼ Some b').
 Proof.
@@ -366,10 +404,16 @@ Proof.
 Qed.
 End cmra.
 
-Global Arguments csumR : clear implicits.
+(* 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 (_ ≼ CsumInvalid) => apply: CsumInvalid_included : core.
+
+Global Arguments csumR {_} _ _.
 
 (* Functor *)
-Global Instance csum_map_cmra_morphism {A A' B B' : cmra} (f : A → A') (g : B → B') :
+Global Instance csum_map_cmra_morphism {SI : sidx} {A A' B B' : cmra}
+    (f : A → A') (g : B → B') :
   CmraMorphism f → CmraMorphism g → CmraMorphism (csum_map f g).
 Proof.
   split; try apply _.
@@ -378,26 +422,29 @@ Proof.
   - intros [xa|ya|] [xb|yb|]=>//=; by rewrite cmra_morphism_op.
 Qed.
 
-Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
+Program Definition csumRF {SI : sidx} (Fa Fb : rFunctor) : rFunctor := {|
   rFunctor_car A _ B _ := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
-  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := csumO_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
+    csumO_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
 |}.
 Next Obligation.
-  by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumO_map_ne; try apply rFunctor_map_ne.
+  intros ? Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg;
+    by apply csumO_map_ne; try apply rFunctor_map_ne.
 Qed.
 Next Obligation.
-  intros Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x).
+  intros ? Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x).
   apply csum_map_ext=>y; apply rFunctor_map_id.
 Qed.
 Next Obligation.
-  intros Fa Fb A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -csum_map_compose.
+  intros ? Fa Fb A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x.
+  rewrite /= -csum_map_compose.
   apply csum_map_ext=>y; apply rFunctor_map_compose.
 Qed.
 
-Global Instance csumRF_contractive Fa Fb :
+Global Instance csumRF_contractive {SI : sidx} Fa Fb :
   rFunctorContractive Fa → rFunctorContractive Fb →
   rFunctorContractive (csumRF Fa Fb).
 Proof.
-  intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
+  intros ??? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
   by apply csumO_map_ne; try apply rFunctor_map_contractive.
 Qed.