From b94d126229455fbaacf218ca2b7a052b862579ee Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Feb 2016 10:53:20 +0100
Subject: [PATCH] sts, auth: use cancel

---
 program_logic/auth.v | 11 +++++------
 program_logic/sts.v  |  9 +++++----
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/program_logic/auth.v b/program_logic/auth.v
index a582173d8..0e022e91d 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,4 +1,4 @@
-From algebra Require Export auth.
+From algebra Require Export auth upred_tactics.
 From program_logic Require Export invariants global_functor.
 Import uPred.
 
@@ -56,8 +56,7 @@ Section auth.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     trans (▷ auth_inv γ φ ★ auth_own γ a)%I.
     { rewrite /auth_inv -(exist_intro a) later_sep.
-      rewrite const_equiv // left_id.
-      rewrite [(_ ★ ▷ φ _)%I]comm -assoc. apply sep_mono; first done.
+      rewrite const_equiv // left_id. cancel (▷ φ a)%I.
       rewrite -later_intro /auth_own -own_op auth_both_op. done. }
     rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
     by rewrite always_and_sep_l.
@@ -81,8 +80,7 @@ Section auth.
     { by move=>n ? ? /timeless_iff ->. }
     { by eauto with I. }
     rewrite const_equiv // left_id comm.
-    apply sep_mono; first done.
-    by rewrite sep_elim_l.
+    apply sep_mono_r. by rewrite sep_elim_l.
   Qed.
 
   Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
@@ -91,6 +89,7 @@ Section auth.
     ⊑ (|={E}=> ▷ auth_inv γ φ ★ auth_own γ (L a)).
   Proof.
     intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a â‹… a')).
+    (* TODO it would be really nice to use cancel here *)
     rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
     rewrite -pvs_frame_l. apply sep_mono; first done.
     rewrite const_equiv // left_id -later_intro -own_op.
@@ -146,7 +145,7 @@ Section auth.
     P ⊑ fsa E Ψ.
   Proof.
     intros ??? HP. eapply auth_fsa with N γ a; eauto.
-    rewrite HP; apply sep_mono; first done; apply forall_mono=> a'.
+    rewrite HP; apply sep_mono_r, forall_mono=> a'.
     apply wand_mono; first done. apply (fsa_mono fsa)=> b.
     rewrite -(exist_intro L). by repeat erewrite <-exist_intro by apply _.
   Qed.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index b66a60e13..c6271cf6f 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -1,4 +1,4 @@
-From algebra Require Export sts.
+From algebra Require Export sts upred_tactics.
 From program_logic Require Export invariants global_functor.
 Import uPred.
 
@@ -85,7 +85,7 @@ Section sts.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     trans (▷ sts_inv γ φ ★ sts_own γ s (⊤ ∖ sts.tok s))%I.
     { rewrite /sts_inv -(exist_intro s) later_sep.
-      rewrite [(_ ★ ▷ φ _)%I]comm -assoc. apply sep_mono_r.
+      cancel (▷ φ s)%I.
       by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
     rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
     by rewrite always_and_sep_l.
@@ -112,8 +112,9 @@ Section sts.
     sts.steps (s, T) (s', T') →
     (▷ φ s' ★ own γ (sts_auth s T)) ⊑ (|={E}=> ▷ sts_inv γ φ ★ sts_own γ s' T').
   Proof.
-    intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s').
-    rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
+    intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s') later_sep.
+    (* TODO it would be really nice to use cancel here *)
+    rewrite [(_ ★ ▷φ _)%I]comm -assoc.
     rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
     rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
     trans (|={E}=> own γ (sts_auth s' T'))%I.
-- 
GitLab