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/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