prove frame-preservnig updates for global CMRA

algebra/fin_maps.v

@@ -223,6 +223,19 @@ Proof.
   rewrite !cmra_update_updateP; eauto using map_insert_updateP with congruence.
 Qed.
 
+Lemma map_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x :
+  x ~~>: P → (∀ y, P y → Q {[ i ↦ y ]}) → {[ i ↦ x ]} ~~>: Q.
+Proof. apply map_insert_updateP. Qed.
+Lemma map_singleton_updateP' (P : A → Prop) i x :
+  x ~~>: P → {[ i ↦ x ]} ~~>: λ m', ∃ y, m' = {[ i ↦ y ]} ∧ P y.
+Proof. eauto using map_singleton_updateP. Qed.
+Lemma map_singleton_update i (x y : A) : x ~~> y → {[ i ↦ x ]} ~~> {[ i ↦ y ]}.
+Proof.
+  rewrite !cmra_update_updateP=>?. eapply map_singleton_updateP; first eassumption.
+  by move=>? ->.
+Qed.
+
+
 Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
 Lemma map_updateP_alloc (Q : gmap K A → Prop) m x :
   ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.

program_logic/global_cmra.v

@@ -8,23 +8,33 @@ Definition globalC (Σ : gid → iFunctor) : iFunctor :=
 
 Class InG Λ (Σ : gid → iFunctor) (i : gid) (A : cmraT) :=
   inG : A = Σ i (laterC (iPreProp Λ (globalC Σ))).
-Definition to_Σ {Λ} {Σ : gid → iFunctor} (i : gid) 
-           `{!InG Λ Σ i A} (a : A) : Σ i (laterC (iPreProp Λ (globalC Σ))) :=
-  eq_rect A id a _ inG.
-Definition to_globalC {Λ} {Σ : gid → iFunctor}
-           (i : gid) (γ : gid) `{!InG Λ Σ i A} (a : A) : iGst Λ (globalC Σ) :=
-  iprod_singleton i {[ γ ↦ to_Σ _ a ]}.
-Definition own {Λ} {Σ : gid → iFunctor}
-    (i : gid) `{!InG Λ Σ i A} (γ : gid) (a : A) : iProp Λ (globalC Σ) :=
-  ownG (to_globalC i γ a).
 
 Section global.
 Context {Λ : language} {Σ : gid → iFunctor} (i : gid) `{!InG Λ Σ i A}.
 Implicit Types a : A.
 
-(* Proeprties of to_globalC *)
+Definition to_Σ (a : A) : Σ i (laterC (iPreProp Λ (globalC Σ))) :=
+  eq_rect A id a _ inG.
+Definition to_globalC (γ : gid) `{!InG Λ Σ i A} (a : A) : iGst Λ (globalC Σ) :=
+  iprod_singleton i {[ γ ↦ to_Σ a ]}.
+Definition own (γ : gid) (a : A) : iProp Λ (globalC Σ) :=
+  ownG (to_globalC γ a).
+
+Definition from_Σ (b : Σ i (laterC (iPreProp Λ (globalC Σ)))) : A  :=
+  eq_rect (Σ i _) id b _ (Logic.eq_sym inG).
+Definition P_to_Σ (P : A → Prop) (b : Σ i (laterC (iPreProp Λ (globalC Σ)))) : Prop
+  := P (from_Σ b).
+
+(* Properties of the transport. *)
+Lemma to_from_Σ b :
+  to_Σ (from_Σ b) = b.
+Proof.
+  rewrite /to_Σ /from_Σ. by destruct inG.
+Qed.
+
+(* Properties of to_globalC *)
 Lemma globalC_op γ a1 a2 :
-  to_globalC i γ (a1 ⋅ a2) ≡ to_globalC i γ a1 ⋅ to_globalC i γ a2.
+  to_globalC γ (a1 ⋅ a2) ≡ to_globalC γ a1 ⋅ to_globalC γ a2.
 Proof.
   rewrite /to_globalC iprod_op_singleton map_op_singleton.
   apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
@@ -32,7 +42,7 @@ Proof.
 Qed.
 
 Lemma globalC_validN n γ a :
-  ✓{n} (to_globalC i γ a) <-> ✓{n} a.
+  ✓{n} (to_globalC γ a) <-> ✓{n} a.
 Proof.
   rewrite /to_globalC.
   rewrite -iprod_validN_singleton -map_validN_singleton.
@@ -40,7 +50,7 @@ Proof.
 Qed.
 
 Lemma globalC_unit γ a :
-  unit (to_globalC i γ a) ≡ to_globalC i γ (unit a).
+  unit (to_globalC γ a) ≡ to_globalC γ (unit a).
 Proof.
   rewrite /to_globalC.
   rewrite iprod_unit_singleton map_unit_singleton.
@@ -48,57 +58,92 @@ Proof.
   by rewrite /to_Σ; destruct inG.
 Qed.
 
-Global Instance globalC_timeless γ m : Timeless m → Timeless (to_globalC i γ m).
+Global Instance globalC_timeless γ m : Timeless m → Timeless (to_globalC γ m).
 Proof.
   rewrite /to_globalC => ?.
   apply iprod_singleton_timeless, map_singleton_timeless.
   by rewrite /to_Σ; destruct inG.
 Qed.
 
+(* Properties of the lifted frame-preserving updates *)
+Lemma update_to_Σ a P :
+  a ~~>: P → to_Σ a ~~>: P_to_Σ P.
+Proof.
+  move=>Hu gf n Hf. destruct (Hu (from_Σ gf) n) as [a' Ha'].
+  { move: Hf. rewrite /to_Σ /from_Σ. by destruct inG. }
+  exists (to_Σ a'). move:Hf Ha'.
+  rewrite /P_to_Σ /to_Σ /from_Σ. destruct inG. done.
+Qed. 
+
 (* Properties of own *)
 
-Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ).
+Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
 Proof.
   intros m m' Hm; apply ownG_ne, iprod_singleton_ne, singleton_ne.
   by rewrite /to_globalC /to_Σ; destruct inG.
 Qed.
 
-Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper _.
+Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own γ) := ne_proper _.
 
-Lemma own_op γ a1 a2 : own i γ (a1 ⋅ a2) ≡ (own i γ a1 ★ own i γ a2)%I.
+Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ≡ (own γ a1 ★ own γ a2)%I.
 Proof. rewrite /own -ownG_op. apply ownG_proper, globalC_op. Qed.
 
 (* TODO: This also holds if we just have ✓a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
 Lemma own_alloc E a :
-  ✓a → True ⊑ pvs E E (∃ γ, own i γ a).
+  ✓a → True ⊑ pvs E E (∃ γ, own γ a).
 Proof.
-  intros Hm. set (P m := ∃ γ, m = to_globalC i γ a).
+  intros Ha. set (P m := ∃ γ, m = to_globalC γ a).
   rewrite -(pvs_mono _ _ (∃ m, ■P m ∧ ownG m)%I).
-  - rewrite -pvs_updateP_empty //; [].
+  - rewrite -pvs_ownG_updateP_empty //; [].
     subst P. eapply (iprod_singleton_updateP_empty i).
-    + eapply map_updateP_alloc' with (x:=to_Σ i a).
+    + apply map_updateP_alloc' with (x:=to_Σ a).
       by rewrite /to_Σ; destruct inG.
     + simpl. move=>? [γ [-> ?]]. exists γ. done.
-  - apply exist_elim=>m. apply const_elim_l.
-    move=>[p ->] {P}. by rewrite -(exist_intro p).
+  - apply exist_elim=>m. apply const_elim_l=>-[p ->] {P}.
+    by rewrite -(exist_intro p).
 Qed.
 
-Lemma always_own_unit γ m : (□ own i γ (unit m))%I ≡ own i γ (unit m).
+Lemma always_own_unit γ a : (□ own γ (unit a))%I ≡ own γ (unit a).
 Proof. rewrite /own -globalC_unit. by apply always_ownG_unit. Qed.
 
-Lemma own_valid γ m : (own i γ m) ⊑ (✓ m).
+Lemma own_valid γ a : (own γ a) ⊑ (✓ a).
 Proof.
   rewrite /own ownG_valid. apply uPred.valid_mono=>n.
   by apply globalC_validN.
 Qed.
 
-Lemma own_valid_r' γ m : (own i γ m) ⊑ (own i γ m ★ ✓ m).
+Lemma own_valid_r' γ a : (own γ a) ⊑ (own γ a ★ ✓ a).
 Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
 
-Global Instance ownG_timeless γ m : Timeless m → TimelessP (own i γ m).
+Global Instance ownG_timeless γ a : Timeless a → TimelessP (own γ a).
 Proof.
   intros. apply ownG_timeless. apply _.
 Qed.
 
+Lemma pvs_updateP E γ a P :
+  a ~~>: P → own γ a ⊑ pvs E E (∃ a', ■ P a' ∧ own γ a').
+Proof.
+  intros Ha. set (P' m := ∃ a', P a' ∧ m = to_globalC γ a').
+  rewrite -(pvs_mono _ _ (∃ m, ■P' m ∧ ownG m)%I).
+  - rewrite -pvs_ownG_updateP; first by rewrite /own.
+    rewrite /to_globalC. eapply iprod_singleton_updateP.
+    + (* FIXME RJ: I tried apply... with instead of instantiate, that
+         does not work. *)
+      apply map_singleton_updateP'. instantiate (1:=P_to_Σ P).
+      by apply update_to_Σ.
+    + simpl. move=>? [y [-> HP]]. exists (from_Σ y). split.
+      * move: HP. rewrite /P_to_Σ /from_Σ. by destruct inG.
+      * clear HP. rewrite /to_globalC to_from_Σ; done.
+  - apply exist_elim=>m. apply const_elim_l=>-[a' [HP ->]].
+    rewrite -(exist_intro a'). apply and_intro; last done.
+    by apply const_intro.
+Qed.
+
+Lemma pvs_update E γ a a' : a ~~> a' → own γ a ⊑ pvs E E (own γ a').
+Proof.
+  intros; rewrite (pvs_updateP E _ _ (a' =)); last by apply cmra_update_updateP.
+  by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
+Qed.
+
 End global.

program_logic/pviewshifts.v

@@ -97,7 +97,7 @@ Proof.
   * by rewrite -(left_id_L ∅ (∪) Ef).
   * apply uPred_weaken with r n; auto.
 Qed.
-Lemma pvs_updateP E m (P : iGst Λ Σ → Prop) :
+Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
   m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
 Proof.
   intros Hup%option_updateP' r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
@@ -105,7 +105,7 @@ Proof.
   { apply cmra_includedN_le with (S n); auto. }
   by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
 Qed.
-Lemma pvs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
+Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
     E (P : iGst Λ Σ → Prop) :
   ∅ ~~>: P → True ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
 Proof.
@@ -148,9 +148,9 @@ Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → pvs E1 E1 P ⊑ pvs E2 E2 P.
 Proof.
   intros; rewrite (union_difference_L E1 E2) //; apply pvs_mask_frame; auto.
 Qed.
-Lemma pvs_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m').
+Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m').
 Proof.
-  intros; rewrite (pvs_updateP E _ (m' =)); last by apply cmra_update_updateP.
+  intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
   by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
 Qed.
 End pvs.

program_logic/viewshifts.v

 Require Export program_logic.pviewshifts.
 Require Import program_logic.ownership.
 
+(* TODO: State lemmas in terms of inv and own. *)
+
 Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
   (□ (P → pvs E1 E2 Q))%I.
 Arguments vs {_ _} _ _ _%I _%I.
@@ -25,14 +27,18 @@ Proof.
   intros; rewrite -{1}always_const; apply always_intro, impl_intro_l.
   by rewrite always_const (right_id _ _).
 Qed.
+
 Global Instance vs_ne E1 E2 n :
   Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
 Proof. by intros P P' HP Q Q' HQ; rewrite /vs HP HQ. Qed.
+
 Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Λ Σ E1 E2).
 Proof. apply ne_proper_2, _. Qed.
+
 Lemma vs_mono E1 E2 P P' Q Q' :
   P ⊑ P' → Q' ⊑ Q → P' >{E1,E2}> Q' ⊑ P >{E1,E2}> Q.
 Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.
+
 Global Instance vs_mono' E1 E2 :
   Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@vs Λ Σ E1 E2).
 Proof. by intros until 2; apply vs_mono. Qed.
@@ -41,6 +47,7 @@ Lemma vs_false_elim E1 E2 P : False >{E1,E2}> P.
 Proof. apply vs_alt, False_elim. Qed.
 Lemma vs_timeless E P : TimelessP P → ▷ P >{E}> P.
 Proof. by intros ?; apply vs_alt, pvs_timeless. Qed.
+
 Lemma vs_transitive E1 E2 E3 P Q R :
   E2 ⊆ E1 ∪ E3 → (P >{E1,E2}> Q ∧ Q >{E2,E3}> R) ⊑ P >{E1,E3}> R.
 Proof.
@@ -48,54 +55,67 @@ Proof.
   rewrite always_and (associative _) (always_elim (P → _)) impl_elim_r.
   by rewrite pvs_impl_r; apply pvs_trans.
 Qed.
+
 Lemma vs_transitive' E P Q R : (P >{E}> Q ∧ Q >{E}> R) ⊑ P >{E}> R.
 Proof. apply vs_transitive; solve_elem_of. Qed.
 Lemma vs_reflexive E P : P >{E}> P.
 Proof. apply vs_alt, pvs_intro. Qed.
+
 Lemma vs_impl E P Q : □ (P → Q) ⊑ P >{E}> Q.
 Proof.
   apply always_intro, impl_intro_l.
   by rewrite always_elim impl_elim_r -pvs_intro.
 Qed.
+
 Lemma vs_frame_l E1 E2 P Q R : P >{E1,E2}> Q ⊑ (R ★ P) >{E1,E2}> (R ★ Q).
 Proof.
   apply always_intro, impl_intro_l.
   rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -(associative _).
   by rewrite always_elim wand_elim_r.
 Qed.
+
 Lemma vs_frame_r E1 E2 P Q R : P >{E1,E2}> Q ⊑ (P ★ R) >{E1,E2}> (Q ★ R).
 Proof. rewrite !(commutative _ _ R); apply vs_frame_l. Qed.
+
 Lemma vs_mask_frame E1 E2 Ef P Q :
   Ef ∩ (E1 ∪ E2) = ∅ → P >{E1,E2}> Q ⊑ P >{E1 ∪ Ef,E2 ∪ Ef}> Q.
 Proof.
   intros ?; apply always_intro, impl_intro_l; rewrite (pvs_mask_frame _ _ Ef)//.
   by rewrite always_elim impl_elim_r.
 Qed.
+
 Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → P >{E}> Q ⊑ P >{E ∪ Ef}> Q.
 Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
 Lemma vs_open i P : ownI i P >{{[i]},∅}> ▷ P.
 Proof. intros; apply vs_alt, pvs_open. Qed.
+
 Lemma vs_open' E i P : i ∉ E → ownI i P >{{[i]} ∪ E,E}> ▷ P.
 Proof.
   intros; rewrite -{2}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of.
   apply vs_open.
 Qed.
+
 Lemma vs_close i P : (ownI i P ∧ ▷ P) >{∅,{[i]}}> True.
 Proof. intros; apply vs_alt, pvs_close. Qed.
+
 Lemma vs_close' E i P : i ∉ E → (ownI i P ∧ ▷ P) >{E,{[i]} ∪ E}> True.
 Proof.
   intros; rewrite -{1}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of.
   apply vs_close.
 Qed.
-Lemma vs_updateP E m (P : iGst Λ Σ → Prop) :
+
+Lemma vs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
   m ~~>: P → ownG m >{E}> (∃ m', ■ P m' ∧ ownG m').
-Proof. by intros; apply vs_alt, pvs_updateP. Qed.
-Lemma vs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
+Proof. by intros; apply vs_alt, pvs_ownG_updateP. Qed.
+
+Lemma vs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
     E (P : iGst Λ Σ → Prop) :
   ∅ ~~>: P → True >{E}> (∃ m', ■ P m' ∧ ownG m').
-Proof. by intros; apply vs_alt, pvs_updateP_empty. Qed.
+Proof. by intros; apply vs_alt, pvs_ownG_updateP_empty. Qed.
+
 Lemma vs_update E m m' : m ~~> m' → ownG m >{E}> ownG m'.
-Proof. by intros; apply vs_alt, pvs_update. Qed.
+Proof. by intros; apply vs_alt, pvs_ownG_update. Qed.
 Lemma vs_alloc E P : ¬set_finite E → ▷ P >{E}> (∃ i, ■ (i ∈ E) ∧ ownI i P).
 Proof. by intros; apply vs_alt, pvs_alloc. Qed.
+
 End vs.