prove auth_pvs!

algebra/cmra.v

@@ -24,7 +24,7 @@ Notation "✓{ n }" := (validN n) (at level 1, format "✓{ n }").
 
 Class Valid (A : Type) := valid : A → Prop.
 Instance: Params (@valid) 2.
-Notation "✓" := valid (at level 1).
+Notation "✓" := valid (at level 1) : C_scope.
 Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x.
 
 Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.

algebra/upred.v

@@ -191,8 +191,8 @@ Arguments uPred_holds {_} _%I _ _.
 Arguments uPred_entails _ _%I _%I.
 Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
 Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
-Notation "■ φ" := (uPred_const φ%type) (at level 20) : uPred_scope.
-Notation "x = y" := (uPred_const (x%type = y%type)) : uPred_scope.
+Notation "■ φ" := (uPred_const φ%C%type) (at level 20) : uPred_scope.
+Notation "x = y" := (uPred_const (x%C%type = y%C%type)) : uPred_scope.
 Notation "'False'" := (uPred_const False) : uPred_scope.
 Notation "'True'" := (uPred_const True) : uPred_scope.
 Infix "∧" := uPred_and : uPred_scope.
@@ -617,6 +617,10 @@ Lemma sep_and P Q : (P ★ Q) ⊑ (P ∧ Q).
 Proof. auto. Qed.
 Lemma impl_wand P Q : (P → Q) ⊑ (P -★ Q).
 Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
+Lemma const_elim_sep_l φ Q R : (φ → Q ⊑ R) → (■ φ ★ Q) ⊑ R.
+Proof. intros; apply const_elim with φ; eauto. Qed.
+Lemma const_elim_sep_r φ Q R : (φ → Q ⊑ R) → (Q ★ ■ φ) ⊑ R.
+Proof. intros; apply const_elim with φ; eauto. Qed.
 
 Global Instance sep_False : LeftAbsorb (≡) False%I (@uPred_sep M).
 Proof. intros P; apply (anti_symmetric _); auto. Qed.
@@ -669,9 +673,9 @@ Lemma later_or P Q : (▷ (P ∨ Q))%I ≡ (▷ P ∨ ▷ Q)%I.
 Proof. intros x [|n]; simpl; tauto. Qed.
 Lemma later_forall {A} (P : A → uPred M) : (▷ ∀ a, P a)%I ≡ (∀ a, ▷ P a)%I.
 Proof. by intros x [|n]. Qed.
-Lemma later_exist {A} (P : A → uPred M) : (∃ a, ▷ P a) ⊑ (▷ ∃ a, P a).
+Lemma later_exist_1 {A} (P : A → uPred M) : (∃ a, ▷ P a) ⊑ (▷ ∃ a, P a).
 Proof. by intros x [|[|n]]. Qed.
-Lemma later_exist' `{Inhabited A} (P : A → uPred M) :
+Lemma later_exist `{Inhabited A} (P : A → uPred M) :
   (▷ ∃ a, P a)%I ≡ (∃ a, ▷ P a)%I.
 Proof. intros x [|[|n]]; split; done || by exists inhabitant; simpl. Qed.
 Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.

program_logic/auth.v

@@ -59,17 +59,45 @@ Section auth.
   Qed.
 
   Context (L : LocalUpdate A) `{!LocalUpdateSpec L}.
-  Lemma auth_closing  a a' b γ :
+  Lemma auth_closing E a a' b γ :
     L a = Some b → ✓(b ⋅ a') →
-    (φ (b ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
-      ⊑ pvs N N (auth_inv γ ★ auth_own γ b).
+    (▷φ (b ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
+      ⊑ pvs E E (▷auth_inv γ ★ auth_own γ b).
   Proof.
     intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (b ⋅ a')).
-    rewrite [(_ ★ φ _)%I]commutative -associative.
+    rewrite later_sep [(_ ★ ▷φ _)%I]commutative -associative.
     rewrite -pvs_frame_l. apply sep_mono; first done.
-    rewrite -own_op. apply own_update.
+    rewrite -later_intro -own_op. apply own_update.
     by apply (auth_local_update L).
   Qed.
 
+  (* FIXME it should be enough to assume that A is all-timeless. *)
+  (* Notice how the user has t prove that `L a` equals `Some b` at
+     *all* step-indices, and similar that `b⋅a'` is valid at all
+     step-indices. This is because the side-conditions for frame-preserving
+     updates have to be shown on the meta-level. *)
+  Lemma auth_pvs `{!∀ a : authRA A, Timeless a} E P (Q : A → iProp Λ (globalC Σ)) γ a :
+    nclose N ⊆ E →
+    (auth_ctx γ ★ auth_own γ a ★ (∀ a', ▷φ (a ⋅ a') -★
+          pvs (E ∖ nclose N) (E ∖ nclose N)
+            (∃ b, L a = Some b ★ ■(✓(b⋅a')) ★ ▷φ (b ⋅ a') ★ Q b)))
+      ⊑ pvs E E (∃ b, auth_own γ b ★ Q b).
+  Proof.
+    rewrite /auth_ctx=>HN.
+    rewrite -[pvs E E _]pvs_open_close; last eassumption.
+    apply sep_mono; first done. apply wand_intro_l.
+    rewrite [auth_own _ _]later_intro associative -later_sep.
+    rewrite auth_opened later_exist sep_exist_r. apply exist_elim=>a'.
+    rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]commutative later_sep.
+    rewrite associative wand_elim_l pvs_frame_r. apply pvs_strip_pvs.
+    rewrite sep_exist_r. apply exist_elim=>b.
+    rewrite [(▷own _ _ _)%I]pvs_timeless pvs_frame_l. apply pvs_strip_pvs.
+    rewrite -!associative. apply const_elim_sep_l=>HL.
+    apply const_elim_sep_l=>Hv.
+    rewrite associative [(_ ★ Q b)%I]commutative -associative auth_closing //; [].
+    erewrite pvs_frame_l. apply pvs_mono. rewrite -(exist_intro b).
+    rewrite associative [(_ ★ Q b)%I]commutative associative.
+    apply sep_mono; last done. by rewrite commutative.
+  Qed.
 End auth.
 

program_logic/invariants.v

@@ -73,15 +73,15 @@ Proof. by rewrite always_always. Qed.
 
 Lemma pvs_open_close E N P Q :
   nclose N ⊆ E →
-  (inv N P ∧ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q))) ⊑ pvs E E Q.
+  (inv N P ★ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q))) ⊑ pvs E E Q.
 Proof.
   move=>HN.
-  rewrite /inv and_exist_r. apply exist_elim=>i.
-  rewrite -associative. apply const_elim_l=>HiN.
+  rewrite /inv sep_exist_r. apply exist_elim=>i.
+  rewrite always_and_sep_l' -associative. apply const_elim_sep_l=>HiN.
   rewrite -(pvs_trans3 E (E ∖ {[encode i]})) //; last by solve_elem_of+.
   (* Add this to the local context, so that solve_elem_of finds it. *)
   assert ({[encode i]} ⊆ nclose N) by eauto.
-  rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)).
+  rewrite (always_sep_dup' (ownI _ _)).
   rewrite {1}pvs_openI !pvs_frame_r.
   apply pvs_mask_frame_mono ; [solve_elem_of..|].
   rewrite (commutative _ (▷_)%I) -associative wand_elim_r pvs_frame_l.
@@ -92,15 +92,15 @@ Qed.
 
 Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) :
   atomic e → nclose N ⊆ E →
-  (inv N P ∧ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v))) ⊑ wp E e Q.
+  (inv N P ★ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v))) ⊑ wp E e Q.
 Proof.
   move=>He HN.
-  rewrite /inv and_exist_r. apply exist_elim=>i.
-  rewrite -associative. apply const_elim_l=>HiN.
+  rewrite /inv sep_exist_r. apply exist_elim=>i.
+  rewrite always_and_sep_l' -associative. apply const_elim_sep_l=>HiN.
   rewrite -(wp_atomic E (E ∖ {[encode i]})) //; last by solve_elem_of+.
   (* Add this to the local context, so that solve_elem_of finds it. *)
   assert ({[encode i]} ⊆ nclose N) by eauto.
-  rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)).
+  rewrite (always_sep_dup' (ownI _ _)).
   rewrite {1}pvs_openI !pvs_frame_r.
   apply pvs_mask_frame_mono; [solve_elem_of..|].
   rewrite (commutative _ (▷_)%I) -associative wand_elim_r wp_frame_l.

program_logic/viewshifts.v

@@ -88,14 +88,14 @@ Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
 
 Lemma vs_open_close N E P Q R :
   nclose N ⊆ E →
-  (inv N R ∧ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊑ (P ={E}=> Q).
+  (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊑ (P ={E}=> Q).
 Proof.
   intros; apply (always_intro' _ _), impl_intro_l.
-  rewrite associative (commutative _ P) -associative.
-  rewrite -(pvs_open_close E N) //; apply and_mono; first done.
+  rewrite always_and_sep_r' associative [(P ★ _)%I]commutative -associative.
+  rewrite -(pvs_open_close E N) //. apply sep_mono; first done.
   apply wand_intro_l.
   (* Oh wow, this is annyoing... *)
-  rewrite always_and_sep_r' associative -always_and_sep_r'.
+  rewrite associative -always_and_sep_r'.
   by rewrite /vs always_elim impl_elim_r.
 Qed.