Better support for framing persistent hypotheses.

- Allow framing of persistent hypotheses below the always modality.
- Allow framing of persistent hypotheses in just one branch of a
  disjunction.

theories/base_logic/derived.v

@@ -656,7 +656,8 @@ Lemma always_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
 Proof. destruct p; simpl; auto using always_sep. Qed.
 Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
 Proof. destruct p; simpl; auto using always_later. Qed.
-
+Lemma always_if_laterN p n P : □?p ▷^n P ⊣⊢ ▷^n □?p P.
+Proof. destruct p; simpl; auto using always_laterN. Qed.
 
 (* True now *)
 Global Instance except_0_ne : NonExpansive (@uPred_except_0 M).

theories/base_logic/lib/fancy_updates.v

@@ -174,8 +174,8 @@ Section proofmode_classes.
     rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
   Qed.
 
-  Global Instance frame_fupd E1 E2 R P Q :
-    Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+  Global Instance frame_fupd p E1 E2 R P Q :
+    Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
   Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
 
   Global Instance is_except_0_fupd E1 E2 P : IsExcept0 (|={E1,E2}=> P).

theories/base_logic/lib/fractional.v

@@ -20,7 +20,7 @@ Section fractional.
   Context {M : ucmraT}.
   Implicit Types P Q : uPred M.
   Implicit Types Φ : Qp → uPred M.
-  Implicit Types p q : Qp.
+  Implicit Types q : Qp.
 
   Lemma fractional_split P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
@@ -145,27 +145,30 @@ Section fractional.
      [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 R Φ RES : Qp → Qp → Prop :=
-  | frame_fractional_hyps_l Q p p' r:
-      Frame R (Φ p) Q → MakeSep Q (Φ p') RES →
-      FrameFractionalHyps R Φ RES r (p + p')
-  | frame_fractional_hyps_r Q p p' r:
-      Frame R (Φ p') Q → MakeSep Q (Φ p) RES →
-      FrameFractionalHyps R Φ RES r (p + p')
-  | frame_fractional_hyps_half p:
-      AsFractional RES Φ (p/2)%Qp → FrameFractionalHyps R Φ RES (p/2)%Qp p.
+  Inductive FrameFractionalHyps
+      (p : bool) (R : uPred M) (Φ : Qp → uPred M) (RES : uPred M) : 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.
-  Global Instance frame_fractional R r Φ P p RES:
-    AsFractional R Φ r → AsFractional P Φ p → FrameFractionalHyps R Φ RES r p →
-    Frame R P RES.
+    frame_fractional_hyps_half.
+  Global Instance 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.
   Proof.
     rewrite /Frame=>-[HR _][->?]H.
-    revert H HR=>-[Q p0 p0' r0|Q p0 p0' r0|p0].
+    revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
     - rewrite fractional=><-<-. by rewrite assoc.
     - rewrite fractional=><-<-=>_.
-      rewrite (comm _ Q (Φ p0)) !assoc. f_equiv. by rewrite comm.
-    - move=>-[-> _]->. by rewrite -fractional Qp_div_2.
+      by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
+    - move=>-[-> _]->. by rewrite uPred.always_if_elim -fractional Qp_div_2.
   Qed.
 End fractional.

theories/program_logic/weakestpre.v

@@ -255,8 +255,8 @@ Section proofmode_classes.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val Λ → iProp Σ.
 
-  Global Instance frame_wp E e R Φ Ψ :
-    (∀ v, Frame R (Φ v) (Ψ v)) → Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
+  Global Instance frame_wp p E e R Φ Ψ :
+    (∀ v, Frame p R (Φ v) (Ψ v)) → Frame p R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
   Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 
   Global Instance is_except_0_wp E e Φ : IsExcept0 (WP e @ E {{ Φ }}).

theories/proofmode/class_instances.v

 From iris.proofmode Require Export classes.
 From iris.algebra Require Import gmap.
 From stdpp Require Import gmultiset.
-From iris.base_logic Require Import big_op.
+From iris.base_logic Require Import big_op tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
@@ -420,10 +420,10 @@ Global Instance into_and_big_sepL_app {A} p (Φ : nat → A → uPred M) l1 l2 :
 Proof. apply mk_into_and_sep. by rewrite big_sepL_app. Qed.
 
 (* Frame *)
-Global Instance frame_here R : Frame R R True.
-Proof. by rewrite /Frame right_id. Qed.
-Global Instance frame_here_pure φ Q : FromPure Q φ → Frame ⌜φ⌝ Q True.
-Proof. rewrite /FromPure /Frame=> ->. by rewrite right_id. Qed.
+Global Instance frame_here p R : Frame p R R True.
+Proof. by rewrite /Frame right_id always_if_elim. Qed.
+Global Instance frame_here_pure p φ Q : FromPure Q φ → Frame p ⌜φ⌝ Q True.
+Proof. rewrite /FromPure /Frame=> ->. by rewrite always_if_elim right_id. Qed.
 
 Class MakeSep (P Q PQ : uPred M) := make_sep : P ∗ Q ⊣⊢ PQ.
 Global Instance make_sep_true_l P : MakeSep True P P.
@@ -432,21 +432,29 @@ Global Instance make_sep_true_r P : MakeSep P True P.
 Proof. by rewrite /MakeSep right_id. Qed.
 Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
 Proof. done. Qed.
+
+Global Instance frame_sep_persistent_l R P1 P2 Q1 Q2 Q' :
+  Frame true R P1 Q1 → MaybeFrame true R P2 Q2 → MakeSep Q1 Q2 Q' →
+  Frame true R (P1 ∗ P2) Q' | 9.
+Proof.
+  rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
+  rewrite {1}(always_sep_dup (□ R)). solve_sep_entails.
+Qed.
 Global Instance frame_sep_l R P1 P2 Q Q' :
-  Frame R P1 Q → MakeSep Q P2 Q' → Frame R (P1 ∗ P2) Q' | 9.
+  Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
 Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
-Global Instance frame_sep_r R P1 P2 Q Q' :
-  Frame R P2 Q → MakeSep P1 Q Q' → Frame R (P1 ∗ P2) Q' | 10.
-Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc (comm _ R) assoc. Qed.
+Global Instance frame_sep_r p R P1 P2 Q Q' :
+  Frame p R P2 Q → MakeSep P1 Q Q' → Frame p R (P1 ∗ P2) Q' | 10.
+Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc. Qed.
 
-Global Instance frame_big_sepL_cons {A} (Φ : nat → A → uPred M) R Q x l :
-  Frame R (Φ 0 x ∗ [∗ list] k ↦ y ∈ l, Φ (S k) y) Q →
-  Frame R ([∗ list] k ↦ y ∈ x :: l, Φ k y) Q.
+Global Instance frame_big_sepL_cons {A} p (Φ : nat → A → uPred M) R Q x l :
+  Frame p R (Φ 0 x ∗ [∗ list] k ↦ y ∈ l, Φ (S k) y) Q →
+  Frame p R ([∗ list] k ↦ y ∈ x :: l, Φ k y) Q.
 Proof. by rewrite /Frame big_sepL_cons. Qed.
-Global Instance frame_big_sepL_app {A} (Φ : nat → A → uPred M) R Q l1 l2 :
-  Frame R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
+Global Instance frame_big_sepL_app {A} p (Φ : nat → A → uPred M) R Q l1 l2 :
+  Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
            [∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
-  Frame R ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y) Q.
+  Frame p R ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y) Q.
 Proof. by rewrite /Frame big_sepL_app. Qed.
 
 Class MakeAnd (P Q PQ : uPred M) := make_and : P ∧ Q ⊣⊢ PQ.
@@ -456,11 +464,11 @@ Global Instance make_and_true_r P : MakeAnd P True P.
 Proof. by rewrite /MakeAnd right_id. Qed.
 Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. done. Qed.
-Global Instance frame_and_l R P1 P2 Q Q' :
-  Frame R P1 Q → MakeAnd Q P2 Q' → Frame R (P1 ∧ P2) Q' | 9.
+Global Instance frame_and_l p R P1 P2 Q Q' :
+  Frame p R P1 Q → MakeAnd Q P2 Q' → Frame p R (P1 ∧ P2) Q' | 9.
 Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
-Global Instance frame_and_r R P1 P2 Q Q' :
-  Frame R P2 Q → MakeAnd P1 Q Q' → Frame R (P1 ∧ P2) Q' | 10.
+Global Instance frame_and_r p R P1 P2 Q Q' :
+  Frame p R P2 Q → MakeAnd P1 Q Q' → Frame p R (P1 ∧ P2) Q' | 10.
 Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
 
 Class MakeOr (P Q PQ : uPred M) := make_or : P ∨ Q ⊣⊢ PQ.
@@ -470,12 +478,24 @@ Global Instance make_or_true_r P : MakeOr P True True.
 Proof. by rewrite /MakeOr right_absorb. Qed.
 Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
 Proof. done. Qed.
+
+Global Instance frame_or_persistent_l R P1 P2 Q1 Q2 Q :
+  Frame true R P1 Q1 → MaybeFrame true R P2 Q2 → MakeOr Q1 Q2 Q →
+  Frame true R (P1 ∨ P2) Q | 9.
+Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
+Global Instance frame_or_persistent_r R P1 P2 Q1 Q2 Q :
+  MaybeFrame true R P2 Q2 → MakeOr P1 Q2 Q →
+  Frame true R (P1 ∨ P2) Q | 10.
+Proof.
+  rewrite /Frame /MaybeFrame /MakeOr => <- <-. by rewrite sep_or_l sep_elim_r.
+Qed.
 Global Instance frame_or R P1 P2 Q1 Q2 Q :
-  Frame R P1 Q1 → Frame R P2 Q2 → MakeOr Q1 Q2 Q → Frame R (P1 ∨ P2) Q.
+  Frame false R P1 Q1 → Frame false R P2 Q2 → MakeOr Q1 Q2 Q →
+  Frame false R (P1 ∨ P2) Q.
 Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
 
-Global Instance frame_wand R P1 P2 Q2 :
-  Frame R P2 Q2 → Frame R (P1 -∗ P2) (P1 -∗ Q2).
+Global Instance frame_wand p R P1 P2 Q2 :
+  Frame p R P2 Q2 → Frame p R (P1 -∗ P2) (P1 -∗ Q2).
 Proof.
   rewrite /Frame=> ?. apply wand_intro_l.
   by rewrite assoc (comm _ P1) -assoc wand_elim_r.
@@ -487,10 +507,11 @@ Proof. by rewrite /MakeLater later_True. Qed.
 Global Instance make_later_default P : MakeLater P (▷ P) | 100.
 Proof. done. Qed.
 
-Global Instance frame_later R R' P Q Q' :
-  IntoLaterN 1 R' R → Frame R P Q → MakeLater Q Q' → Frame R' (▷ P) Q'.
+Global Instance frame_later p R R' P Q Q' :
+  IntoLaterN 1 R' R → Frame p R P Q → MakeLater Q Q' → Frame p R' (▷ P) Q'.
 Proof.
-  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-. by rewrite later_sep.
+  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
+  by rewrite always_if_later later_sep.
 Qed.
 
 Class MakeLaterN (n : nat) (P lP : uPred M) := make_laterN : ▷^n P ⊣⊢ lP.
@@ -499,10 +520,24 @@ Proof. by rewrite /MakeLaterN laterN_True. Qed.
 Global Instance make_laterN_default P : MakeLaterN n P (▷^n P) | 100.
 Proof. done. Qed.
 
-Global Instance frame_laterN n R R' P Q Q' :
-  IntoLaterN n R' R → Frame R P Q → MakeLaterN n Q Q' → Frame R' (▷^n P) Q'.
+Global Instance frame_laterN p n R R' P Q Q' :
+  IntoLaterN n R' R → Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
+Proof.
+  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
+  by rewrite always_if_laterN laterN_sep.
+Qed.
+
+Class MakeAlways (P Q : uPred M) := make_always : □ P ⊣⊢ Q.
+Global Instance make_always_true : MakeAlways True True.
+Proof. by rewrite /MakeAlways always_pure. Qed.
+Global Instance make_always_default P : MakeAlways P (□ P) | 100.
+Proof. done. Qed.
+
+Global Instance frame_always R P Q Q' :
+  Frame true R P Q → MakeAlways Q Q' → Frame true R (□ P) Q'.
 Proof.
-  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-. by rewrite laterN_sep.
+  rewrite /Frame /MakeAlways=> <- <-.
+  by rewrite always_sep /= always_always.
 Qed.
 
 Class MakeExcept0 (P Q : uPred M) := make_except_0 : ◇ P ⊣⊢ Q.
@@ -511,21 +546,21 @@ Proof. by rewrite /MakeExcept0 except_0_True. Qed.
 Global Instance make_except_0_default P : MakeExcept0 P (◇ P) | 100.
 Proof. done. Qed.
 
-Global Instance frame_except_0 R P Q Q' :
-  Frame R P Q → MakeExcept0 Q Q' → Frame R (◇ P) Q'.
+Global Instance frame_except_0 p R P Q Q' :
+  Frame p R P Q → MakeExcept0 Q Q' → Frame p R (◇ P) Q'.
 Proof.
   rewrite /Frame /MakeExcept0=><- <-.
-  by rewrite except_0_sep -(except_0_intro R).
+  by rewrite except_0_sep -(except_0_intro (□?p R)).
 Qed.
 
-Global Instance frame_exist {A} R (Φ Ψ : A → uPred M) :
-  (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∃ x, Φ x) (∃ x, Ψ x).
+Global Instance frame_exist {A} p R (Φ Ψ : A → uPred M) :
+  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∃ x, Φ x) (∃ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
-Global Instance frame_forall {A} R (Φ Ψ : A → uPred M) :
-  (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∀ x, Φ x) (∀ x, Ψ x).
+Global Instance frame_forall {A} p R (Φ Ψ : A → uPred M) :
+  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 
-Global Instance frame_bupd R P Q : Frame R P Q → Frame R (|==> P) (|==> Q).
+Global Instance frame_bupd p R P Q : Frame p R P Q → Frame p R (|==> P) (|==> Q).
 Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
 
 (* FromOr *)

theories/proofmode/classes.v

@@ -102,9 +102,19 @@ Arguments into_op {_} _ _ _ {_}.
 (* No [Hint Mode] since we want to turn [?x] into [?x1 ⋅ ?x2], for example
 when having [H : own ?x]. *)
 
-Class Frame {M} (R P Q : uPred M) := frame : R ∗ Q ⊢ P.
-Arguments frame {_} _ _ _ {_}.
-Hint Mode Frame + ! ! - : typeclass_instances.
+Class Frame {M} (p : bool) (R P Q : uPred M) := frame : □?p R ∗ Q ⊢ P.
+Arguments frame {_ _} _ _ _ {_}.
+Hint Mode Frame + + ! ! - : typeclass_instances.
+
+Class MaybeFrame {M} (p : bool) (R P Q : uPred M) := maybe_frame : □?p R ∗ Q ⊢ P.
+Arguments maybe_frame {_} _ _ _ {_}.
+Hint Mode MaybeFrame + + ! ! - : typeclass_instances.
+
+Instance maybe_frame_frame {M} p (R P Q : uPred M) :
+  Frame p R P Q → MaybeFrame p R P Q.
+Proof. done. Qed.
+Instance maybe_frame_default {M} p (R P : uPred M) : MaybeFrame p R P P | 100.
+Proof. apply sep_elim_r. Qed.
 
 Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
 Arguments from_or {_} _ _ _ {_}.

theories/proofmode/coq_tactics.v

@@ -806,15 +806,17 @@ Qed.
 
 (** * Framing *)
 Lemma tac_frame_pure Δ (φ : Prop) P Q :
-  φ → Frame ⌜φ⌝ P Q → (Δ ⊢ Q) → Δ ⊢ P.
-Proof. intros ?? ->. by rewrite -(frame ⌜φ⌝ P) pure_True // left_id. Qed.
+  φ → Frame true ⌜φ⌝ P Q → (Δ ⊢ Q) → Δ ⊢ P.
+Proof.
+  intros ?? ->. by rewrite -(frame ⌜φ⌝ P) /= always_pure pure_True // left_id.
+Qed.
 
 Lemma tac_frame Δ Δ' i p R P Q :
-  envs_lookup_delete i Δ = Some (p, R, Δ') → Frame R P Q →
+  envs_lookup_delete i Δ = Some (p, R, Δ') → Frame p R P Q →
   ((if p then Δ else Δ') ⊢ Q) → Δ ⊢ P.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
-  - by rewrite envs_lookup_persistent_sound // always_elim -(frame R P) HQ.
+  - by rewrite envs_lookup_persistent_sound // -(frame R P) HQ.
   - rewrite envs_lookup_sound //; simpl. by rewrite -(frame R P) HQ.
 Qed.
 

theories/proofmode/tactics.v

@@ -183,7 +183,7 @@ Local Ltac iFramePure t :=
 Local Ltac iFrameHyp H :=
   eapply tac_frame with _ H _ _ _;
     [env_cbv; reflexivity || fail "iFrame:" H "not found"
-    |let R := match goal with |- Frame ?R _ _ => R end in
+    |let R := match goal with |- Frame _ ?R _ _ => R end in
      apply _ || fail "iFrame: cannot frame" R
     |iFrameFinish].
 

theories/tests/proofmode.v

@@ -165,3 +165,7 @@ Lemma test_iNext_sep2 (M : ucmraT) (P Q : uPred M) :
 Proof.
   iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
 Qed.
+
+Lemma test_frame_persistent (M : ucmraT) (P Q : uPred M) :
+  □ P -∗ Q -∗ □ (P ∗ P) ∗ (P ∧ Q ∨ Q).
+Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.