CHANGELOG.md

@@ -38,6 +38,7 @@ Coq 8.13 is no longer supported.
     use the tactic `dist_later_intro`/`dist_later_fin_intro` to introduce it.
   (by Michael Sammler, Lennard Gäher, and Simon Spies).
 * Add `max_Z` and `mono_Z` cameras.
+* Add `dfrac_valid`.
 
 **Changes in `bi`:**
 
@@ -75,6 +76,24 @@ Coq 8.13 is no longer supported.
   - Add some `apply bi.entails_wand`/`apply bi.wand_entails` to 'convert'
     between the old and new way of interpreting `P -∗ Q`.
 * Add `auto` hint to introduce the BI version of `↔`.
+* Change `big_sepM2_alt` to use `dom m1 = dom2 m2` instead of
+  `∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)`. The old lemma is still
+  available as `big_sepM2_alt_lookup`.
+* Overhaul `Fractional`/`AsFractional`:
+  - Remove `AsFractional → Fractional` instance.
+  - No longer use `AsFractional P Φ q` backwards, from `Φ` and `q` to `P` -- just
+    use `Φ q` instead.
+  - Remove multiplication instances (that also go from `AsFractional` to
+    `Fractional`, making it very hard to reason about search termination).
+  - Rewrite `frame_fractional` lemma using the new `FrameFractionalQp` typeclass
+    for `Qp` reasoning.
+  - Change statements of `fractional_split`, `fractional_half`, and
+    `fractional_merge` to avoid using `AsFractional` backwards, and only keep
+    the bi-directional versions (remove `fractional_split_1`,
+    `fractional_split_2`, `fractional_half_1`, `fractional_half_2`).
+    `iDestruct`/`iCombine`/`iSplitL`/`iSplitR` should be used instead.
+* Add missing transitivity, symmetry and reflexivity lemmas about the `↔`, `→`,
+  `-∗` and `∗-∗` connectives. (by Ike Mulder)
 
 **Changes in `proofmode`:**
 
@@ -104,6 +123,9 @@ Coq 8.13 is no longer supported.
   statement involves `let`.
 * Remove `string_to_ident`; use `string_to_ident_cps` instead which is in CPS
   form and hence does not require awful hacks.
+* The `iFrame` tactic now removes some conjunctions and disjunctions with `False`,
+  since additional `MakeOr` and `MakeAnd` instances were provided. If you use these
+  classes, their results may have become more concise.
 
 **Changes in `base_logic`:**
 
@@ -119,7 +141,10 @@ Coq 8.13 is no longer supported.
 * Refactor soundness lemmas: `bupd_plain_soundness` → `bupd_soundness`,
   `soundness` → `laterN_soundness` + `pure_soundness`; removed
   `consistency_modal`.
-* Strengthen `cmra_valid_elim` to `✓ a ⊢ ⌜ ✓{0} a ⌝`; make `discrete_valid` a derived law.
+* Strengthen `cmra_valid_elim` to `✓ a ⊢ ⌜ ✓{0} a ⌝`; make `discrete_valid` a
+  derived law.
+* Remove `frac_validI`. Instead, move to the pure context (with `%` in the proof
+  mode or `uPred.discrete_valid` in manual proofs) and use `frac_valid`.
 
 **Changes in `heap_lang`:**
 
@@ -148,6 +173,8 @@ s/\bloc_add(_assoc|_0|_inj|)\b/Loc.add\1/g
 s/\bfresh_locs(_fresh|)\b/Loc.fresh\1/g
 # unseal
 s/\bMonPred\.unseal\b/monPred\.unseal/g
+# big op
+s/\bbig_sepM2_alt\b/big_sepM2_alt_lookup/g
 EOF
 ```
 
@@ -432,6 +459,8 @@ everyone involved!
   propositions that want to support framing are expected to register an
   appropriate instance themselves. HeapLang and gen_heap `↦` still support
   framing, but the other fractional propositions in Iris do not.
+* Strenghten the `Persistent`/`Affine`/`Timeless` results for big ops. Add a `'`
+  to the name of the weaker results, which remain to be used as instances.
 
 **Changes in `heap_lang`:**
 

README.md

@@ -33,7 +33,8 @@ This version is known to compile with:
  - Coq 8.15.2 / 8.16.1 / 8.17.0
  - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
 
-Generally we always aim to support at least the last two stable Coq releases.
+Generally we always aim to support the last two stable Coq releases. Support for
+older versions will be dropped when it is convenient.
 
 If you need to work with older versions of Coq, you can check out the
 [tags](https://gitlab.mpi-sws.org/iris/iris/-/tags) for old Iris releases that

coq-iris.opam

@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.15" & < "8.18~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2023-05-30.0.82cf79ba") | (= "dev") }
+  "coq-stdpp" { (= "dev.2023-06-01.0.d1254759") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]

iris/algebra/big_op.v

@@ -223,6 +223,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 :
@@ -457,6 +469,22 @@ Section gmap.
   Proof.
     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.
 
 Lemma big_opM_sep_zip_with `{Countable K} {A B C}
@@ -597,6 +625,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) :
@@ -701,6 +745,22 @@ Section gmultiset.
   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_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 *)

iris/algebra/dfrac.v

@@ -104,6 +104,14 @@ Section dfrac.
     | DfracBoth q, DfracBoth q' => DfracBoth (q + q')
     end.
 
+  Lemma dfrac_valid dq :
+    ✓ dq ↔ match dq with
+           | DfracOwn q => q ≤ 1
+           | DfracDiscarded => True
+           | DfracBoth q => q < 1
+           end%Qp.
+  Proof. done. Qed.
+
   Lemma dfrac_op_own q p : DfracOwn p ⋅ DfracOwn q = DfracOwn (p + q).
   Proof. done. Qed.
 

iris/base_logic/algebra.v

@@ -23,9 +23,6 @@ Section upred.
     ✓ g ⊣⊢ ∀ i, ✓ g i.
   Proof. by uPred.unseal. Qed.
 
-  Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1⌝%Qp.
-  Proof. rewrite uPred.discrete_valid frac_valid //. Qed.
-
   Section gmap_ofe.
     Context `{Countable K} {A : ofe}.
     Implicit Types m : gmap K A.
@@ -112,6 +109,27 @@ Section upred.
 
     Lemma to_agree_uninjI x : ✓ x ⊢ ∃ a, to_agree a ≡ x.
     Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
+
+    (** Derived lemma: If two [x y : agree O] compose to some [to_agree a],
+      they are internally equal, and also equal to the [to_agree a].
+
+      Empirically, [x ⋅ y ≡ to_agree a] appears often when agreement comes up
+      in CMRA validity terms, especially when [view]s are involved. The desired
+      simplification [x ≡ y ∧ y ≡ to_agree a] is also not straightforward to
+      derive, so we have a special lemma to handle this common case. *)
+    Lemma agree_op_equiv_to_agreeI x y a :
+      x ⋅ y ≡ to_agree a ⊢ x ≡ y ∧ y ≡ to_agree a.
+    Proof.
+      assert (x ⋅ y ≡ to_agree a ⊢ x ≡ y) as Hxy_equiv.
+      { rewrite -(agree_validI x y) internal_eq_sym.
+        apply: (internal_eq_rewrite' _ _ (λ o, ✓ o)%I); first done.
+        rewrite -to_agree_validI. apply bi.True_intro. }
+      apply bi.and_intro; first done.
+      rewrite -{1}(idemp bi_and (_ ≡ _)%I) {1}Hxy_equiv. apply bi.impl_elim_l'.
+      apply: (internal_eq_rewrite' _ _
+        (λ y', x ⋅ y' ≡ to_agree a → y' ≡ to_agree a)%I); [solve_proper|done|].
+      rewrite agree_idemp. apply bi.impl_refl.
+    Qed.
   End agree.
 
   Section csum_ofe.
@@ -225,6 +243,9 @@ Section upred.
     Proof.
       by rewrite auth_auth_dfrac_validI bi.pure_True // left_id.
     Qed.
+    Lemma auth_auth_dfrac_op_validI dq1 dq2 a1 a2 :
+      ✓ (●{dq1} a1 ⋅ ●{dq2} a2) ⊣⊢ ✓ (dq1 ⋅ dq2) ∧ (a1 ≡ a2) ∧ ✓ a1.
+    Proof. uPred.unseal; split => n x _. apply auth_auth_dfrac_op_validN. Qed.
 
     Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢ ✓ a.
     Proof.

iris/base_logic/lib/cancelable_invariants.v

@@ -47,7 +47,7 @@ Section proofs.
   Proof. split; [done|]. apply _. Qed.
 
   Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ⌜q1 + q2 ≤ 1⌝%Qp.
-  Proof. rewrite -frac_validI. apply (own_valid_2 γ q1 q2). Qed.
+  Proof. rewrite -frac_valid -uPred.discrete_valid. apply (own_valid_2 γ q1 q2). Qed.
 
   Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
   Proof.

iris/base_logic/lib/gen_heap.v

@@ -49,10 +49,10 @@ building abstractions, then one can gradually assign more ghost information to a
 location instead of having to do all of this at once. We use namespaces so that
 these can be matched up with the invariant namespaces. *)
 
-(** To implement this mechanism, we use three resource algebras:
+(** To implement this mechanism, we use three pieces of ghost state:
 
-- A [gmap_view L V], which keeps track of the values of locations.
-- A [gmap_view L gname], which keeps track of the meta information of
+- A [ghost_map L V], which keeps track of the values of locations.
+- A [ghost_map L gname], which keeps track of the meta information of
   locations. More specifically, this RA introduces an indirection: it keeps
   track of a ghost name for each location.
 - The ghost names in the aforementioned authoritative RA refer to namespace maps
@@ -188,9 +188,9 @@ Section gen_heap.
   Proof. rewrite mapsto_unseal. apply ghost_map_elem_persist. Qed.
 
   (** Framing support *)
-  Global Instance frame_mapsto p l v q1 q2 RES :
-    FrameFractionalHyps p (l ↦{#q1} v) (λ q, l ↦{#q} v)%I RES q1 q2 →
-    Frame p (l ↦{#q1} v) (l ↦{#q2} v) RES | 5.
+  Global Instance frame_mapsto p l v q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (l ↦{#q1} v) (l ↦{#q2} v) (l ↦{#q} v) | 5.
   Proof. apply: frame_fractional. Qed.
 
   (** General properties of [meta] and [meta_token] *)

iris/base_logic/lib/ghost_var.v

@@ -113,9 +113,9 @@ Section lemmas.
   Proof. iApply ghost_var_update_2. apply Qp.half_half. Qed.
 
   (** Framing support *)
-  Global Instance frame_ghost_var p γ a q1 q2 RES :
-    FrameFractionalHyps p (ghost_var γ q1 a) (λ q, ghost_var γ q a)%I RES q1 q2 →
-    Frame p (ghost_var γ q1 a) (ghost_var γ q2 a) RES | 5.
+  Global Instance frame_ghost_var p γ a q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (ghost_var γ q1 a) (ghost_var γ q2 a) (ghost_var γ q a) | 5.
   Proof. apply: frame_fractional. Qed.
 
 End lemmas.

iris/base_logic/lib/mono_nat.v

@@ -101,13 +101,22 @@ Section mono_nat.
     ⊢ |==> mono_nat_lb_own γ 0.
   Proof. unseal. iApply own_unit. Qed.
 
-  Lemma mono_nat_own_alloc n :
-    ⊢ |==> ∃ γ, mono_nat_auth_own γ 1 n ∗ mono_nat_lb_own γ n.
+  Lemma mono_nat_own_alloc_strong P n :
+    pred_infinite P →
+    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ mono_nat_auth_own γ 1 n ∗ mono_nat_lb_own γ n.
   Proof.
-    unseal. iMod (own_alloc (●MN n ⋅ ◯MN n)) as (γ) "[??]".
+    unseal. intros.
+    iMod (own_alloc_strong (●MN n ⋅ ◯MN n) P) as (γ) "[% [??]]"; first done.
     { apply mono_nat_both_valid; auto. }
     auto with iFrame.
   Qed.
+  Lemma mono_nat_own_alloc n :
+    ⊢ |==> ∃ γ, mono_nat_auth_own γ 1 n ∗ mono_nat_lb_own γ n.
+  Proof.
+    iMod (mono_nat_own_alloc_strong (λ _, True) n) as (γ) "[_ ?]".
+    - by apply pred_infinite_True.
+    - eauto.
+  Qed.
 
   Lemma mono_nat_own_update {γ n} n' :
     n ≤ n' →

iris/base_logic/lib/own.v

@@ -376,8 +376,9 @@ Section proofmode_instances.
   Proof. intros. by rewrite /FromSep -own_op -is_op. Qed.
   (* TODO: Improve this instance with generic own simplification machinery
   once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
+  (* Cost > 50 to give priority to [combine_sep_as_fractional]. *)
   Global Instance combine_sep_as_own γ a b1 b2 :
-    IsOp a b1 b2 → CombineSepAs (own γ b1) (own γ b2) (own γ a).
+    IsOp a b1 b2 → CombineSepAs (own γ b1) (own γ b2) (own γ a) | 60.
   Proof. intros. by rewrite /CombineSepAs -own_op -is_op. Qed.
   (* TODO: Improve this instance with generic own validity simplification
   machinery once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)

iris/base_logic/proofmode.v

@@ -26,9 +26,10 @@ Section class_instances.
   Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
   (* TODO: Improve this instance with generic own simplification machinery
   once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
+  (* Cost > 50 to give priority to [combine_sep_as_fractional]. *)
   Global Instance combine_sep_as_ownM (a b1 b2 : M) :
     IsOp a b1 b2 →
-    CombineSepAs (uPred_ownM b1) (uPred_ownM b2) (uPred_ownM a).
+    CombineSepAs (uPred_ownM b1) (uPred_ownM b2) (uPred_ownM a) | 60.
   Proof. intros. by rewrite /CombineSepAs -ownM_op -is_op. Qed.
   (* TODO: Improve this instance with generic own validity simplification
   machinery once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)

iris/bi/big_op.v

@@ -56,8 +56,7 @@ Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" :=
 
 Local Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
     (Φ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : PROP :=
-  (⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝ ∧
-   [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2)%I.
+  ⌜ dom m1 = dom m2 ⌝ ∧ [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2.
 Local Definition big_sepM2_aux : seal (@big_sepM2_def). Proof. by eexists. Qed.
 Definition big_sepM2 := big_sepM2_aux.(unseal).
 Global Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
@@ -138,9 +137,13 @@ Section sep_list.
   Global Instance big_sepL_nil_persistent Φ :
     Persistent ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
-  Global Instance big_sepL_persistent Φ l :
+  Lemma big_sepL_persistent Φ l :
+    (∀ k x, l !! k = Some x → Persistent (Φ k x)) →
+    Persistent ([∗ list] k↦x ∈ l, Φ k x).
+  Proof. apply big_opL_closed; apply _. Qed.
+  Global Instance big_sepL_persistent' Φ l :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∗ list] k↦x ∈ l, Φ k x).
-  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Proof. intros; apply big_sepL_persistent, _. Qed.
   Global Instance big_sepL_persistent_id Ps :
     TCForall Persistent Ps → Persistent ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
@@ -148,18 +151,27 @@ Section sep_list.
   Global Instance big_sepL_nil_affine Φ :
     Affine ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
-  Global Instance big_sepL_affine Φ l :
+  Lemma big_sepL_affine Φ l :
+    (∀ k x, l !! k = Some x → Affine (Φ k x)) →
+    Affine ([∗ list] k↦x ∈ l, Φ k x).
+  Proof. apply big_opL_closed; apply _. Qed.
+  Global Instance big_sepL_affine' Φ l :
     (∀ k x, Affine (Φ k x)) → Affine ([∗ list] k↦x ∈ l, Φ k x).
-  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Proof. intros. apply big_sepL_affine, _. Qed.
   Global Instance big_sepL_affine_id Ps : TCForall Affine Ps → Affine ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
 
   Global Instance big_sepL_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
     Timeless ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
-  Global Instance big_sepL_timeless `{!Timeless (emp%I : PROP)} Φ l :
-    (∀ k x, Timeless (Φ k x)) → Timeless ([∗ list] k↦x ∈ l, Φ k x).
-  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Lemma big_sepL_timeless `{!Timeless (emp%I : PROP)} Φ l :
+    (∀ k x, l !! k = Some x → Timeless (Φ k x)) →
+    Timeless ([∗ list] k↦x ∈ l, Φ k x).
+  Proof. apply big_opL_closed; apply _. Qed.
+  Global Instance big_sepL_timeless' `{!Timeless (emp%I : PROP)} Φ l :
+    (∀ k x, Timeless (Φ k x)) →
+    Timeless ([∗ list] k↦x ∈ l, Φ k x).
+  Proof. intros. apply big_sepL_timeless, _. Qed.
   Global Instance big_sepL_timeless_id `{!Timeless (emp%I : PROP)} Ps :
     TCForall Timeless Ps → Timeless ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
@@ -600,29 +612,53 @@ Section sep_list2.
            (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
   Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_proper; intros; apply Hf. Qed.
 
+  (** Shows that some property [P] is closed under [big_sepL2]. Examples of [P]
+  are [Persistent], [Affine], [Timeless]. *)
+  Lemma big_sepL2_closed (P : PROP → Prop) Φ l1 l2 :
+    P emp%I → P False%I →
+    (∀ Q1 Q2, P Q1 → P Q2 → P (Q1 ∗ Q2)%I) →
+    (∀ k x1 x2, l1 !! k = Some x1 → l2 !! k = Some x2 → P (Φ k x1 x2)) →
+    P ([∗ list] k↦x1;x2 ∈ l1; l2, Φ k x1 x2)%I.
+  Proof.
+    intros ?? Hsep. revert l2 Φ. induction l1 as [|x1 l1 IH]=> -[|x2 l2] Φ HΦ //=.
+    apply Hsep; first by auto. apply IH=> k. apply (HΦ (S k)).
+  Qed.
+
   Global Instance big_sepL2_nil_persistent Φ :
     Persistent ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
   Proof. simpl; apply _. Qed.
-  Global Instance big_sepL2_persistent Φ l1 l2 :
+  Lemma big_sepL2_persistent Φ l1 l2 :
+    (∀ k x1 x2, l1 !! k = Some x1 → l2 !! k = Some x2 → Persistent (Φ k x1 x2)) →
+    Persistent ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
+  Proof. apply big_sepL2_closed; apply _. Qed.
+  Global Instance big_sepL2_persistent' Φ l1 l2 :
     (∀ k x1 x2, Persistent (Φ k x1 x2)) →
     Persistent ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
-  Proof. rewrite big_sepL2_alt. apply _. Qed.
+  Proof. intros; apply big_sepL2_persistent, _. Qed.
 
   Global Instance big_sepL2_nil_affine Φ :
     Affine ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
   Proof. simpl; apply _. Qed.
-  Global Instance big_sepL2_affine Φ l1 l2 :
+  Lemma big_sepL2_affine Φ l1 l2 :
+    (∀ k x1 x2, l1 !! k = Some x1 → l2 !! k = Some x2 → Affine (Φ k x1 x2)) →
+    Affine ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
+  Proof. apply big_sepL2_closed; apply _. Qed.
+  Global Instance big_sepL2_affine' Φ l1 l2 :
     (∀ k x1 x2, Affine (Φ k x1 x2)) →
     Affine ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
-  Proof. rewrite big_sepL2_alt. apply _. Qed.
+  Proof. intros; apply big_sepL2_affine, _. Qed.
 
   Global Instance big_sepL2_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
     Timeless ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
   Proof. simpl; apply _. Qed.
-  Global Instance big_sepL2_timeless `{!Timeless (emp%I : PROP)} Φ l1 l2 :
+  Lemma big_sepL2_timeless `{!Timeless (emp%I : PROP)} Φ l1 l2 :
+    (∀ k x1 x2, l1 !! k = Some x1 → l2 !! k = Some x2 → Timeless (Φ k x1 x2)) →
+    Timeless ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
+  Proof. apply big_sepL2_closed; apply _. Qed.
+  Global Instance big_sepL2_timeless' `{!Timeless (emp%I : PROP)} Φ l1 l2 :
     (∀ k x1 x2, Timeless (Φ k x1 x2)) →
     Timeless ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
-  Proof. rewrite big_sepL2_alt. apply _. Qed.
+  Proof. intros; apply big_sepL2_timeless, _. Qed.
 
   Lemma big_sepL2_insert_acc Φ l1 l2 i x1 x2 :
     l1 !! i = Some x1 → l2 !! i = Some x2 →
@@ -1026,23 +1062,34 @@ Section and_list.
   Global Instance big_andL_nil_absorbing Φ :
     Absorbing ([∧ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
-  Global Instance big_andL_absorbing Φ l :
+  Lemma big_andL_absorbing Φ l :
+    (∀ k x, l !! k = Some x → Absorbing (Φ k x)) →
+    Absorbing ([∧ list] k↦x ∈ l, Φ k x).
+  Proof. apply big_opL_closed; apply _. Qed.
+  Global Instance big_andL_absorbing' Φ l :
     (∀ k x, Absorbing (Φ k x)) → Absorbing ([∧ list] k↦x ∈ l, Φ k x).
-  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Proof. intros; apply big_andL_absorbing, _. Qed.
 
   Global Instance big_andL_nil_persistent Φ :
     Persistent ([∧ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
-  Global Instance big_andL_persistent Φ l :
+  Lemma big_andL_persistent Φ l :
+    (∀ k x, l !! k = Some x → Persistent (Φ k x)) → Persistent ([∧ list] k↦x ∈ l, Φ k x).
+  Proof. apply big_opL_closed; apply _. Qed.
+  Global Instance big_andL_persistent' Φ l :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∧ list] k↦x ∈ l, Φ k x).
-  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Proof. intros; apply big_andL_persistent, _. Qed.
 
   Global Instance big_andL_nil_timeless Φ :
     Timeless ([∧ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
-  Global Instance big_andL_timeless Φ l :
+  Lemma big_andL_timeless Φ l :
+    (∀ k x, l !! k = Some x → Timeless (Φ k x)) →
+    Timeless ([∧ list] k↦x ∈ l, Φ k x).
+  Proof. apply big_opL_closed; apply _. Qed.
+  Global Instance big_andL_timeless' Φ l :
     (∀ k x, Timeless (Φ k x)) → Timeless ([∧ list] k↦x ∈ l, Φ k x).
-  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Proof. intros; apply big_andL_timeless, _. Qed.
 
   Lemma big_andL_lookup Φ l i x :
     l !! i = Some x → ([∧ list] k↦y ∈ l, Φ k y) ⊢ Φ i x.
@@ -1186,15 +1233,23 @@ Section or_list.
     Persistent ([∨ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
   Global Instance big_orL_persistent Φ l :
+    (∀ k x, l !! k = Some x → Persistent (Φ k x)) →
+    Persistent ([∨ list] k↦x ∈ l, Φ k x).
+  Proof. apply big_opL_closed; apply _. Qed.
+  Global Instance big_orL_persistent' Φ l :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∨ list] k↦x ∈ l, Φ k x).
-  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Proof. intros; apply big_orL_persistent, _. Qed.
 
   Global Instance big_orL_nil_timeless Φ :
     Timeless ([∨ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
   Global Instance big_orL_timeless Φ l :
+    (∀ k x, l !! k = Some x → Timeless (Φ k x)) →
+    Timeless ([∨ list] k↦x ∈ l, Φ k x).
+  Proof. apply big_opL_closed; apply _. Qed.
+  Global Instance big_orL_timeless' Φ l :
     (∀ k x, Timeless (Φ k x)) → Timeless ([∨ list] k↦x ∈ l, Φ k x).
-  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Proof. intros; apply big_orL_timeless, _. Qed.
 
   Lemma big_orL_intro Φ l i x :
     l !! i = Some x → Φ i x ⊢ ([∨ list] k↦y ∈ l, Φ k y).
@@ -1301,32 +1356,35 @@ Section sep_map.
   Global Instance big_sepM_empty_persistent Φ :
     Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite big_opM_empty. apply _. Qed.
-  Global Instance big_sepM_persistent Φ m :
+  Lemma big_sepM_persistent Φ m :
+    (∀ k x, m !! k = Some x → Persistent (Φ k x)) →
+    Persistent ([∗ map] k↦x ∈ m, Φ k x).
+  Proof. apply big_opM_closed; apply _. Qed.
+  Global Instance big_sepM_persistent' Φ m :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x).
-  Proof.
-    induction m using map_ind;
-      [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
-  Qed.
+  Proof. intros; apply big_sepM_persistent, _. Qed.
 
   Global Instance big_sepM_empty_affine Φ :
     Affine ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite big_opM_empty. apply _. Qed.
-  Global Instance big_sepM_affine Φ m :
+  Lemma big_sepM_affine Φ m :
+    (∀ k x, m !! k = Some x → Affine (Φ k x)) →
+    Affine ([∗ map] k↦x ∈ m, Φ k x).
+  Proof. apply big_opM_closed; apply _. Qed.
+  Global Instance big_sepM_affine' Φ m :
     (∀ k x, Affine (Φ k x)) → Affine ([∗ map] k↦x ∈ m, Φ k x).
-  Proof.
-    induction m using map_ind;
-      [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
-  Qed.
+  Proof. intros; apply big_sepM_affine, _. Qed.
 
   Global Instance big_sepM_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
     Timeless ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite big_opM_empty. apply _. Qed.
-  Global Instance big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
+  Lemma big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
+    (∀ k x, m !! k = Some x → Timeless (Φ k x)) →
+    Timeless ([∗ map] k↦x ∈ m, Φ k x).
+  Proof. apply big_opM_closed; apply _. Qed.
+  Global Instance big_sepM_timeless' `{!Timeless (emp%I : PROP)} Φ m :
     (∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x).
-  Proof.
-    induction m using map_ind;
-      [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
-  Qed.
+  Proof. intros; apply big_sepM_timeless, _. Qed.
 
   (* We place the [Affine] instance after [m1] and [m2], so that
      manually instantiating [m1] or [m2] in [iApply] does not also
@@ -1728,22 +1786,24 @@ Section and_map.
   Global Instance big_andM_empty_persistent Φ :
     Persistent ([∧ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite big_opM_empty. apply _. Qed.
-  Global Instance big_andM_persistent Φ m :
+  Lemma big_andM_persistent Φ m :
+    (∀ k x, m !! k = Some x → Persistent (Φ k x)) →
+    Persistent ([∧ map] k↦x ∈ m, Φ k x).
+  Proof. apply big_opM_closed; apply _. Qed.
+  Global Instance big_andM_persistent' Φ m :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∧ map] k↦x ∈ m, Φ k x).
-  Proof.
-    induction m using map_ind;
-      [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
-  Qed.
+  Proof. intros; apply big_andM_persistent, _. Qed.
 
   Global Instance big_andM_empty_timeless Φ :
     Timeless ([∧ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite big_opM_empty. apply _. Qed.
-  Global Instance big_andM_timeless Φ m :
+  Lemma big_andM_timeless Φ m :
+    (∀ k x, m !! k = Some x → Timeless (Φ k x)) →
+    Timeless ([∧ map] k↦x ∈ m, Φ k x).
+  Proof. apply big_opM_closed; apply _. Qed.
+  Global Instance big_andM_timeless' Φ m :
     (∀ k x, Timeless (Φ k x)) → Timeless ([∧ map] k↦x ∈ m, Φ k x).
-  Proof.
-    induction m using map_ind;
-      [rewrite big_opM_empty|rewrite big_opM_insert //]; apply _.
-  Qed.
+  Proof. intros; apply big_andM_timeless, _. Qed.
 
   Lemma big_andM_subseteq Φ m1 m2 :
     m2 ⊆ m1 → ([∧ map] k ↦ x ∈ m1, Φ k x) ⊢ [∧ map] k ↦ x ∈ m2, Φ k x.
@@ -1902,26 +1962,28 @@ End and_map.
 (** ** Big ops over two maps *)
 Lemma big_sepM2_alt `{Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
   ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊣⊢
-  ⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝ ∧
-  [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2.
+  ⌜ dom m1 = dom m2 ⌝ ∧ [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2.
 Proof. by rewrite big_sepM2_unseal. Qed.
 
 Section map2.
   Context `{Countable K} {A B : Type}.
   Implicit Types Φ Ψ : K → A → B → PROP.
 
+  Lemma big_sepM2_alt_lookup (Φ : K → A → B → PROP) m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊣⊢
+    ⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝ ∧
+    [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2.
+  Proof. rewrite big_sepM2_alt set_eq. by setoid_rewrite elem_of_dom. Qed.
+
   Lemma big_sepM2_lookup_iff Φ m1 m2 :
     ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊢
     ⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝.
-  Proof. by rewrite big_sepM2_alt and_elim_l. Qed.
+  Proof. by rewrite big_sepM2_alt_lookup and_elim_l. Qed.
 
   Lemma big_sepM2_dom Φ m1 m2 :
     ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊢
     ⌜ dom m1 = dom m2 ⌝.
-  Proof.
-    rewrite big_sepM2_lookup_iff. apply pure_mono=>Hm.
-    apply set_eq=> k. by rewrite !elem_of_dom.
-  Qed.
+  Proof. by rewrite big_sepM2_alt and_elim_l. Qed.
 
   Lemma big_sepM2_flip Φ m1 m2 :
     ([∗ map] k↦y1;y2 ∈ m2; m1, Φ k y2 y1) ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2).
@@ -1934,11 +1996,36 @@ Section map2.
   Lemma big_sepM2_empty Φ : ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2) ⊣⊢ emp.
   Proof.
     rewrite big_sepM2_alt map_zip_with_empty big_sepM_empty pure_True ?left_id //.
-    intros k. rewrite !lookup_empty; split; by inversion 1.
   Qed.
   Lemma big_sepM2_empty' P `{!Affine P} Φ : P ⊢ [∗ map] k↦y1;y2 ∈ ∅;∅, Φ k y1 y2.
   Proof. rewrite big_sepM2_empty. apply: affine. Qed.
 
+  Lemma big_sepM2_empty_l m1 Φ : ([∗ map] k↦y1;y2 ∈ m1; ∅, Φ k y1 y2) ⊢ ⌜m1 = ∅⌝.
+  Proof.
+    rewrite big_sepM2_dom dom_empty_L.
+    apply pure_mono, dom_empty_iff_L.
+  Qed.
+  Lemma big_sepM2_empty_r m2 Φ : ([∗ map] k↦y1;y2 ∈ ∅; m2, Φ k y1 y2) ⊢ ⌜m2 = ∅⌝.
+  Proof.
+    rewrite big_sepM2_dom dom_empty_L.
+    apply pure_mono=>?. eapply dom_empty_iff_L. eauto.
+  Qed.
+
+  Lemma big_sepM2_insert Φ m1 m2 i x1 x2 :
+    m1 !! i = None → m2 !! i = None →
+    ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
+    ⊣⊢ Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2.
+  Proof.
+    intros Hm1 Hm2. rewrite !big_sepM2_alt -map_insert_zip_with.
+    rewrite big_sepM_insert;
+      last by rewrite map_lookup_zip_with Hm1.
+    rewrite !persistent_and_affinely_sep_l /=.
+    rewrite sep_assoc (sep_comm _ (Φ _ _ _)) -sep_assoc.
+    repeat apply sep_proper=>//.
+    apply affinely_proper, pure_proper. rewrite !dom_insert_L.
+    apply not_elem_of_dom in Hm1. apply not_elem_of_dom in Hm2. set_solver.
+  Qed.
+
   (** The lemmas [big_sepM2_mono], [big_sepM2_ne] and [big_sepM2_proper] are more
   generic than the instances as they also give [mi !! k = Some yi] in the premise. *)
   Lemma big_sepM2_mono Φ Ψ m1 m2 :
@@ -1980,11 +2067,7 @@ Section map2.
     ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2) ⊣⊢ [∗ map] k ↦ y1;y2 ∈ m1';m2', Ψ k y1 y2.
   Proof.
     intros Hm1 Hm2 Hf. rewrite !big_sepM2_alt. f_equiv.
-    { f_equiv; split; intros Hm k.
-      - trans (is_Some (m1 !! k)); [symmetry; apply is_Some_proper; by f_equiv|].
-        rewrite Hm. apply is_Some_proper; by f_equiv.
-      - trans (is_Some (m1' !! k)); [apply is_Some_proper; by f_equiv|].
-        rewrite Hm. symmetry. apply is_Some_proper; by f_equiv. }
+    { by rewrite Hm1 Hm2. }
     apply big_opM_proper_2; [by f_equiv|].
     intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some
       (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some [??]; naive_solver.
@@ -2004,62 +2087,58 @@ Section map2.
       ==> (=) ==> (=) ==> (⊣⊢)) (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
   Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_proper; intros; apply Hf. Qed.
 
+  (** Shows that some property [P] is closed under [big_sepM2]. Examples of [P]
+  are [Persistent], [Affine], [Timeless]. *)
+  Lemma big_sepM2_closed (P : PROP → Prop) Φ m1 m2 :
+    Proper ((≡) ==> iff) P →
+    P emp%I → P False%I →
+    (∀ Q1 Q2, P Q1 → P Q2 → P (Q1 ∗ Q2)%I) →
+    (∀ k x1 x2, m1 !! k = Some x1 → m2 !! k = Some x2 → P (Φ k x1 x2)) →
+    P ([∗ map] k↦x1;x2 ∈ m1; m2, Φ k x1 x2)%I.
+  Proof.
+    intros ??? Hsep HΦ.
+    rewrite big_sepM2_alt. destruct (decide (dom m1 = dom m2)).
+    - rewrite pure_True // left_id. apply big_opM_closed; [done..|].
+      intros k [x1 x2] Hk. rewrite map_lookup_zip_with in Hk.
+      simplify_option_eq; auto.
+    - by rewrite pure_False // left_absorb.
+  Qed.
+
   Global Instance big_sepM2_empty_persistent Φ :
     Persistent ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
   Proof. rewrite big_sepM2_empty. apply _. Qed.
-  Global Instance big_sepM2_persistent Φ m1 m2 :
+  Lemma big_sepM2_persistent Φ m1 m2 :
+    (∀ k x1 x2, m1 !! k = Some x1 → m2 !! k = Some x2 → Persistent (Φ k x1 x2)) →
+    Persistent ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
+  Proof. apply big_sepM2_closed; apply _. Qed.
+  Global Instance big_sepM2_persistent' Φ m1 m2 :
     (∀ k x1 x2, Persistent (Φ k x1 x2)) →
     Persistent ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
-  Proof. rewrite big_sepM2_alt. apply _. Qed.
+  Proof. intros; apply big_sepM2_persistent, _. Qed.
 
   Global Instance big_sepM2_empty_affine Φ :
     Affine ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
   Proof. rewrite big_sepM2_empty. apply _. Qed.
-  Global Instance big_sepM2_affine Φ m1 m2 :
+  Lemma big_sepM2_affine Φ m1 m2 :
+    (∀ k x1 x2, m1 !! k = Some x1 → m2 !! k = Some x2 → Affine (Φ k x1 x2)) →
+    Affine ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
+  Proof. apply big_sepM2_closed; apply _. Qed.
+  Global Instance big_sepM2_affine' Φ m1 m2 :
     (∀ k x1 x2, Affine (Φ k x1 x2)) →
     Affine ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
-  Proof. rewrite big_sepM2_alt. apply _. Qed.
+  Proof. intros; apply big_sepM2_affine, _. Qed.
 
   Global Instance big_sepM2_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
     Timeless ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
   Proof. rewrite big_sepM2_alt map_zip_with_empty. apply _. Qed.
-  Global Instance big_sepM2_timeless `{!Timeless (emp%I : PROP)} Φ m1 m2 :
+  Lemma big_sepM2_timeless `{!Timeless (emp%I : PROP)} Φ m1 m2 :
+    (∀ k x1 x2, m1 !! k = Some x1 → m2 !! k = Some x2 → Timeless (Φ k x1 x2)) →
+    Timeless ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
+  Proof. apply big_sepM2_closed; apply _. Qed.
+  Global Instance big_sepM2_timeless' `{!Timeless (emp%I : PROP)} Φ m1 m2 :
     (∀ k x1 x2, Timeless (Φ k x1 x2)) →
     Timeless ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
-  Proof. intros. rewrite big_sepM2_alt. apply _. Qed.
-
-  Lemma big_sepM2_empty_l m1 Φ : ([∗ map] k↦y1;y2 ∈ m1; ∅, Φ k y1 y2) ⊢ ⌜m1 = ∅⌝.
-  Proof.
-    rewrite big_sepM2_dom dom_empty_L.
-    apply pure_mono, dom_empty_iff_L.
-  Qed.
-
-  Lemma big_sepM2_empty_r m2 Φ : ([∗ map] k↦y1;y2 ∈ ∅; m2, Φ k y1 y2) ⊢ ⌜m2 = ∅⌝.
-  Proof.
-    rewrite big_sepM2_dom dom_empty_L.
-    apply pure_mono=>?. eapply dom_empty_iff_L. eauto.
-  Qed.
-
-  Lemma big_sepM2_insert Φ m1 m2 i x1 x2 :
-    m1 !! i = None → m2 !! i = None →
-    ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2)
-    ⊣⊢ Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2.
-  Proof.
-    intros Hm1 Hm2. rewrite !big_sepM2_alt -map_insert_zip_with.
-    rewrite big_sepM_insert;
-      last by rewrite map_lookup_zip_with Hm1.
-    rewrite !persistent_and_affinely_sep_l /=.
-    rewrite sep_assoc (sep_comm _ (Φ _ _ _)) -sep_assoc.
-    repeat apply sep_proper=>//.
-    apply affinely_proper, pure_proper.
-    split.
-    - intros H1 k. destruct (decide (i = k)) as [->|?].
-      + rewrite Hm1 Hm2 //. by split; intros ?; exfalso; eapply is_Some_None.
-      + specialize (H1 k). revert H1. rewrite !lookup_insert_ne //.
-    - intros H1 k. destruct (decide (i = k)) as [->|?].
-      + rewrite !lookup_insert. split; by econstructor.
-      + rewrite !lookup_insert_ne //.
-  Qed.
+  Proof. intros; apply big_sepM2_timeless, _. Qed.
 
   Lemma big_sepM2_delete Φ m1 m2 i x1 x2 :
     m1 !! i = Some x1 → m2 !! i = Some x2 →
@@ -2070,13 +2149,9 @@ Section map2.
     rewrite !persistent_and_affinely_sep_l /=.
     rewrite sep_assoc (sep_comm  (Φ _ _ _)) -sep_assoc.
     apply sep_proper.
-    - apply affinely_proper, pure_proper. split.
-      + intros Hm k. destruct (decide (i = k)) as [->|?].
-        { rewrite !lookup_delete. split; intros []%is_Some_None. }
-        rewrite !lookup_delete_ne //.
-      + intros Hm k. specialize (Hm k). revert Hm. destruct (decide (i = k)) as [->|?].
-        { intros _. rewrite Hx1 Hx2. split; eauto. }
-        rewrite !lookup_delete_ne //.
+    - apply affinely_proper, pure_proper. rewrite !dom_delete_L.
+      apply elem_of_dom_2 in Hx1; apply elem_of_dom_2 in Hx2. set_unfold.
+      apply base.forall_proper=> k. destruct (decide (k = i)); naive_solver.
     - rewrite -map_delete_zip_with.
       apply (big_sepM_delete (λ i xx, Φ i xx.1 xx.2) (map_zip m1 m2) i (x1,x2)).
       by rewrite map_lookup_zip_with Hx1 Hx2.
@@ -2088,11 +2163,11 @@ Section map2.
             (Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2).
   Proof.
     intros Hm1. apply (anti_symm _).
-    - rewrite big_sepM2_alt. apply pure_elim_l=> Hm.
+    - rewrite big_sepM2_alt_lookup. apply pure_elim_l=> Hm.
       assert (is_Some (m2 !! i)) as [x2 Hm2].
       { apply Hm. by econstructor. }
       rewrite -(exist_intro x2).
-      rewrite big_sepM2_alt (big_sepM_delete _ _ i (x1,x2)) /=;
+      rewrite big_sepM2_alt_lookup (big_sepM_delete _ _ i (x1,x2)) /=;
         last by rewrite map_lookup_zip_with Hm1 Hm2.
       rewrite pure_True // left_id.
       f_equiv. apply and_intro.
@@ -2108,12 +2183,12 @@ Section map2.
             (Φ i x1 x2 ∗ [∗ map] k↦y1;y2 ∈ delete i m1;delete i m2, Φ k y1 y2).
   Proof.
     intros Hm2. apply (anti_symm _).
-    - rewrite big_sepM2_alt.
+    - rewrite big_sepM2_alt_lookup.
       apply pure_elim_l=> Hm.
       assert (is_Some (m1 !! i)) as [x1 Hm1].
       { apply Hm. by econstructor. }
       rewrite -(exist_intro x1).
-      rewrite big_sepM2_alt (big_sepM_delete _ _ i (x1,x2)) /=;
+      rewrite big_sepM2_alt_lookup (big_sepM_delete _ _ i (x1,x2)) /=;
         last by rewrite map_lookup_zip_with Hm1 Hm2.
       rewrite pure_True // left_id.
       f_equiv. apply and_intro.
@@ -2156,8 +2231,7 @@ Section map2.
     apply entails_wand, wand_intro_r.
     rewrite !persistent_and_affinely_sep_l /=.
     rewrite (sep_comm  (Φ _ _ _)) -sep_assoc. apply sep_mono.
-    { apply affinely_mono, pure_mono. intros Hm k.
-      rewrite !lookup_insert_is_Some. naive_solver. }
+    { apply affinely_mono, pure_mono. rewrite !dom_insert_L. set_solver. }
     rewrite (big_sepM_insert_2 (λ k xx, Φ k xx.1 xx.2) (map_zip m1 m2) i (x1, x2)).
     rewrite map_insert_zip_with. apply wand_elim_r.
   Qed.
@@ -2208,17 +2282,14 @@ Section map2.
     apply (anti_symm _).
     - apply and_elim_r.
     - rewrite <- (left_id True%I (∧)%I (Φ i x1 x2)).
-      apply and_mono=>//. apply pure_mono=>_ k.
-      rewrite !lookup_insert_is_Some' !lookup_empty -!not_eq_None_Some.
-      naive_solver.
+      apply and_mono=> //. apply pure_mono=> _. set_solver.
   Qed.
 
   Lemma big_sepM2_fst_snd Φ m :
     ([∗ map] k↦y1;y2 ∈ fst <$> m; snd <$> m, Φ k y1 y2) ⊣⊢
     [∗ map] k ↦ xy ∈ m, Φ k (xy.1) (xy.2).
   Proof.
-    rewrite big_sepM2_alt.
-    setoid_rewrite lookup_fmap. setoid_rewrite fmap_is_Some.
+    rewrite big_sepM2_alt. rewrite !dom_fmap_L.
     by rewrite pure_True // True_and map_zip_fst_snd.
   Qed.
 
@@ -2226,10 +2297,7 @@ Section map2.
     ([∗ map] k↦y1;y2 ∈ f <$> m1; g <$> m2, Φ k y1 y2)
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k (f y1) (g y2)).
   Proof.
-    rewrite !big_sepM2_alt. rewrite map_fmap_zip.
-    apply and_proper.
-    - setoid_rewrite lookup_fmap. by setoid_rewrite fmap_is_Some.
-    - by rewrite big_sepM_fmap.
+    rewrite !big_sepM2_alt. by rewrite map_fmap_zip !dom_fmap_L big_sepM_fmap.
   Qed.
 
   Lemma big_sepM2_fmap_l {A'} (f : A → A') (Φ : K → A' → B → PROP) m1 m2 :
@@ -2247,7 +2315,7 @@ Section map2.
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2).
   Proof.
     rewrite !big_sepM2_alt.
-    rewrite -{1}(idemp bi_and ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)⌝%I).
+    rewrite -{1}(idemp bi_and ⌜ dom m1 = dom m2 ⌝%I).
     rewrite -assoc.
     rewrite !persistent_and_affinely_sep_l /=.
     rewrite -assoc. apply sep_proper=>//.
@@ -2282,7 +2350,7 @@ Section map2.
       ([∗ map] k↦y1;y2 ∈ m1;m2, <affine> ⌜φ k y1 y2⌝).
   Proof.
     intros Hdom.
-    rewrite big_sepM2_alt.
+    rewrite big_sepM2_alt_lookup.
     rewrite -big_sepM_affinely_pure_2.
     rewrite affinely_and_r -pure_and. f_equiv. f_equiv=>-Hforall.
     split; first done.
@@ -2318,7 +2386,7 @@ Section map2.
     □ (∀ k x1 x2, ⌜m1 !! k = Some x1⌝ → ⌜m2 !! k = Some x2⌝ → Φ k x1 x2) ⊢
     [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
   Proof.
-    intros. rewrite big_sepM2_alt.
+    intros. rewrite big_sepM2_alt_lookup.
     apply and_intro; [by apply pure_intro|].
     rewrite -big_sepM_intro. f_equiv; f_equiv=> k.
     apply forall_intro=> -[x1 x2]. rewrite (forall_elim x1) (forall_elim x2).
@@ -2337,7 +2405,7 @@ Section map2.
     { apply and_intro; [apply big_sepM2_lookup_iff|].
       apply forall_intro=> k. apply forall_intro=> x1. apply forall_intro=> x2.
       do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply: big_sepM2_lookup. }
-    apply pure_elim_l=> Hdom. rewrite big_sepM2_alt.
+    apply pure_elim_l=> Hdom. rewrite big_sepM2_alt_lookup.
     apply and_intro; [by apply pure_intro|].
     rewrite big_sepM_forall. f_equiv=> k.
     apply forall_intro=> -[x1 x2]. rewrite (forall_elim x1) (forall_elim x2).
@@ -2420,7 +2488,8 @@ Section map2.
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ1 k y1 ∗ Φ2 k y2) ⊣⊢
     ([∗ map] k↦y1 ∈ m1, Φ1 k y1) ∗ ([∗ map] k↦y2 ∈ m2, Φ2 k y2).
   Proof.
-    intros. rewrite -big_sepM_sep_zip // big_sepM2_alt pure_True // left_id //.
+    intros.
+    rewrite -big_sepM_sep_zip // big_sepM2_alt_lookup pure_True // left_id //.
   Qed.
   Lemma big_sepM2_sepM_2 (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
     (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
@@ -2491,11 +2560,7 @@ Lemma big_sepM2_ne_2 `{Countable K} (A B : ofe)
   ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2)%I ≡{n}≡ ([∗ map] k ↦ y1;y2 ∈ m1';m2', Ψ k y1 y2)%I.
 Proof.
   intros Hm1 Hm2 Hf. rewrite !big_sepM2_alt. f_equiv.
-  { f_equiv; split; intros Hm k.
-    - trans (is_Some (m1 !! k)); [symmetry; apply: is_Some_ne; by f_equiv|].
-      rewrite Hm. apply: is_Some_ne; by f_equiv.
-    - trans (is_Some (m1' !! k)); [apply: is_Some_ne; by f_equiv|].
-      rewrite Hm. symmetry. apply: is_Some_ne; by f_equiv. }
+  { by rewrite Hm1 Hm2. }
   apply big_opM_ne_2; [by f_equiv|].
   intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some
     (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some [??]; naive_solver.
@@ -2531,31 +2596,31 @@ Section gset.
   Global Instance big_sepS_empty_persistent Φ :
     Persistent ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite big_opS_empty. apply _. Qed.
-  Global Instance big_sepS_persistent Φ X :
+  Lemma big_sepS_persistent Φ X :
+    (∀ x, x ∈ X → Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
+  Proof. apply big_opS_closed; apply _. Qed.
+  Global Instance big_sepS_persistent' Φ X :
     (∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
-  Proof.
-    induction X using set_ind_L;
-      [rewrite big_opS_empty|rewrite big_opS_insert //]; apply _.
-  Qed.
+  Proof. intros; apply big_sepS_persistent, _. Qed.
 
   Global Instance big_sepS_empty_affine Φ : Affine ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite big_opS_empty. apply _. Qed.
-  Global Instance big_sepS_affine Φ X :
+  Lemma big_sepS_affine Φ X :
+    (∀ x, x ∈ X → Affine (Φ x)) → Affine ([∗ set] x ∈ X, Φ x).
+  Proof. apply big_opS_closed; apply _. Qed.
+  Global Instance big_sepS_affine' Φ X :
     (∀ x, Affine (Φ x)) → Affine ([∗ set] x ∈ X, Φ x).
-  Proof.
-    induction X using set_ind_L;
-      [rewrite big_opS_empty|rewrite big_opS_insert //]; apply _.
-  Qed.
+  Proof. intros; apply big_sepS_affine, _. Qed.
 
   Global Instance big_sepS_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
     Timeless ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite big_opS_empty. apply _. Qed.
-  Global Instance big_sepS_timeless `{!Timeless (emp%I : PROP)} Φ X :
+  Lemma big_sepS_timeless `{!Timeless (emp%I : PROP)} Φ X :
+    (∀ x, x ∈ X → Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
+  Proof. apply big_opS_closed; apply _. Qed.
+  Global Instance big_sepS_timeless' `{!Timeless (emp%I : PROP)} Φ X :
     (∀ x, Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
-  Proof.
-    induction X using set_ind_L;
-      [rewrite big_opS_empty|rewrite big_opS_insert //]; apply _.
-  Qed.
+  Proof. intros; apply big_sepS_timeless, _. Qed.
 
   (* See comment above [big_sepM_subseteq] as for why the [Affine]
      instance is placed late. *)
@@ -2870,31 +2935,31 @@ Section gmultiset.
   Global Instance big_sepMS_empty_persistent Φ :
     Persistent ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite big_opMS_empty. apply _. Qed.
-  Global Instance big_sepMS_persistent Φ X :
+  Lemma big_sepMS_persistent Φ X :
+    (∀ x, x ∈ X → Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
+  Proof. apply big_opMS_closed; apply _. Qed.
+  Global Instance big_sepMS_persistent' Φ X :
     (∀ x, Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
-  Proof.
-    induction X using gmultiset_ind;
-      [rewrite big_opMS_empty|rewrite big_opMS_insert]; apply _.
-  Qed.
+  Proof. intros; apply big_sepMS_persistent, _. Qed.
 
   Global Instance big_sepMS_empty_affine Φ : Affine ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite big_opMS_empty. apply _. Qed.
-  Global Instance big_sepMS_affine Φ X :
+  Lemma big_sepMS_affine Φ X :
+    (∀ x, x ∈ X → Affine (Φ x)) → Affine ([∗ mset] x ∈ X, Φ x).
+  Proof. apply big_opMS_closed; apply _. Qed.
+  Global Instance big_sepMS_affine' Φ X :
     (∀ x, Affine (Φ x)) → Affine ([∗ mset] x ∈ X, Φ x).
-  Proof.
-    induction X using gmultiset_ind;
-      [rewrite big_opMS_empty|rewrite big_opMS_insert]; apply _.
-  Qed.
+  Proof. intros; apply big_sepMS_affine, _. Qed.
 
   Global Instance big_sepMS_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
     Timeless ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite big_opMS_empty. apply _. Qed.
-  Global Instance big_sepMS_timeless `{!Timeless (emp%I : PROP)} Φ X :
+  Lemma big_sepMS_timeless `{!Timeless (emp%I : PROP)} Φ X :
+    (∀ x, x ∈ X → Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
+  Proof. apply big_opMS_closed; apply _. Qed.
+  Global Instance big_sepMS_timeless' `{!Timeless (emp%I : PROP)} Φ X :
     (∀ x, Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
-  Proof.
-    induction X using gmultiset_ind;
-      [rewrite big_opMS_empty|rewrite big_opMS_insert]; apply _.
-  Qed.
+  Proof. intros; apply big_sepMS_timeless, _. Qed.
 
   (* See comment above [big_sepM_subseteq] as for why the [Affine]
      instance is placed late. *)

iris/bi/derived_laws.v

@@ -223,6 +223,11 @@ Proof.
   - by apply impl_intro_l; rewrite left_id.
 Qed.
 
+Lemma impl_refl P Q : Q ⊢ P → P.
+Proof. apply impl_intro_l, and_elim_l. Qed.
+Lemma impl_trans P Q R : (P → Q) ∧ (Q → R) ⊢ (P → R).
+Proof. apply impl_intro_l. by rewrite assoc !impl_elim_r. Qed.
+
 Lemma False_impl P : (False → P) ⊣⊢ True.
 Proof.
   apply (anti_symm (⊢)); [by auto|].
@@ -336,13 +341,20 @@ Global Instance iff_proper :
   Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_iff PROP) := ne_proper_2 _.
 
 Lemma iff_refl Q P : Q ⊢ P ↔ P.
-Proof. rewrite /bi_iff; apply and_intro; apply impl_intro_l; auto. Qed.
+Proof. rewrite /bi_iff. apply and_intro; apply impl_refl. Qed.
 Lemma iff_sym P Q : (P ↔ Q) ⊣⊢ (Q ↔ P).
 Proof.
   apply equiv_entails. split; apply and_intro;
     try apply and_elim_r; apply and_elim_l.
 Qed.
-
+Lemma iff_trans P Q R : (P ↔ Q) ∧ (Q ↔ R) ⊢ (P ↔ R).
+Proof.
+  apply and_intro.
+  - rewrite /bi_iff (and_elim_l _ (_ → _)) (and_elim_l _ (_ → _)).
+    apply impl_trans.
+  - rewrite /bi_iff (and_elim_r _ (_ → _)) (and_elim_r _ (_ → _)) comm.
+    apply impl_trans.
+Qed.
 
 (* BI Stuff *)
 Local Hint Resolve sep_mono : core.
@@ -427,6 +439,8 @@ Proof.
   apply wand_intro_l. rewrite left_absorb. auto.
 Qed.
 
+Lemma wand_refl P : ⊢ P -∗ P.
+Proof. apply wand_intro_l. by rewrite right_id. Qed.
 Lemma wand_trans P Q R : (P -∗ Q) ∗ (Q -∗ R) ⊢ (P -∗ R).
 Proof. apply wand_intro_l. by rewrite assoc !wand_elim_r. Qed.
 
@@ -476,8 +490,16 @@ Proof. solve_proper. Qed.
 Global Instance wand_iff_proper :
   Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_wand_iff PROP) := ne_proper_2 _.
 
-Lemma wand_iff_refl P : emp ⊢ P ∗-∗ P.
+Lemma wand_iff_refl P : ⊢ P ∗-∗ P.
 Proof. apply and_intro; apply wand_intro_l; by rewrite right_id. Qed.
+Lemma wand_iff_sym P Q : (P ∗-∗ Q) ⊣⊢ (Q ∗-∗ P).
+Proof. apply equiv_entails; split; rewrite /bi_wand_iff; eauto. Qed.
+Lemma wand_iff_trans P Q R : (P ∗-∗ Q) ∗ (Q ∗-∗ R) ⊢ (P ∗-∗ R).
+Proof.
+  apply and_intro.
+  - rewrite /bi_wand_iff !and_elim_l. apply wand_trans.
+  - rewrite /bi_wand_iff !and_elim_r comm. apply wand_trans.
+Qed.
 
 Lemma wand_entails P Q : (⊢ P -∗ Q) → P ⊢ Q.
 Proof. intros. rewrite -[P]emp_sep. by apply wand_elim_l'. Qed.
@@ -496,12 +518,6 @@ Proof.
   intros HPQ; apply (anti_symm (⊢));
     apply wand_entails; rewrite /bi_emp_valid HPQ /bi_wand_iff; auto.
 Qed.
-Lemma wand_iff_sym P Q :
-  (P ∗-∗ Q) ⊣⊢ (Q ∗-∗ P).
-Proof.
-  apply equiv_entails; split; apply and_intro;
-    try apply and_elim_r; apply and_elim_l.
-Qed.
 
 Lemma entails_impl P Q : (P ⊢ Q) → (⊢ P → Q).
 Proof. intros ->. apply impl_intro_l. auto. Qed.

iris/bi/lib/fractional.v

@@ -5,20 +5,33 @@ From iris.prelude Require Import options.
 Class Fractional {PROP : bi} (Φ : Qp → PROP) :=
   fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
 Global Arguments Fractional {_} _%I : simpl never.
+Global Arguments fractional {_ _ _} _ _.
+
+(** The [AsFractional] typeclass eta-expands a proposition [P] into [Φ q] such
+that [Φ] is a fractional predicate. This is needed because higher-order
+unification cannot be relied upon to guess the right [Φ].
 
+[AsFractional] should generally be used in APIs that work with fractional
+predicates (instead of [Fractional]): when the user provides the original
+resource [P], have a premise [AsFractional P Φ 1] to convert that into some
+fractional predicate.
+
+The equivalence in [as_fractional] should hold definitionally; various typeclass
+instances assume that [Φ q] will un-do the eta-expansion performed by
+[AsFractional]. *)
 Class AsFractional {PROP : bi} (P : PROP) (Φ : Qp → PROP) (q : Qp) := {
   as_fractional : P ⊣⊢ Φ q;
-  as_fractional_fractional :> Fractional Φ
+  as_fractional_fractional : Fractional Φ
 }.
 Global Arguments AsFractional {_} _%I _%I _%Qp.
-
-Global Arguments fractional {_ _ _} _ _.
-
 Global Hint Mode AsFractional - ! - - : typeclass_instances.
-(* To make [as_fractional_fractional] a useful instance, we have to
-allow [q] to be an evar. The head of [Φ] will always be a λ so ! is
-not a useful mode there. *)
-Global Hint Mode AsFractional - - + - : typeclass_instances.
+
+(** The class [FrameFractionalQp] is used for fractional framing, it substracts
+the fractional of the hypothesis from the goal: it computes [r := qP - qR].
+See [frame_fractional] for how it is used. *)
+Class FrameFractionalQp (qR qP r : Qp) :=
+  frame_fractional_qp : qP = (qR + r)%Qp.
+Global Hint Mode FrameFractionalQp ! ! - : typeclass_instances.
 
 Section fractional.
   Context {PROP : bi}.
@@ -34,39 +47,45 @@ Section fractional.
     by setoid_rewrite Hequiv.
   Qed.
 
-  Lemma fractional_split P P1 P2 Φ q1 q2 :
-    AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    P ⊣⊢ P1 ∗ P2.
-  Proof. by move=>-[-> ->] [-> _] [-> _]. Qed.
-  Lemma fractional_split_1 P P1 P2 Φ q1 q2 :
-    AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    P -∗ P1 ∗ P2.
-  Proof. intros. apply bi.entails_wand. by rewrite -(fractional_split P). Qed.
-  Lemma fractional_split_2 P P1 P2 Φ q1 q2 :
-    AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    P1 -∗ P2 -∗ P.
-  Proof. intros. apply bi.entails_wand, bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
-
+  (* Every [Fractional] predicate admits an obvious [AsFractional] instance.
+
+  Ideally, this instance would mean that a user never has to define a manual
+  [AsFractional] instance for a [Fractional] predicate (even if it's of the
+  form [λ q, Φ a1 ‥ q ‥ an] for some n-ary predicate [Φ].) However, Coq's
+  lack of guarantees for higher-order unification mean this instance wouldn't
+  guarantee to apply for every [AsFractional] goal.
+
+  Therefore, this instance is not global to avoid conflicts with existing instances
+  defined by our users, since we can't ask users to universally delete their
+  manually-defined [AsFractional] instances for their own [Fractional] predicates.
+
+  (We could just support this instance for predicates with the fractional argument
+  in the final position, but that was felt to be a bit of a foot-gun - users would
+  have to remember to *not* define an [AsFractional] some of the time.) *)
+  Local Instance fractional_as_fractional Φ q :
+    Fractional Φ → AsFractional (Φ q) Φ q.
+  Proof. done. Qed.
+
+  (** This lemma is meant to be used when [P] is known. But really you should be
+   using [iDestruct "H" as "[H1 H2]"], which supports splitting at fractions. *)
+  Lemma fractional_split P Φ q1 q2 :
+    AsFractional P Φ (q1 + q2) →
+    P ⊣⊢ Φ q1 ∗ Φ q2.
+  Proof. by move=>-[-> ->]. Qed.
+  (** This lemma is meant to be used when [P] is known. But really you should be
+   using [iDestruct "H" as "[H1 H2]"], which supports halving fractions. *)
+  Lemma fractional_half P Φ q :
+    AsFractional P Φ q →
+    P ⊣⊢ Φ (q/2)%Qp ∗ Φ (q/2)%Qp.
+  Proof. by rewrite -{1}(Qp.div_2 q)=>-[->->]. Qed.
+  (** This lemma is meant to be used when [P1], [P2] are known. But really you
+   should be using [iCombine "H1 H2" as "H"] (for forwards reasoning) or
+   [iSplitL]/[iSplitR] (for goal-oriented reasoning), which support merging
+   fractions. *)
   Lemma fractional_merge P1 P2 Φ q1 q2 `{!Fractional Φ} :
     AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    P1 -∗ P2 -∗ Φ (q1 + q2)%Qp.
-  Proof.
-    move=>-[-> _] [-> _]. rewrite fractional.
-    apply bi.entails_wand, bi.wand_intro_r. done.
-  Qed.
-
-  Lemma fractional_half P P12 Φ q :
-    AsFractional P Φ q → AsFractional P12 Φ (q/2) →
-    P ⊣⊢ P12 ∗ P12.
-  Proof. by rewrite -{1}(Qp.div_2 q)=>-[->->][-> _]. Qed.
-  Lemma fractional_half_1 P P12 Φ q :
-    AsFractional P Φ q → AsFractional P12 Φ (q/2) →
-    P -∗ P12 ∗ P12.
-  Proof. intros. apply bi.entails_wand. by rewrite -(fractional_half P). Qed.
-  Lemma fractional_half_2 P P12 Φ q :
-    AsFractional P Φ q → AsFractional P12 Φ (q/2) →
-    P12 -∗ P12 -∗ P.
-  Proof. intros. apply bi.entails_wand, bi.wand_intro_r. by rewrite -(fractional_half P). Qed.
+    P1 ∗ P2 ⊣⊢ Φ (q1 + q2)%Qp.
+  Proof. move=>-[-> _] [-> _]. rewrite fractional //. Qed.
 
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional (P : PROP) :
@@ -96,7 +115,7 @@ Section fractional.
 
   Global Instance as_fractional_embed `{!BiEmbed PROP PROP'} P Φ q :
     AsFractional P Φ q → AsFractional (⎡ P ⎤) (λ q, ⎡ Φ q ⎤)%I q.
-  Proof. split; [by rewrite ->!as_fractional | apply _]. Qed.
+  Proof. intros [??]; split; [by f_equiv|apply _]. Qed.
 
   Global Instance fractional_big_sepL {A} (l : list A) Ψ :
     (∀ k x, Fractional (Ψ k x)) →
@@ -123,107 +142,57 @@ Section fractional.
     Fractional (PROP:=PROP) (λ q, [∗ mset] x ∈ X, Ψ x q)%I.
   Proof. intros ? q q'. rewrite -big_sepMS_sep. by setoid_rewrite fractional. Qed.
 
-  (** Mult instances *)
-
-  Global Instance mul_fractional_l Φ Ψ p :
-    (∀ q, AsFractional (Φ q) Ψ (q * p)) → Fractional Φ.
-  Proof.
-    intros H q q'. rewrite ->!as_fractional, Qp.mul_add_distr_r. by apply H.
-  Qed.
-  Global Instance mul_fractional_r Φ Ψ p :
-    (∀ q, AsFractional (Φ q) Ψ (p * q)) → Fractional Φ.
-  Proof.
-    intros H q q'. rewrite ->!as_fractional, Qp.mul_add_distr_l. by apply H.
-  Qed.
-
-  (* REMARK: These two instances do not work in either direction of the
-     search:
-       - In the forward direction, they make the search not terminate
-       - In the backward direction, the higher order unification of Φ
-         with the goal does not work. *)
-  Local Instance mul_as_fractional_l P Φ p q :
-    AsFractional P Φ (q * p) → AsFractional P (λ q, Φ (q * p)%Qp) q.
-  Proof.
-    intros H. split; first apply H. eapply (mul_fractional_l _ Φ p).
-    split; first done. apply H.
-  Qed.
-  Local Instance mul_as_fractional_r P Φ p q :
-    AsFractional P Φ (p * q) → AsFractional P (λ q, Φ (p * q)%Qp) q.
-  Proof.
-    intros H. split; first apply H. eapply (mul_fractional_r _ Φ p).
-    split; first done. apply H.
-  Qed.
-
   (** Proof mode instances *)
-  Global Instance from_and_fractional_fwd P P1 P2 Φ q1 q2 :
-    AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    FromSep P P1 P2.
-  Proof. by rewrite /FromSep=>-[-> ->] [-> _] [-> _]. Qed.
-  Global Instance combine_sep_fractional_bwd P P1 P2 Φ q1 q2 :
-    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → AsFractional P Φ (q1 + q2) →
-    CombineSepAs P1 P2 P | 50.
+  Global Instance from_sep_fractional P Φ q1 q2 :
+    AsFractional P Φ (q1 + q2) → FromSep P (Φ q1) (Φ q2).
+  Proof. rewrite /FromSep=>-[-> ->] //. Qed.
+  Global Instance combine_sep_as_fractional P1 P2 Φ q1 q2 :
+    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
+    CombineSepAs P1 P2 (Φ (q1 + q2)%Qp) | 50.
   (* Explicit cost, to make it easier to provide instances with higher or
      lower cost. Higher-cost instances exist to combine (for example)
      [l ↦{q1} v1] with [l ↦{q2} v2] where [v1] and [v2] are not unifiable. *)
-  Proof. by rewrite /CombineSepAs =>-[-> _] [-> <-] [-> _]. Qed.
-
-  Global Instance from_sep_fractional_half_fwd P Q Φ q :
-    AsFractional P Φ q → AsFractional Q Φ (q/2) →
-    FromSep P Q Q | 10.
-  Proof. by rewrite /FromSep -{1}(Qp.div_2 q)=>-[-> ->] [-> _]. Qed.
-  Global Instance from_sep_fractional_half_bwd P Q Φ q :
-    AsFractional P Φ (q/2) → AsFractional Q Φ q →
-    CombineSepAs P P Q | 50.
+  Proof. rewrite /CombineSepAs =>-[-> _] [-> <-] //. Qed.
+
+  Global Instance from_sep_fractional_half P Φ q :
+    AsFractional P Φ q → FromSep P (Φ (q / 2)%Qp) (Φ (q / 2)%Qp) | 10.
+  Proof. rewrite /FromSep -{1}(Qp.div_2 q). intros [-> <-]. rewrite Qp.div_2 //. Qed.
+  Global Instance combine_sep_as_fractional_half P Φ q :
+    AsFractional P Φ (q/2) → CombineSepAs P P (Φ q) | 50.
   (* Explicit cost, to make it easier to provide instances with higher or
      lower cost. Higher-cost instances exist to combine (for example)
      [l ↦{q1} v1] with [l ↦{q2} v2] where [v1] and [v2] are not unifiable. *)
-  Proof. rewrite /CombineSepAs=>-[-> <-] [-> _]. by rewrite Qp.div_2. Qed.
-
-  Global Instance into_sep_fractional P P1 P2 Φ q1 q2 :
-    AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    IntoSep P P1 P2.
-  Proof. intros. rewrite /IntoSep [P]fractional_split //. Qed.
-
-  Global Instance into_sep_fractional_half P Q Φ q :
-    AsFractional P Φ q → AsFractional Q Φ (q/2) →
-    IntoSep P Q Q | 100.
-  Proof. intros. rewrite /IntoSep [P]fractional_half //. Qed.
-
-  (* The instance [frame_fractional] can be tried at all the nodes of
-     the proof search. The proof search then fails almost always on
-     [AsFractional R Φ r], but the slowdown is still noticeable.  For
-     that reason, we factorize the three instances that could have been
-     defined for that purpose into one. *)
-  Inductive FrameFractionalHyps
-      (p : bool) (R : PROP) (Φ : Qp → PROP) (RES : PROP) : Qp → Qp → Prop :=
-    | frame_fractional_hyps_l Q q q' r:
-       Frame p R (Φ q) Q →
-       MakeSep Q (Φ q') RES →
-       FrameFractionalHyps p R Φ RES r (q + q')
-    | frame_fractional_hyps_r Q q q' r:
-       Frame p R (Φ q') Q →
-       MakeSep Q (Φ q) RES →
-       FrameFractionalHyps p R Φ RES r (q + q')
-    | frame_fractional_hyps_half q :
-       AsFractional RES Φ (q/2) →
-       FrameFractionalHyps p R Φ RES (q/2) q.
-  Existing Class FrameFractionalHyps.
-  Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
-    frame_fractional_hyps_half.
+  Proof. rewrite /CombineSepAs=>-[-> <-]. by rewrite Qp.div_2. Qed.
+
+  Global Instance into_sep_fractional P Φ q1 q2 :
+    AsFractional P Φ (q1 + q2) → IntoSep P (Φ q1) (Φ q2).
+  Proof. intros [??]. rewrite /IntoSep [P]fractional_split //. Qed.
+
+  Global Instance into_sep_fractional_half P Φ q :
+    AsFractional P Φ q → IntoSep P (Φ (q / 2)%Qp) (Φ (q / 2)%Qp) | 100.
+  Proof. intros [??]. rewrite /IntoSep [P]fractional_half //. Qed.
+
+  Global Instance frame_fractional_qp_add_l q q' : FrameFractionalQp q (q + q') q'.
+  Proof. by rewrite /FrameFractionalQp. Qed.
+  Global Instance frame_fractional_qp_add_r q q' : FrameFractionalQp q' (q + q') q.
+  Proof. by rewrite /FrameFractionalQp Qp.add_comm. Qed.
+  Global Instance frame_fractional_qp_half q : FrameFractionalQp (q/2) q (q/2).
+  Proof. by rewrite /FrameFractionalQp Qp.div_2. Qed.
 
   (* Not an instance because of performance; you can locally add it if you are
   willing to pay the cost. We have concrete instances for certain fractional
-  assertions such as ↦. *)
-  Lemma frame_fractional p R r Φ P q RES:
-    AsFractional R Φ r → AsFractional P Φ q →
-    FrameFractionalHyps p R Φ RES r q →
-    Frame p R P RES.
+  assertions such as ↦.
+
+  Coq is sometimes unable to infer the [Φ], hence it might be useful to write
+  [apply: (frame_fractional (λ q, ...))] when using the lemma to prove your
+  custom instance. See also https://github.com/coq/coq/issues/17688 *)
+  Lemma frame_fractional Φ p R P qR qP r :
+    AsFractional R Φ qR →
+    AsFractional P Φ qP →
+    FrameFractionalQp qR qP r →
+    Frame p R P (Φ r).
   Proof.
-    rewrite /Frame=>-[HR _][->?]H.
-    revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
-    - rewrite fractional /Frame /MakeSep=><-<-. by rewrite assoc.
-    - rewrite fractional /Frame /MakeSep=><-<-=>_.
-      by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
-    - move=>-[-> _]->. by rewrite bi.intuitionistically_if_elim -fractional Qp.div_2.
+    rewrite /Frame /FrameFractionalQp=> -[-> _] [-> ?] ->.
+    by rewrite bi.intuitionistically_if_elim fractional.
   Qed.
 End fractional.

iris/proofmode/class_instances_make.v

@@ -62,6 +62,10 @@ Global Instance make_and_emp_l P : QuickAffine P → KnownLMakeAnd emp P P.
 Proof. apply emp_and. Qed.
 Global Instance make_and_emp_r P : QuickAffine P → KnownRMakeAnd P emp P.
 Proof. apply and_emp. Qed.
+Global Instance make_and_false_l P : KnownLMakeAnd False P False.
+Proof. apply left_absorb, _. Qed.
+Global Instance make_and_false_r P : KnownRMakeAnd P False False.
+Proof. by rewrite /KnownRMakeAnd /MakeAnd right_absorb. Qed.
 Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. by rewrite /MakeAnd. Qed.
 
@@ -74,6 +78,10 @@ Global Instance make_or_emp_l P : QuickAffine P → KnownLMakeOr emp P emp.
 Proof. apply emp_or. Qed.
 Global Instance make_or_emp_r P : QuickAffine P → KnownRMakeOr P emp emp.
 Proof. apply or_emp. Qed.
+Global Instance make_or_false_l P : KnownLMakeOr False P P.
+Proof. apply left_id, _. Qed.
+Global Instance make_or_false_r P : KnownRMakeOr P False P.
+Proof. by rewrite /KnownRMakeOr /MakeOr right_id. Qed.
 Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
 Proof. by rewrite /MakeOr. Qed.
 

iris/proofmode/class_instances_updates.v

@@ -186,6 +186,15 @@ Global Instance add_modal_fupd `{!BiFUpd PROP} E1 E2 P Q :
   AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
 Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 
+Global Instance elim_acc_bupd `{!BiBUpd PROP} {X} α β mγ Q :
+  ElimAcc (X:=X) True bupd bupd α β mγ
+          (|==> Q)
+          (λ x, |==> β x ∗ (mγ x -∗? |==> Q))%I.
+Proof.
+  iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+  iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
+  iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
+Qed.
 Global Instance elim_acc_fupd `{!BiFUpd PROP} {X} E1 E2 E α β mγ Q :
   ElimAcc (X:=X) True (fupd E1 E2) (fupd E2 E1) α β mγ
           (|={E1,E}=> Q)

iris/proofmode/classes.v

@@ -273,7 +273,11 @@ Note that [FromSep] and [CombineSepAs] have nearly the same definition. However,
 they have different Hint Modes and are used for different tactics. [FromSep] is
 used to compute the two new goals obtained after applying [iSplitL]/[iSplitR],
 taking the current goal as input. [CombineSepAs] is used to combine two
-hypotheses into one. *)
+hypotheses into one.
+
+In terms of costs, note that the [AsFractional] instance for [CombineSepAs]
+has cost 50. If that instance should take priority over yours, make sure to use
+a higher cost. *)
 Class CombineSepAs {PROP : bi} (P Q R : PROP) := combine_sep_as : P ∗ Q ⊢ R.
 Global Arguments CombineSepAs {_} _%I _%I _%I : simpl never.
 Global Arguments combine_sep_as {_} _%I _%I _%I {_}.
@@ -547,8 +551,6 @@ Global Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
    based on [ElimAcc] and [IntoAcc].  However, logics like Iris 2 that support
    invariants but not mask-changing fancy updates can use this class directly to
    still benefit from [iInv].
-
-   TODO: Add support for a binder (like accessors have it).
 *)
 Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
       (Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))

iris/proofmode/ltac_tactics.v

@@ -3136,7 +3136,7 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
 (* Without closing view shift *)
 Tactic Notation "iInvCore" constr(N) "with" constr(pats) "in" tactic3(tac) :=
   iInvCore N with pats as (@None string) in ltac:(tac).
-(* Without pattern *)
+(* Without selection pattern *)
 Tactic Notation "iInvCore" constr(N) "as" constr(Hclose) "in" tactic3(tac) :=
   iInvCore N with "[$]" as Hclose in ltac:(tac).
 (* Without both *)
@@ -3287,7 +3287,7 @@ Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(
                 | _ => revert x; intros x1; iDestructHyp H as (   x2 x3 x4 x5 x6 x7 x8 x9 x10) pat
                 end).
 
-(* Without pattern *)
+(* Without selection pattern *)
 Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
   iInvCore N as (Some Hclose) in
     (fun x H => lazymatch type of x with

tests/proofmode.ref

@@ -269,6 +269,17 @@ Tactic failure: iSpecialize: Q not persistent.
      : string
 The command has indeed failed with message:
 Tactic failure: iSpecialize: (|==> P)%I not persistent.
+"test_iFrame_conjunction_3"
+     : string
+1 goal
+  
+  PROP : bi
+  P, Q : PROP
+  Absorbing0 : Absorbing Q
+  ============================
+  "HQ" : Q
+  --------------------------------------∗
+  False
 "test_iFrame_affinely_emp"
      : string
 1 goal
@@ -308,6 +319,15 @@ Tactic failure: iSpecialize: (|==> P)%I not persistent.
   ============================
   --------------------------------------∗
   ▷ (∃ x : nat, emp ∧ ⌜x = 0⌝ ∨ emp)
+"test_iFrame_or_3"
+     : string
+1 goal
+  
+  PROP : bi
+  P1, P2, P3 : PROP
+  ============================
+  --------------------------------------∗
+  ▷ (∃ x : nat, ⌜x = 0⌝)
 "test_iFrame_or_affine_1"
      : string
 1 goal