provide tactics to more easily apply wands

algebra/upred.v

@@ -623,6 +623,21 @@ Lemma wand_elim_l' P Q R : P ⊑ (Q -★ R) → (P ★ Q) ⊑ R.
 Proof. intros ->; apply wand_elim_l. Qed.
 Lemma wand_elim_r' P Q R : Q ⊑ (P -★ R) → (P ★ Q) ⊑ R.
 Proof. intros ->; apply wand_elim_r. Qed.
+Lemma wand_apply_l P Q Q' R R' : P ⊑ (Q' -★ R') → R' ⊑ R → Q ⊑ Q' → (P ★ Q) ⊑ R.
+Proof. intros -> -> <-; apply wand_elim_l. Qed.
+Lemma wand_apply_r P Q Q' R R' : P ⊑ (Q' -★ R') → R' ⊑ R → Q ⊑ Q' → (Q ★ P) ⊑ R.
+Proof. intros -> -> <-; apply wand_elim_r. Qed.
+Lemma wand_apply_l' P Q Q' R : P ⊑ (Q' -★ R) → Q ⊑ Q' → (P ★ Q) ⊑ R.
+Proof. intros -> <-; apply wand_elim_l. Qed.
+Lemma wand_apply_r' P Q Q' R : P ⊑ (Q' -★ R) → Q ⊑ Q' → (Q ★ P) ⊑ R.
+Proof. intros -> <-; apply wand_elim_r. Qed.
+Lemma wand_frame_l P Q R : (Q -★ R) ⊑ (P ★ Q -★ P ★ R).
+Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
+Lemma wand_frame_r P Q R : (Q -★ R) ⊑ (Q ★ P -★ R ★ P).
+Proof.
+  apply wand_intro_l. rewrite ![(_ ★ P)%I]comm -assoc.
+  apply sep_mono_r, wand_elim_r.
+Qed.
 Lemma sep_and P Q : (P ★ Q) ⊑ (P ∧ Q).
 Proof. auto. Qed.
 Lemma impl_wand P Q : (P → Q) ⊑ (P -★ Q).

program_logic/auth.v

@@ -116,9 +116,9 @@ Section auth.
     rewrite (auth_opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
     apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
     rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]comm.
-    (* Getting this wand eliminated is really annoying. *)
-    rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
-    rewrite wand_elim_r fsa_frame_l.
+    eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
+    { rewrite assoc [(_ ★ own _ _)%I]comm -assoc. done. }
+    rewrite fsa_frame_l.
     apply (fsa_mono_pvs fsa)=> x.
     rewrite sep_exist_l; apply exist_elim=> L.
     rewrite sep_exist_l; apply exist_elim=> Lv.

program_logic/sts.v

@@ -133,9 +133,9 @@ Section sts.
     rewrite (sts_opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
     apply (fsa_strip_pvs fsa). apply exist_elim=>s.
     rewrite (forall_elim s). rewrite [(▷_ ★ _)%I]comm.
-    (* Getting this wand eliminated is really annoying. *)
-    rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
-    rewrite wand_elim_r fsa_frame_l.
+    eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
+    { rewrite assoc [(_ ★ own _ _)%I]comm -assoc. done. }
+    rewrite fsa_frame_l.
     apply (fsa_mono_pvs fsa)=> x.
     rewrite sep_exist_l; apply exist_elim=> s'.
     rewrite sep_exist_l; apply exist_elim=>T'.