global_cmra.v 3.1 KB
Newer Older
1
Require Export algebra.iprod program_logic.ownership program_logic.pviewshifts.
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
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 Δ) :=
18
  ownG (Σ:=globalC Δ) (to_globalC i γ a).
19 20 21 22 23

Section global.
Context {Λ : language} {Δ : gid  iFunctor} (i : gid) `{!InG Λ Δ i A}.
Implicit Types a : A.

24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
(* Proeprties of to_globalC *)
Lemma globalC_op γ a1 a2 :
  to_globalC i γ (a1  a2)  to_globalC i γ a1  to_globalC i γ a2.
Proof.
  rewrite /to_globalC iprod_op_singleton map_op_singleton.
  apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
  by rewrite /to_funC; destruct inG.
Qed.

Lemma globalC_validN n γ a :
  {n} (to_globalC i γ a) <-> {n} a.
Proof.
  rewrite /to_globalC.
  rewrite -iprod_validN_singleton -map_validN_singleton.
  by rewrite /to_funC; destruct inG.
Qed.

(* Properties of own *)

43 44 45
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.
46
  by rewrite /to_globalC /to_funC; destruct inG.
47 48 49 50 51
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.
52
Proof. rewrite /own -ownG_op. apply ownG_proper, globalC_op. Qed.
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67

(* 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).
68
Qed.
69 70 71 72 73 74 75 76

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.
77 78 79
  rewrite /own ownG_valid. apply uPred.valid_mono=>n.
  by apply globalC_validN.
Qed.
80 81 82 83 84 85 86 87 88 89

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.
Admitted.

End global.