From 7ceb690d6d7492b791fcdcf5cd5953a6aa1b313e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Feb 2016 09:52:45 +0100
Subject: [PATCH] prove auth_pvs!

---
 algebra/cmra.v             |  2 +-
 algebra/upred.v            | 12 ++++++++----
 program_logic/auth.v       | 38 +++++++++++++++++++++++++++++++++-----
 program_logic/invariants.v | 16 ++++++++--------
 program_logic/viewshifts.v |  8 ++++----
 5 files changed, 54 insertions(+), 22 deletions(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 54c6c4a5d..81af47400 100644
--- a/algebra/cmra.v
+++ b/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.
diff --git a/algebra/upred.v b/algebra/upred.v
index 343dfccf3..9fb690d02 100644
--- a/algebra/upred.v
+++ b/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.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index ec2496b55..2c01dd8e4 100644
--- a/program_logic/auth.v
+++ b/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.
 
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 72529d620..2b24b5284 100644
--- a/program_logic/invariants.v
+++ b/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.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index e86145e48..39cc02e85 100644
--- a/program_logic/viewshifts.v
+++ b/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.
 
-- 
GitLab