Improve iFrame tactic

- It can now also frame under later.
- Better treatment of evars, it now won't end up in loops whenever the goal
  involves sub-formulas ?P and it trying to apply all framing rules eagerly.
- It no longer delta expands while framing.
- Better clean up of True sub-formulas after a successful frame. For example,
  framing "P" in "▷ ▷ P ★ Q" yields just "Q" instead of "▷ True ★ Q" or so.

heap_lang/lib/barrier/proof.v

@@ -104,7 +104,8 @@ Proof.
   iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
   iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}))
     "-" as {γ'} "[#? Hγ']"; eauto.
-  { iNext. iFrame "Hl". iExists (const P). rewrite !big_sepS_singleton /=.
+  { iNext. rewrite /barrier_inv /=. iFrame "Hl".
+    iExists (const P). rewrite !big_sepS_singleton /=.
     iSplit; [|done]. by iIntros "> ?". }
   iAssert (barrier_ctx γ' l P)%I as "#?".
   { rewrite /barrier_ctx. by repeat iSplit. }

heap_lang/lib/par.v

@@ -41,7 +41,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊢ WP e1 || e2 {{ Φ }}.
 Proof.
-  iIntros {?} "(#Hh&H1&H2&H)". iApply par_spec; auto.
+  iIntros {?} "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); auto.
   iFrame "Hh H". iSplitL "H1"; by wp_let.
 Qed.
 End proof.

proofmode/coq_tactics.v

@@ -712,42 +712,65 @@ Proof.
 Qed.
 
 (** * Framing *)
-Class Frame (R P Q : uPred M) := frame : (R ★ Q) ⊢ P.
+(** The [option] is to account for formulas that can be framed entirely, so
+we do not end up with [True]s everywhere. *)
+Class Frame (R P : uPred M) (mQ : option (uPred M)) :=
+  frame : (R ★ from_option True mQ) ⊢ P.
 Arguments frame : clear implicits.
 
-Global Instance frame_here R : Frame R R True | 1.
+Instance frame_here R : Frame R R None | 1.
 Proof. by rewrite /Frame right_id. Qed.
-Global Instance frame_here_l R P : Frame R (R ★ P) P | 0.
-Proof. done. Qed.
-Global Instance frame_here_r R P : Frame R (P ★ R) P | 0.
-Proof. by rewrite /Frame comm. Qed.
-Global Instance frame_here_and_l R P : Frame R (R ∧ P) P | 0.
-Proof. by rewrite /Frame sep_and. Qed.
-Global Instance frame_here_and_r R P : Frame R (P ∧ R) P | 0.
-Proof. by rewrite /Frame sep_and comm. Qed.
-Global Instance frame_sep_l R P1 P2 Q :
-  Frame R P1 Q → Frame R (P1 ★ P2) (Q ★ P2).
-Proof. rewrite /Frame => <-. solve_sep_entails. Qed.
-Global Instance frame_sep_r R P1 P2 Q :
-  Frame R P2 Q → Frame R (P1 ★ P2) (P1 ★ Q).
-Proof. rewrite /Frame => <-. solve_sep_entails. Qed.
-Global Instance frame_or R P1 P2 Q1 Q2 :
-  Frame R P1 Q1 → Frame R P2 Q2 → Frame R (P1 ∨ P2) (Q1 ∨ Q2).
-Proof. rewrite /Frame=> <- <-. by rewrite -sep_or_l. Qed.
-Global Instance frame_exist {A} R (Φ Ψ : A → uPred M) :
-  (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∃ x, Φ x) (∃ x, Ψ x).
+Instance frame_sep_l R P1 P2 mQ :
+  Frame R P1 mQ →
+  Frame R (P1 ★ P2) (Some $ if mQ is Some Q then Q ★ P2 else P2)%I.
+Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
+Instance frame_sep_r R P1 P2 mQ :
+  Frame R P2 mQ →
+  Frame R (P1 ★ P2) (Some $ if mQ is Some Q then P1 ★ Q else P1)%I.
+Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
+Instance frame_and_l R P1 P2 mQ :
+  Frame R P1 mQ →
+  Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then Q ∧ P2 else P2)%I.
+Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
+Instance frame_and_r R P1 P2 mQ :
+  Frame R P2 mQ →
+  Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then P1 ∧ Q else P1)%I.
+Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
+Instance frame_or R P1 P2 mQ1 mQ2 :
+  Frame R P1 mQ1 → Frame R P2 mQ2 →
+  Frame R (P1 ∨ P2) (match mQ1, mQ2 with
+                     | Some Q1, Some Q2 => Some (Q1 ∨ Q2)%I | _, _ => None
+                     end).
+Proof.
+  rewrite /Frame=> <- <-.
+  destruct mQ1 as [Q1|], mQ2 as [Q2|]; simpl; auto with I.
+  by rewrite -sep_or_l.
+Qed.
+Instance frame_later R P mQ :
+  Frame R P mQ → Frame R (▷ P) (if mQ is Some Q then Some (▷ Q) else None)%I.
+Proof.
+  rewrite /Frame=><-.
+  by destruct mQ; rewrite /= later_sep -(later_intro R) ?later_True.
+Qed.
+Instance frame_exist {A} R (Φ : A → uPred M) mΨ :
+  (∀ a, Frame R (Φ a) (mΨ a)) →
+  Frame R (∃ x, Φ x) (Some (∃ x, if mΨ x is Some Q then Q else True))%I.
 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).
+Instance frame_forall {A} R (Φ : A → uPred M) mΨ :
+  (∀ a, Frame R (Φ a) (mΨ a)) →
+  Frame R (∀ x, Φ x) (Some (∀ x, if mΨ x is Some Q then Q else True))%I.
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 
-Lemma tac_frame Δ Δ' i p R P Q :
-  envs_lookup_delete i Δ = Some (p, R, Δ')%I → Frame R P Q →
-  (if p then Δ else Δ') ⊢ Q → Δ ⊢ P.
+Lemma tac_frame Δ Δ' i p R P mQ :
+  envs_lookup_delete i Δ = Some (p, R, Δ')%I → Frame R P mQ →
+  (if mQ is Some Q then (if p then Δ else Δ') ⊢ Q else True) →
+  Δ ⊢ P.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ? HQ; destruct p.
-  - by rewrite envs_lookup_persistent_sound // HQ always_elim.
-  - rewrite envs_lookup_sound //; simpl. by rewrite HQ.
+  intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
+  - rewrite envs_lookup_persistent_sound // always_elim.
+    rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
+  - rewrite envs_lookup_sound //; simpl.
+    rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
 Qed.
 
 (** * Disjunction *)
@@ -842,3 +865,19 @@ Proof.
     by rewrite right_id wand_elim_r.
 Qed.
 End tactics.
+
+(** Make sure we can frame in the presence of evars without making Coq loop due
+to it applying these rules too eager.
+
+Note: that [Hint Mode Frame - + + - : typeclass_instances] would disable framing
+with evars entirely.
+Note: we give presence to framing on the left. *)
+Hint Extern 0 (Frame _ ?R _) => class_apply @frame_here : typeclass_instances.
+Hint Extern 9 (Frame _ (_ ★ _) _) => class_apply @frame_sep_l : typeclass_instances.
+Hint Extern 10 (Frame _ (_ ★ _) _) => class_apply @frame_sep_r : typeclass_instances.
+Hint Extern 9 (Frame _ (_ ∧ _) _) => class_apply @frame_and_l : typeclass_instances.
+Hint Extern 10 (Frame _ (_ ∧ _) _) => class_apply @frame_and_r : typeclass_instances.
+Hint Extern 10 (Frame _ (_ ∨ _) _) => class_apply @frame_or : typeclass_instances.
+Hint Extern 10 (Frame _ (▷ _) _) => class_apply @frame_later : typeclass_instances.
+Hint Extern 10 (Frame _ (∃ _, _) _) => class_apply @frame_exist : typeclass_instances.
+Hint Extern 10 (Frame _ (∀ _, _) _) => class_apply @frame_forall : typeclass_instances.

proofmode/pviewshifts.v

@@ -21,8 +21,9 @@ Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Λ Σ) :
 Proof.
   rewrite /ExistSplit=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
 Qed.
-Global Instance frame_pvs E1 E2 R P Q :
-  Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+Instance frame_pvs E1 E2 R P mQ :
+  Frame R P mQ →
+  Frame R (|={E1,E2}=> P) (Some (|={E1,E2}=> from_option True mQ))%I.
 Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
 Global Instance to_wand_pvs E1 E2 R P Q :
   ToWand R P Q → ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q).
@@ -96,6 +97,9 @@ Proof.
 Qed.
 End pvs.
 
+Hint Extern 10 (Frame _ (|={_,_}=> _) _) =>
+  class_apply frame_pvs : typeclass_instances.
+
 Tactic Notation "iPvsIntro" := apply tac_pvs_intro.
 
 Tactic Notation "iPvsCore" constr(H) :=

proofmode/weakestpre.v

@@ -8,10 +8,15 @@ Context {Λ : language} {Σ : iFunctor}.
 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 {{ Ψ }}).
+Instance frame_wp E e R Φ mΨ :
+  (∀ v, Frame R (Φ v) (mΨ v)) →
+  Frame R (WP e @ E {{ Φ }})
+          (Some (WP e @ E {{ v, if mΨ v is Some Q then Q else True }}))%I.
 Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 Global Instance fsa_split_wp E e Φ :
   FSASplit (WP e @ E {{ Φ }})%I E (wp_fsa e) (language.atomic e) Φ.
 Proof. split. done. apply _. Qed.
 End weakestpre.
+
+Hint Extern 10 (Frame _ (WP _ @ _ {{ _ }}) _) =>
+  class_apply frame_wp : typeclass_instances.
\ No newline at end of file

tests/proofmode.v

@@ -39,4 +39,8 @@ Proof.
   iSplitL "H3".
   * iFrame "H3". by iRight.
   * iSplitL "HQ". iAssumption. by iSplitL "H1".
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma demo_3 (M : cmraT) (P1 P2 P3 : uPred M) :
+  (P1 ★ P2 ★ P3) ⊢ (▷ P1 ★ ▷ (P2 ★ ∃ x, (P3 ∧ x = 0) ∨ P3)).
+Proof. iIntros "($ & $ & H)". iFrame "H". simpl. iNext. by iExists 0. Qed.
\ No newline at end of file