From efd340e5399b5a9c0a93168b8d0ea2d9f02515d3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Feb 2016 13:26:57 +0100
Subject: [PATCH] provide tactics to more easily apply wands

---
 algebra/upred.v      | 15 +++++++++++++++
 program_logic/auth.v |  6 +++---
 program_logic/sts.v  |  6 +++---
 3 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 9bb48f67c..06b9b69d0 100644
--- a/algebra/upred.v
+++ b/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).
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 65e54aeca..f16ac33e6 100644
--- a/program_logic/auth.v
+++ b/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.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index f8e477745..ea3186370 100644
--- a/program_logic/sts.v
+++ b/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'.
-- 
GitLab