From 497cb7fa7e01162caebed6eb9710a121f1f309d0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 7 May 2016 12:41:03 +0200
Subject: [PATCH] Convert more stuff to the proofmode.

---
 heap_lang/heap.v           |  30 ++++-----
 program_logic/auth.v       | 127 ++++++++++++-------------------------
 program_logic/hoare.v      |   5 +-
 program_logic/invariants.v |  84 +++++-------------------
 program_logic/sts.v        | 107 ++++++++++---------------------
 program_logic/viewshifts.v |   6 +-
 proofmode/invariants.v     |  12 ++--
 proofmode/sts.v            |   3 +-
 8 files changed, 120 insertions(+), 254 deletions(-)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 7ac3c7a24..5de7c10d8 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -144,10 +144,8 @@ Section heap.
   Proof.
     iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
     iPvs (auth_empty heap_name) as "Hheap".
-    (* TODO: change [auth_fsa] to single turnstile and use [iApply] *)
-    apply (auth_fsa heap_inv (wp_fsa (Alloc e)))
-      with N heap_name ∅; simpl; eauto with I.
-    iFrame "Hheap". iIntros {h}. rewrite [∅ ⋅ h]left_id.
+    iApply (auth_fsa heap_inv (wp_fsa (Alloc e)) _ N); simpl; eauto.
+    iFrame "Hinv Hheap". iIntros {h}. rewrite [∅ ⋅ h]left_id.
     iIntros "[% Hheap]". rewrite /heap_inv.
     iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
     iIntros {l} "[% Hheap]". iExists (op {[ l := Frac 1 (DecAgree v) ]}), _, _.
@@ -164,9 +162,9 @@ Section heap.
     ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
   Proof.
     iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
-    apply (auth_fsa' heap_inv (wp_fsa _) id)
-      with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto.
-    iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+    iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
+      heap_name {[ l := Frac q (DecAgree v) ]}); simpl; eauto.
+    iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
     rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
     iIntros "$". by iSplit.
@@ -178,9 +176,9 @@ Section heap.
     ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
     iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
-    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
-      with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I.
-    iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+    iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l) _
+      N _ heap_name {[ l := Frac 1 (DecAgree v') ]}); simpl; eauto.
+    iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
     iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
@@ -192,9 +190,9 @@ Section heap.
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
     iIntros {????} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
-    apply (auth_fsa' heap_inv (wp_fsa _) id)
-      with N heap_name {[ l := Frac q (DecAgree v') ]}; simpl; eauto 10.
-    iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+    iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
+      heap_name {[ l := Frac q (DecAgree v') ]}); simpl; eauto 10.
+    iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
     iIntros "$". by iSplit.
@@ -206,9 +204,9 @@ Section heap.
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
     iIntros {???} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
-    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
-      with N heap_name {[ l := Frac 1 (DecAgree v1) ]}; simpl; eauto 10.
-    iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+    iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l)
+      _ N _ heap_name {[ l := Frac 1 (DecAgree v1) ]}); simpl; eauto 10.
+    iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
     rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
     iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index dc272fe9d..029e21f17 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export auth upred_tactics.
 From iris.program_logic Require Export invariants ghost_ownership.
+From iris.proofmode Require Import invariants ghost_ownership.
 Import uPred.
 
 (* The CMRA we need. *)
@@ -57,100 +58,56 @@ Section auth.
     ✓ a → nclose N ⊆ E →
     ▷ φ a ⊢ (|={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
   Proof.
-    intros Ha HN. eapply sep_elim_True_r.
-    { by eapply (own_alloc (Auth (Excl a) a) E). }
-    rewrite pvs_frame_l. apply pvs_strip_pvs.
-    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.
-      ecancel [▷ φ _]%I.
-      by rewrite -later_intro -own_op auth_both_op. }
-    rewrite (inv_alloc N E) // /auth_ctx pvs_frame_r. apply pvs_mono.
-    by rewrite always_and_sep_l.
+    iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
+    iPvs (own_alloc (Auth (Excl a) a)) as {γ} "Hγ"; first done.
+    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
+    iPvs (inv_alloc N _ (auth_inv γ φ) with "-[Hγ']"); first done.
+    { iNext. iExists a. by iFrame "Hφ". }
+    iPvsIntro; iExists γ; by iFrame "Hγ'".
   Qed.
 
   Lemma auth_empty γ E : True ⊢ |={E}=> auth_own γ ∅.
   Proof. by rewrite -own_empty. Qed.
 
-  Lemma auth_opened E γ a :
-    (▷ auth_inv γ φ ★ auth_own γ a)
-    ⊢ (|={E}=> ∃ a', ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a)).
-  Proof.
-    rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
-    rewrite later_sep [(â–· own _ _)%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
-    rewrite own_valid_l discrete_valid -!assoc. apply const_elim_sep_l=>Hv.
-    rewrite [(▷φ _ ★ _)%I]comm assoc -own_op.
-    rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
-    apply exist_elim=>a'.
-    rewrite left_id -(exist_intro a').
-    apply (eq_rewrite b (a ⋅ a') (λ x, ✓ x ★ ▷ φ x ★ own γ (● x ⋅ ◯ a))%I).
-    { by move=>n x y /timeless_iff ->. }
-    { by eauto with I. }
-    rewrite -valid_intro; last by apply Hv.
-    rewrite left_id comm. auto with I.
-  Qed.
-
-  Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
-    Lv a → ✓ (L a ⋅ a') →
-    (▷ φ (L a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a))
-    ⊢ (|={E}=> ▷ auth_inv γ φ ★ auth_own γ (L a)).
-  Proof.
-    intros HL Hv. rewrite /auth_inv -(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_r.
-    rewrite -later_intro -own_op.
-    by apply own_update, (auth_local_update_l L).
-  Qed.
-
   Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
 
-  Lemma auth_fsa E N P (Ψ : V → iPropG Λ Σ) γ a :
-    fsaV →
-    nclose N ⊆ E →
-    P ⊢ auth_ctx γ N φ →
-    P ⊢ (▷ auth_own γ a ★ ∀ a',
-          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
-          fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
-            ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
-            (auth_own γ (L a) -★ Ψ x))) →
-    P ⊢ fsa E Ψ.
+  Lemma auth_fsa E N (Ψ : V → iPropG Λ Σ) γ a :
+    fsaV → nclose N ⊆ E →
+    (auth_ctx γ N φ ★ ▷ auth_own γ a ★ ∀ a',
+      ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+      fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
+        ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
+        (auth_own γ (L a) -★ Ψ x)))
+     ⊢ fsa E Ψ.
   Proof.
-    rewrite /auth_ctx=>? HN Hinv Hinner.
-    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
-    apply wand_intro_l. rewrite assoc.
-    rewrite (pvs_timeless (E ∖ N)) pvs_frame_l pvs_frame_r.
-    apply (fsa_strip_pvs fsa).
-    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.
-    eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
-    { rewrite assoc [(_ ★ own _ _)%I]comm -assoc discrete_valid.  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.
-    rewrite sep_exist_l; apply exist_elim=> ?.
-    rewrite comm -!assoc. apply const_elim_sep_l=>-[HL Hv].
-    rewrite assoc [(_ ★ (_ -★ _))%I]comm -assoc.
-    rewrite (auth_closing (E ∖ N)) //; [].
-    rewrite pvs_frame_l. apply pvs_mono.
-    by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l.
+    iIntros {??} "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
+    iInv N as {a'} "[Hγ Hφ]".
+    iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
+    iDestruct (own_valid _ with "Hγ !") as "Hvalid".
+    iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
+    iDestruct "Ha'" as {b} "Ha'"; iDestruct "Ha'" as %Ha'.
+    rewrite ->(left_id _ _) in Ha'; setoid_subst.
+    iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
+    { iApply "HΨ"; by iSplit. }
+    iIntros {v} "HL". iDestruct "HL" as {L Lv ?} "(% & Hφ & HΨ)".
+    iPvs (own_update _ with "Hγ") as "[Hγ Hγf]".
+    { apply (auth_local_update_l L); tauto. }
+    iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
+    iNext. iExists (L a ⋅ b). by iFrame "Hφ".
   Qed.
-  Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Ψ : V → iPropG Λ Σ) γ a :
-    fsaV →
-    nclose N ⊆ E →
-    P ⊢ auth_ctx γ N φ →
-    P ⊢ (▷ auth_own γ a ★ (∀ a',
-          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
-          fsa (E ∖ nclose N) (λ x,
-            ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
-            (auth_own γ (L a) -★ Ψ x)))) →
-    P ⊢ fsa E Ψ.
+
+  Lemma auth_fsa' L `{!LocalUpdate Lv L} E N (Ψ : V → iPropG Λ Σ) γ a :
+    fsaV → nclose N ⊆ E →
+    (auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a',
+      ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+      fsa (E ∖ nclose N) (λ x,
+        ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
+        (auth_own γ (L a) -★ Ψ x))))
+    ⊢ fsa E Ψ.
   Proof.
-    intros ??? HP. eapply auth_fsa with N γ a; eauto.
-    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 _.
+    iIntros {??} "(#Ha & Hγf & HΨ)"; iApply (auth_fsa E N Ψ γ a); auto.
+    iFrame "Ha Hγf". iIntros {a'} "H".
+    iApply fsa_wand_r; iSplitL; first by iApply "HΨ".
+    iIntros {v} "?"; by iExists L, Lv, _.
   Qed.
 End auth.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index c2d7b69f7..e5898f1f8 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre viewshifts.
-From iris.proofmode Require Import weakestpre.
+From iris.proofmode Require Import weakestpre invariants.
 
 Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
     (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ :=
@@ -145,7 +145,6 @@ Lemma ht_inv N E P Φ R e :
   (inv N R ★ {{ ▷ R ★ P }} e @ E ∖ nclose N {{ v, ▷ R ★ Φ v }})
     ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
-  iIntros {??} "[#? #Hwp] ! HP". eapply wp_inv; eauto.
-  iIntros "HR". iApply "Hwp". by iSplitL "HR".
+  iIntros {??} "[#? #Hwp] ! HP". iInv N as "HR". iApply "Hwp". by iSplitL "HR".
 Qed.
 End hoare.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index da98cfd99..3fb1ae706 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -1,11 +1,7 @@
-From iris.algebra Require Export base.
 From iris.program_logic Require Import ownership.
-From iris.program_logic Require Export namespaces pviewshifts weakestpre.
+From iris.program_logic Require Export namespaces.
+From iris.proofmode Require Import pviewshifts.
 Import uPred.
-Local Hint Extern 100 (@eq coPset _ _) => set_solver.
-Local Hint Extern 100 (@subseteq coPset _ _) => set_solver.
-Local Hint Extern 100 (_ ∉ _) => set_solver.
-Local Hint Extern 99 ({[ _ ]} ⊆ _) => apply elem_of_subseteq_singleton.
 
 (** Derived forms and lemmas about them. *)
 Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
@@ -29,72 +25,22 @@ Proof. rewrite /inv; apply _. Qed.
 Lemma always_inv N P : □ inv N P ⊣⊢ inv N P.
 Proof. by rewrite always_always. Qed.
 
-(** Invariants can be opened around any frame-shifting assertion. *)
-Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ R :
-  fsaV → nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Ψ a)) →
-  R ⊢ fsa E Ψ.
-Proof.
-  intros ? HN Hinv Hinner.
-  rewrite -[R](idemp (∧)%I) {1}Hinv Hinner =>{Hinv Hinner R}.
-  rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i.
-  rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN.
-  rewrite -(fsa_open_close E (E ∖ {[encode i]})) //; last by set_solver+.
-  (* Add this to the local context, so that set_solver finds it. *)
-  assert ({[encode i]} ⊆ nclose N) by eauto.
-  rewrite (always_sep_dup (ownI _ _)).
-  rewrite {1}pvs_openI !pvs_frame_r.
-  apply pvs_mask_frame_mono; [set_solver..|].
-  rewrite (comm _ (â–·_)%I) -assoc wand_elim_r fsa_frame_l.
-  apply fsa_mask_frame_mono; [set_solver..|]. intros a.
-  rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id.
-  apply pvs_mask_frame'; set_solver.
-Qed.
-Lemma inv_fsa_timeless {A} (fsa : FSA Λ Σ A)
-    `{!FrameShiftAssertion fsaV fsa} E N P `{!TimelessP P} Ψ R :
-  fsaV → nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (P -★ fsa (E ∖ nclose N) (λ a, P ★ Ψ a)) →
-  R ⊢ fsa E Ψ.
-Proof.
-  intros ??? HR. eapply inv_fsa, wand_intro_l; eauto.
-  trans (|={E ∖ N}=> P ★ R)%I; first by rewrite pvs_timeless pvs_frame_r.
-  apply (fsa_strip_pvs _). rewrite HR wand_elim_r.
-  apply: fsa_mono=> v. by rewrite -later_intro.
-Qed.
-
-(* Derive the concrete forms for pvs and wp, because they are useful. *)
-
-Lemma pvs_inv E N P Q R :
-  nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (▷ P -★ |={E ∖ nclose N}=> (▷ P ★ Q)) →
-  R ⊢ (|={E}=> Q).
-Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
-Lemma pvs_inv_timeless E N P `{!TimelessP P} Q R :
-  nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (P -★ |={E ∖ nclose N}=> (P ★ Q)) →
-  R ⊢ (|={E}=> Q).
-Proof. intros. by apply: (inv_fsa_timeless pvs_fsa). Qed.
-
-Lemma wp_inv E e N P Φ R :
-  atomic e → nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (▷ P -★ WP e @ E ∖ nclose N {{ v, ▷ P ★ Φ v }}) →
-  R ⊢ WP e @ E {{ Φ }}.
-Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
-Lemma wp_inv_timeless E e N P `{!TimelessP P} Φ R :
-  atomic e → nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (P -★ WP e @ E ∖ nclose N {{ v, P ★ Φ v }}) →
-  R ⊢ WP e @ E {{ Φ }}.
-Proof. intros. by apply: (inv_fsa_timeless (wp_fsa e)). Qed.
-
 Lemma inv_alloc N E P : nclose N ⊆ E → ▷ P ⊢ |={E}=> inv N P.
 Proof.
   intros. rewrite -(pvs_mask_weaken N) //.
   by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
 Qed.
+
+(** Invariants can be opened around any frame-shifting assertion. *)
+Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ :
+  fsaV → nclose N ⊆ E →
+  (inv N P ★ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Ψ a))) ⊢ fsa E Ψ.
+Proof.
+  iIntros {??} "[#Hinv HΨ]"; rewrite /inv; iDestruct "Hinv" as {i} "[% Hi]".
+  iApply (fsa_open_close E (E ∖ {[encode i]})); auto; first by set_solver.
+  iPvs (pvs_openI' _ _ with "Hi") as "HP"; [set_solver..|iPvsIntro].
+  iApply (fsa_mask_weaken _ (E ∖ N)); first set_solver.
+  iApply fsa_wand_r; iSplitL; [by iApply "HΨ"|iIntros {v} "[HP HΨ]"].
+  iPvs (pvs_closeI' _ _ P with "[HP]"); [auto|by iSplit|set_solver|done].
+Qed.
 End inv.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index dfe31b991..18fd96dac 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export sts upred_tactics.
 From iris.program_logic Require Export invariants ghost_ownership.
+From iris.proofmode Require Import invariants ghost_ownership.
 Import uPred.
 
 (** The CMRA we need. *)
@@ -64,7 +65,7 @@ Section sts.
   Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
     T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 →
     sts_ownS γ S1 T1 ⊢ (|={E}=> sts_ownS γ S2 T2).
-  Proof. intros ? ? ?. by apply own_update, sts_update_frag. Qed.
+  Proof. intros ???. by apply own_update, sts_update_frag. Qed.
 
   Lemma sts_own_weaken E γ s S T1 T2 :
     T2 ⊆ T1 → s ∈ S → sts.closed S T2 →
@@ -80,86 +81,46 @@ Section sts.
     nclose N ⊆ E →
     ▷ φ s ⊢ (|={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
   Proof.
-    intros HN. eapply sep_elim_True_r.
-    { apply (own_alloc (sts_auth s (⊤ ∖ sts.tok s)) E).
-      apply sts_auth_valid; set_solver. }
-    rewrite pvs_frame_l. apply pvs_strip_pvs.
-    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.
-      ecancel [▷ φ _]%I.
-      by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
-    rewrite (inv_alloc N E) // /sts_ctx pvs_frame_r.
-    by rewrite always_and_sep_l.
-  Qed.
-
-  Lemma sts_opened E γ S T :
-    (▷ sts_inv γ φ ★ sts_ownS γ S T)
-    ⊢ (|={E}=> ∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own γ (sts_auth s T)).
-  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). ecancel [▷ φ _]%I.
-    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 sts_op_auth_frag //.
-    by assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
-  Qed.
-
-  Lemma sts_closing E γ s T s' T' :
-    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 -(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_valid. apply const_elim_sep_l=>Hval.
-    trans (|={E}=> own γ (sts_auth s' T'))%I.
-    { by apply own_update, sts_update_auth. }
-    by rewrite -own_op sts_op_auth_frag_up.
+    iIntros {?} "Hφ". rewrite /sts_ctx /sts_own.
+    iPvs (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as {γ} "Hγ".
+    { apply sts_auth_valid; set_solver. }
+    iExists γ; iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
+    iPvs (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
+    iNext. iExists s. by iFrame "Hφ".
   Qed.
 
   Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
 
-  Lemma sts_fsaS E N P (Ψ : V → iPropG Λ Σ) γ S T :
+  Lemma sts_fsaS E N (Ψ : V → iPropG Λ Σ) γ S T :
     fsaV → nclose N ⊆ E →
-    P ⊢ sts_ctx γ N φ →
-    P ⊢ (sts_ownS γ S T ★ ∀ s,
-          ■ (s ∈ S) ★ ▷ φ s -★
-          fsa (E ∖ nclose N) (λ x, ∃ s' T',
-            ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★
-            (sts_own γ s' T' -★ Ψ x))) →
-    P ⊢ fsa E Ψ.
+    (sts_ctx γ N φ ★ sts_ownS γ S T ★ ∀ s,
+      ■ (s ∈ S) ★ ▷ φ s -★
+      fsa (E ∖ nclose N) (λ x, ∃ s' T',
+        ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★ (sts_own γ s' T' -★ Ψ x)))
+    ⊢ fsa E Ψ.
   Proof.
-    rewrite /sts_ctx=>? HN Hinv Hinner.
-    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
-    apply wand_intro_l. rewrite assoc.
-    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.
-    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'.
-    rewrite comm -!assoc. apply const_elim_sep_l=>-Hstep.
-    rewrite assoc [(_ ★ (_ -★ _))%I]comm -assoc.
-    rewrite (sts_closing (E ∖ N)) //; [].
-    rewrite pvs_frame_l. apply pvs_mono.
-    by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l.
+    iIntros {??} "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
+    iInv N as {s} "[Hγ Hφ]"; iTimeless "Hγ".
+    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ !") as %Hvalid.
+    assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
+    assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
+    iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ".
+    iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
+    { iApply "HΨ"; by iSplit. }
+    iIntros {a} "H"; iDestruct "H" as {s' T'} "(% & Hφ & HΨ)".
+    iPvs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
+    iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]".
+    iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ".
+    iNext; iExists s'; by iFrame "Hφ".
   Qed.
 
-  Lemma sts_fsa E N P (Ψ : V → iPropG Λ Σ) γ s0 T :
+  Lemma sts_fsa E N (Ψ : V → iPropG Λ Σ) γ s0 T :
     fsaV → nclose N ⊆ E →
-    P ⊢ sts_ctx γ N φ →
-    P ⊢ (sts_own γ s0 T ★ ∀ s,
-          ■ (s ∈ sts.up s0 T) ★ ▷ φ s -★
-          fsa (E ∖ nclose N) (λ x, ∃ s' T',
-            ■ (sts.steps (s, T) (s', T')) ★ ▷ φ s' ★
-            (sts_own γ s' T' -★ Ψ x))) →
-    P ⊢ fsa E Ψ.
+    (sts_ctx γ N φ ★ sts_own γ s0 T ★ ∀ s,
+      ■ (s ∈ sts.up s0 T) ★ ▷ φ s -★
+      fsa (E ∖ nclose N) (λ x, ∃ s' T',
+        ■ (sts.steps (s, T) (s', T')) ★ ▷ φ s' ★
+        (sts_own γ s' T' -★ Ψ x)))
+    ⊢ fsa E Ψ.
   Proof. by apply sts_fsaS. Qed.
 End sts.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index b66bed545..5e2dbdeda 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Import ownership.
 From iris.program_logic Require Export pviewshifts invariants ghost_ownership.
-From iris.proofmode Require Import pviewshifts.
+From iris.proofmode Require Import pviewshifts invariants.
 Import uPred.
 
 Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
@@ -94,8 +94,8 @@ Proof. intros; apply vs_mask_frame; set_solver. Qed.
 Lemma vs_inv N E P Q R :
   nclose N ⊆ E → (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q).
 Proof.
-  iIntros {?} "#[? Hvs] ! HP". eapply pvs_inv; eauto.
-  iIntros "HR". iApply ("Hvs" with "!"). by iSplitL "HR".
+  iIntros {?} "#[? Hvs] ! HP". iInv N as "HR".
+  iApply ("Hvs" with "!"). by iSplitL "HR".
 Qed.
 
 Lemma vs_alloc N P : â–· P ={N}=> inv N P.
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
index ae13afe5b..9758f82bc 100644
--- a/proofmode/invariants.v
+++ b/proofmode/invariants.v
@@ -14,7 +14,8 @@ Lemma tac_inv_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
   envs_app false (Esnoc Enil i (▷ P)) Δ = Some Δ' →
   Δ' ⊢ fsa (E ∖ nclose N) (λ a, ▷ P ★ Φ a) → Δ ⊢ Q.
 Proof.
-  intros ????? HΔ'. rewrite -(fsa_split Q). eapply (inv_fsa fsa); eauto.
+  intros ????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
+  rewrite // -always_and_sep_l. apply and_intro; first done.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
 Qed.
 
@@ -24,9 +25,12 @@ Lemma tac_inv_fsa_timeless {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   Δ' ⊢ fsa (E ∖ nclose N) (λ a, P ★ Φ a) → Δ ⊢ Q.
 Proof.
-  intros ?????? HΔ'. rewrite -(fsa_split Q).
-  eapply (inv_fsa_timeless fsa); eauto.
-  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
+  intros ?????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
+  rewrite // -always_and_sep_l. apply and_intro, wand_intro_l; first done.
+  trans (|={E ∖ N}=> P ★ Δ)%I; first by rewrite pvs_timeless pvs_frame_r.
+  apply (fsa_strip_pvs _).
+  rewrite envs_app_sound //; simpl. rewrite right_id HΔ' wand_elim_r.
+  apply: fsa_mono=> v. by rewrite -later_intro.
 Qed.
 End invariants.
 
diff --git a/proofmode/sts.v b/proofmode/sts.v
index 636f8fee5..d234c5dec 100644
--- a/proofmode/sts.v
+++ b/proofmode/sts.v
@@ -18,7 +18,8 @@ Lemma tac_sts_fsa {A} (fsa : FSA Λ _ A) fsaV Δ E N i γ S T Q Φ :
       ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★ (sts_own γ s' T' -★ Φ a))) →
   Δ ⊢ Q.
 Proof.
-  intros ????? HΔ'. rewrite -(fsa_split Q); eapply (sts_fsaS φ fsa); eauto.
+  intros ????? HΔ'. rewrite -(fsa_split Q) -(sts_fsaS φ fsa) //.
+  rewrite // -always_and_sep_l. apply and_intro; first done.
   rewrite envs_lookup_sound //; simpl; apply sep_mono_r.
   apply forall_intro=>s; apply wand_intro_l.
   rewrite -assoc; apply const_elim_sep_l=> Hs.
-- 
GitLab