write tactics to move particular assertions to the front, and to introduce a...

write tactics to move particular assertions to the front, and to introduce a (*) while taking paticular assertions to the left/right

algebra/upred_tactics.v

@@ -146,6 +146,74 @@ Tactic Notation "ecancel" open_constr(Ps) :=
        close Ps (@nil (uPred M)) ltac:(fun Qs => cancel Qs)
     end. 
 
+(** [to_front [P1, P2, ..]] rewrites in the premise of ⊑ such that
+    the assumptions P1, P2, ... appear at the front, in that order. *)
+Tactic Notation "to_front" open_constr(Ps) :=
+  let rec tofront Ps :=
+    lazymatch eval hnf in Ps with
+    | [] => idtac
+    | ?P :: ?Ps =>
+      rewrite ?(assoc (★)%I);
+      match goal with
+      | |- (?Q ★ _)%I ⊑ _ => (* test if it is already at front. *)
+        unify P Q with typeclass_instances
+      | |- _ => find_pat P ltac:(fun P => rewrite {1}[(_ ★ P)%I]comm)
+      end;
+      tofront Ps
+    end
+  in
+  rewrite [X in _ ⊑ X]lock;
+  tofront (rev Ps);
+  rewrite -[X in _ ⊑ X]lock.
+
+(** [sep_split] is used to introduce a (★).
+    Use [sep_split left: [P1, P2, ...]] to define which assertions will be
+    taken to the left; the rest will be available on the right.
+    [sep_split right: [P1, P2, ...]] works the other way around. *)
+(* TODO: These tactics fail if the list contains *all* assumptions.
+   However, in these cases using the "other" variant with the emtpy list
+   is much more convenient anyway. *)
+(* TODO: These tactics are pretty slow, can we use the reflection stuff
+   above to speed them up? *)
+Tactic Notation "sep_split" "right:" open_constr(Ps) :=
+  match goal with
+  | |- ?P ⊑ _ =>
+    let iProp := type of P in (* ascribe a type to the list, to prevent evars from appearing *)
+    lazymatch eval hnf in (Ps : list iProp) with
+    | [] => apply sep_intro_True_r
+    | ?P :: ?Ps =>
+      to_front (P::Ps);
+      (* Run assoc length (ps) times *)
+      let rec nassoc Ps :=
+          lazymatch eval hnf in Ps with
+          | [] => idtac
+          | _ :: ?Ps => rewrite assoc; nassoc Ps
+          end in
+      rewrite [X in _ ⊑ X]lock -?(assoc (★)%I);
+      nassoc Ps; rewrite [X in X ⊑ _]comm -[X in _ ⊑ X]lock;
+      apply sep_mono
+   end
+  end.
+Tactic Notation "sep_split" "left:" open_constr(Ps) :=
+  match goal with
+  | |- ?P ⊑ _ =>
+    let iProp := type of P in (* ascribe a type to the list, to prevent evars from appearing *)
+    lazymatch eval hnf in (Ps : list iProp) with
+    | [] => apply sep_intro_True_l
+    | ?P :: ?Ps =>
+      to_front (P::Ps);
+      (* Run assoc length (ps) times *)
+      let rec nassoc Ps :=
+          lazymatch eval hnf in Ps with
+          | [] => idtac
+          | _ :: ?Ps => rewrite assoc; nassoc Ps
+          end in
+      rewrite [X in _ ⊑ X]lock -?(assoc (★)%I);
+      nassoc Ps; rewrite -[X in _ ⊑ X]lock;
+      apply sep_mono
+   end
+  end.
+
 (** Assumes a goal of the shape P ⊑ ▷ Q. Alterantively, if Q
     is built of ★, ∧, ∨ with ▷ in all branches; that will work, too.
     Will turn this goal into P ⊑ Q and strip ▷ in P below ★, ∧, ∨. *)

program_logic/hoare_lifting.v

+From algebra Require Import upred_tactics.
 From program_logic Require Export hoare lifting.
 From program_logic Require Import ownership.
 Import uPred.
@@ -31,21 +32,20 @@ Proof.
   intros ?? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
   rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
   rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono.
-  rewrite always_and_sep_r -assoc; apply sep_mono; first done.
+  rewrite always_and_sep_r -assoc; apply sep_mono_r.
   rewrite (later_intro (∀ _, _)) -later_sep; apply later_mono.
   apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
   rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef).
   apply wand_intro_l; rewrite !always_and_sep_l.
+  (* Apply the view shift. *)
   rewrite (assoc _ _ P') -(assoc _ _ _ P') assoc.
   rewrite {1}/vs -always_wand_impl always_elim wand_elim_r.
   rewrite pvs_frame_r; apply pvs_mono.
-  rewrite (comm _ (Φ1 _ _ _)) -assoc (assoc _ (Φ1 _ _ _)).
-  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r.
-  rewrite assoc (comm _ _ (wp _ _ _)) -assoc.
-  apply sep_mono; first done.
-  destruct ef as [e'|]; simpl; [|by apply const_intro].
-  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
-  by apply const_intro.
+  (* Now we're almost done. *)
+  sep_split left: [Φ1 _ _ _; {{ Φ1 _ _ _ }} e2 @ E2 {{ Ψ }}]%I.
+  - rewrite {1}/ht -always_wand_impl always_elim wand_elim_r //.
+  - destruct ef as [e'|]; simpl; [|by apply const_intro].
+    rewrite {1}/ht -always_wand_impl always_elim wand_elim_r //.
 Qed.
 
 Lemma ht_lift_atomic_step
@@ -90,15 +90,10 @@ Proof.
   apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l.
   rewrite (forall_elim e2) (forall_elim ef).
   rewrite always_and_sep_l !always_and_sep_r {1}(always_sep_dup (■ _)).
-  rewrite {1}(assoc _ (_ ★ _)%I) -(assoc _ (■ _)%I).
-  rewrite (assoc _ (■ _)%I P) -{1}(comm _ P) -(assoc _ P).
-  rewrite (assoc _ (■ _)%I) assoc -(assoc _ (■ _ ★ P))%I.
-  rewrite (comm _ (■ _ ★ P'))%I assoc.
-  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r.
-  rewrite -assoc; apply sep_mono; first done.
-  destruct ef as [e'|]; simpl; [|by apply const_intro].
-  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
-  by apply const_intro.
+  sep_split left: [■ φ _ _; P; {{ ■ φ _ _ ★ P }} e2 @ E {{ Ψ }}]%I.
+  - rewrite {1}/ht -always_wand_impl always_elim wand_elim_r //.
+  - destruct ef as [e'|]; simpl; [|by apply const_intro].
+    rewrite assoc {1}/ht -always_wand_impl always_elim wand_elim_r //.
 Qed.
 
 Lemma ht_lift_pure_det_step

program_logic/sts.v

@@ -99,12 +99,12 @@ Section sts.
   Proof.
     rewrite /sts_inv later_exist sep_exist_r. apply exist_elim=>s.
     rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
-    rewrite -(exist_intro s).
-    rewrite [(_ ★ ▷φ _)%I]comm -!assoc -own_op -[(▷φ _ ★ _)%I]comm.
-    rewrite own_valid_l discrete_valid.
-    rewrite -!assoc. apply const_elim_sep_l=> Hvalid.
+    rewrite -(exist_intro s). ecancel [▷ φ _]%I.
+    to_front [own _ _; sts_ownS _ _ _].
+    rewrite -own_op own_valid_l discrete_valid.
+    apply const_elim_sep_l=> Hvalid.
     assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
-    rewrite const_equiv // left_id comm sts_op_auth_frag //.
+    rewrite const_equiv // left_id sts_op_auth_frag //.
     by assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
   Qed.