add Robbert's global.v, change some names around, and prove allocation

_CoqProject

@@ -63,6 +63,7 @@ program_logic/resources.v
 program_logic/hoare.v
 program_logic/language.v
 program_logic/tests.v
+program_logic/global_cmra.v
 heap_lang/heap_lang.v
 heap_lang/heap_lang_tactics.v
 heap_lang/lifting.v

program_logic/global_cmra.v

+Require Export program_logic.ownership program_logic.pviewshifts.
+Import uPred.
+
+Definition gid := positive.
+Definition globalC (Δ : gid → iFunctor) : iFunctor :=
+  iprodF (λ i, mapF gid (Δ i)).
+
+Class InG Λ (Δ : gid → iFunctor) (i : gid) (A : cmraT) :=
+  inG : A = Δ i (laterC (iPreProp Λ (globalC Δ))).
+Definition to_funC {Λ} {Δ : 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_funC _ a ]}.
+Definition own {Λ} {Δ : gid → iFunctor}
+    (i : gid) `{!InG Λ Δ i A} (γ : gid) (a : A) : iProp Λ (globalC Δ) :=
+  ownG (Σ:=globalC Δ) (iprod_singleton i {[ γ ↦ to_funC _ a ]}).
+
+Section global.
+Context {Λ : language} {Δ : gid → iFunctor} (i : gid) `{!InG Λ Δ i A}.
+Implicit Types a : A.
+
+Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ).
+Proof.
+  intros m m' Hm; apply ownG_ne, iprod_singleton_ne, singleton_ne.
+  by rewrite /to_funC; destruct inG.
+Qed.
+
+Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper _.
+
+Lemma own_op γ a1 a2 : own i γ (a1 ⋅ a2) ≡ (own i γ a1 ★ own i γ a2)%I.
+Proof.
+  rewrite /own -ownG_op iprod_op_singleton map_op_singleton.
+  apply ownG_proper, iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
+  by rewrite /to_funC; destruct inG.
+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).
+Proof.
+  intros Hm. set (P m := ∃ γ, m = to_globalC (Δ:=Δ) i γ a).
+  rewrite -(pvs_mono _ _ (∃ m, ■P m ∧ ownG m)%I).
+  - rewrite -pvs_updateP_empty //; [].
+    subst P. eapply (iprod_singleton_updateP_empty i).
+    + eapply map_updateP_alloc' with (x:=to_funC i a).
+      by rewrite /to_funC; destruct inG.
+    + simpl. move=>? [γ [-> ?]]. exists γ. done.
+  - apply exist_elim=>m. apply const_elim_l.
+    move=>[p ->] {P}. by rewrite -(exist_intro p).
+Qed.      
+
+Lemma always_own_unit γ m : (□ own i γ (unit m))%I ≡ own i γ (unit m).
+Proof.
+  rewrite /own.
+Admitted.
+
+Lemma own_valid γ m : (own i γ m) ⊑ (✓ m).
+Proof.
+  rewrite /own ownG_valid; apply uPred.valid_mono.
+intros n ?.
+SearchAbout validN singletonM.
+Admitted.
+
+Lemma own_valid_r' γ m : (own i γ m) ⊑ (own i γ m ★ ✓ m).
+Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
+
+Global Instance ownG_timeless γ m : Timeless m → TimelessP (own i γ m).
+Proof.
+  intros. apply ownG_timeless.
+SearchAbout singletonM Timeless.
+Admitted.
+
+End global.