global_cmra.v 3.59 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
Require Export algebra.iprod program_logic.pviewshifts.
Require Import program_logic.ownership.
3
4
5
Import uPred.

Definition gid := positive.
Ralf Jung's avatar
Ralf Jung committed
6
7
Definition globalC (Σ : gid  iFunctor) : iFunctor :=
  iprodF (λ i, mapF gid (Σ i)).
8

Ralf Jung's avatar
Ralf Jung committed
9
10
11
12
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 Σ))) :=
13
  eq_rect A id a _ inG.
Ralf Jung's avatar
Ralf Jung committed
14
15
16
17
18
19
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).
20
21

Section global.
Ralf Jung's avatar
Ralf Jung committed
22
Context {Λ : language} {Σ : gid  iFunctor} (i : gid) `{!InG Λ Σ i A}.
23
24
Implicit Types a : A.

25
26
27
28
29
30
(* 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 _)).
Ralf Jung's avatar
Ralf Jung committed
31
  by rewrite /to_Σ; destruct inG.
32
33
34
35
36
37
38
Qed.

Lemma globalC_validN n γ a :
  {n} (to_globalC i γ a) <-> {n} a.
Proof.
  rewrite /to_globalC.
  rewrite -iprod_validN_singleton -map_validN_singleton.
Ralf Jung's avatar
Ralf Jung committed
39
  by rewrite /to_Σ; destruct inG.
40
41
Qed.

42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
Lemma globalC_unit γ a :
  unit (to_globalC i γ a)  to_globalC i γ (unit a).
Proof.
  rewrite /to_globalC.
  rewrite iprod_unit_singleton map_unit_singleton.
  apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
  by rewrite /to_Σ; destruct inG.
Qed.

Global Instance globalC_timeless γ m : Timeless m  Timeless (to_globalC i γ m).
Proof.
  rewrite /to_globalC => ?.
  apply iprod_singleton_timeless, map_singleton_timeless.
  by rewrite /to_Σ; destruct inG.
Qed.

58
59
(* Properties of own *)

60
61
62
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.
Ralf Jung's avatar
Ralf Jung committed
63
  by rewrite /to_globalC /to_Σ; destruct inG.
64
65
66
67
68
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.
69
Proof. rewrite /own -ownG_op. apply ownG_proper, globalC_op. Qed.
70
71
72
73

(* 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 :
Ralf Jung's avatar
Ralf Jung committed
74
  a  True  pvs E E ( γ, own i γ a).
75
Proof.
Ralf Jung's avatar
Ralf Jung committed
76
  intros Hm. set (P m :=  γ, m = to_globalC i γ a).
77
78
79
  rewrite -(pvs_mono _ _ ( m, P m  ownG m)%I).
  - rewrite -pvs_updateP_empty //; [].
    subst P. eapply (iprod_singleton_updateP_empty i).
Ralf Jung's avatar
Ralf Jung committed
80
81
    + eapply map_updateP_alloc' with (x:=to_Σ i a).
      by rewrite /to_Σ; destruct inG.
82
83
84
    + simpl. move=>? [γ [-> ?]]. exists γ. done.
  - apply exist_elim=>m. apply const_elim_l.
    move=>[p ->] {P}. by rewrite -(exist_intro p).
85
Qed.
86
87

Lemma always_own_unit γ m : ( own i γ (unit m))%I  own i γ (unit m).
88
Proof. rewrite /own -globalC_unit. by apply always_ownG_unit. Qed.
89
90
91

Lemma own_valid γ m : (own i γ m)  ( m).
Proof.
92
93
94
  rewrite /own ownG_valid. apply uPred.valid_mono=>n.
  by apply globalC_validN.
Qed.
95
96
97
98
99
100

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.
101
102
  intros. apply ownG_timeless. apply _.
Qed.
103
104

End global.