local_updates.v 6.92 KB
Newer Older
1
From iris.algebra Require Export cmra.
2
Set Default Proof Using "Type".
3
4

(** * Local updates *)
5
6
Definition local_update {A : cmraT} (x y : A * A) :=  n mz,
  {n} x.1  x.1 {n} x.2 ? mz  {n} y.1  y.1 {n} y.2 ? mz.
7
Instance: Params (@local_update) 1.
8
Infix "~l~>" := local_update (at level 70).
9
10

Section updates.
11
12
  Context {A : cmraT}.
  Implicit Types x y : A.
13

14
15
16
  Global Instance local_update_proper :
    Proper (() ==> () ==> iff) (@local_update A).
  Proof. unfold local_update. by repeat intro; setoid_subst. Qed.
17

18
19
  Global Instance local_update_preorder : PreOrder (@local_update A).
  Proof. split; unfold local_update; red; naive_solver. Qed.
20

21
22
23
24
25
26
  Lemma exclusive_local_update `{!Exclusive y} x x' :  x'  (x,y) ~l~> (x',x').
  Proof.
    intros ? n mz Hxv Hx; simpl in *.
    move: Hxv; rewrite Hx; move=> /exclusiveN_opM=> ->; split; auto.
    by apply cmra_valid_validN.
  Qed.
27

28
29
30
31
32
33
34
35
36
37
38
  Lemma op_local_update x y z :
    ( n, {n} x  {n} (z  x))  (x,y) ~l~> (z  x, z  y).
  Proof.
    intros Hv n mz Hxv Hx; simpl in *; split; [by auto|].
    by rewrite Hx -cmra_opM_assoc.
  Qed.
  Lemma op_local_update_discrete `{!CMRADiscrete A} x y z :
    ( x   (z  x))  (x,y) ~l~> (z  x, z  y).
  Proof.
    intros; apply op_local_update=> n. by rewrite -!(cmra_discrete_valid_iff n).
  Qed.
39

40
41
42
43
44
45
46
  Lemma op_local_update_frame x y x' y' yf :
    (x,y) ~l~> (x',y')  (x,y  yf) ~l~> (x', y'  yf).
  Proof.
    intros Hup n mz Hxv Hx; simpl in *.
    destruct (Hup n (Some (yf ? mz))); [done|by rewrite /= -cmra_opM_assoc|].
    by rewrite cmra_opM_assoc.
  Qed.
47

48
49
50
  Lemma cancel_local_update x y z `{!Cancelable x} :
    (x  y, x  z) ~l~> (y, z).
  Proof.
51
    intros n f ? Heq. split; first by eapply cmra_validN_op_r.
52
53
54
    apply (cancelableN x); first done. by rewrite -cmra_opM_assoc.
  Qed.

55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
  Lemma local_update_discrete `{!CMRADiscrete A} (x y x' y' : A) :
    (x,y) ~l~> (x',y')   mz,  x  x  y ? mz   x'  x'  y' ? mz.
  Proof.
    rewrite /local_update /=. setoid_rewrite <-cmra_discrete_valid_iff.
    setoid_rewrite <-(λ n, timeless_iff n x).
    setoid_rewrite <-(λ n, timeless_iff n x'). naive_solver eauto using 0.
  Qed.

  Lemma local_update_valid0 x y x' y' :
    ({0} x  {0} y  x {0} y  y {0} x  (x,y) ~l~> (x',y')) 
    (x,y) ~l~> (x',y').
  Proof.
    intros Hup n mz Hmz Hz; simpl in *. apply Hup; auto.
    - by apply (cmra_validN_le n); last lia.
    - apply (cmra_validN_le n); last lia.
      move: Hmz; rewrite Hz. destruct mz; simpl; eauto using cmra_validN_op_l.
    - destruct mz as [z|].
      + right. exists z. apply dist_le with n; auto with lia.
      + left. apply dist_le with n; auto with lia.
  Qed.
  Lemma local_update_valid `{!CMRADiscrete A} x y x' y' :
    ( x   y  x  y  y  x  (x,y) ~l~> (x',y'))  (x,y) ~l~> (x',y').
  Proof.
    rewrite !(cmra_discrete_valid_iff 0)
      (cmra_discrete_included_iff 0) (timeless_iff 0).
    apply local_update_valid0.
  Qed.

  Lemma local_update_total_valid0 `{!CMRATotal A} x y x' y' :
    ({0} x  {0} y  y {0} x  (x,y) ~l~> (x',y'))  (x,y) ~l~> (x',y').
  Proof.
    intros Hup. apply local_update_valid0=> ?? [Hx|?]; apply Hup; auto.
    by rewrite Hx.
  Qed.
  Lemma local_update_total_valid `{!CMRATotal A, !CMRADiscrete A} x y x' y' :
    ( x   y  y  x  (x,y) ~l~> (x',y'))  (x,y) ~l~> (x',y').
  Proof.
    rewrite !(cmra_discrete_valid_iff 0) (cmra_discrete_included_iff 0).
    apply local_update_total_valid0.
  Qed.
95
96
End updates.

97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
Section updates_unital.
  Context {A : ucmraT}.
  Implicit Types x y : A.

  Lemma local_update_unital x y x' y' :
    (x,y) ~l~> (x',y')   n z,
      {n} x  x {n} y  z  {n} x'  x' {n} y'  z.
  Proof.
    split.
    - intros Hup n z. apply (Hup _ (Some z)).
    - intros Hup n [z|]; simpl; [by auto|].
      rewrite -(right_id  op y) -(right_id  op y'). auto.
  Qed.

  Lemma local_update_unital_discrete `{!CMRADiscrete A} (x y x' y' : A) :
    (x,y) ~l~> (x',y')   z,  x  x  y  z   x'  x'  y'  z.
  Proof.
    rewrite local_update_discrete. split.
    - intros Hup z. apply (Hup (Some z)).
    - intros Hup [z|]; simpl; [by auto|].
      rewrite -(right_id  op y) -(right_id  op y'). auto.
  Qed.
119
120
121

  Lemma cancel_local_update_empty x y `{!Cancelable x} :
    (x  y, x) ~l~> (y, ).
122
  Proof. rewrite -{2}(right_id  op x). by apply cancel_local_update. Qed.
123
124
End updates_unital.

125
(** * Product *)
126
127
128
Lemma prod_local_update {A B : cmraT} (x y x' y' : A * B) :
  (x.1,y.1) ~l~> (x'.1,y'.1)  (x.2,y.2) ~l~> (x'.2,y'.2) 
  (x,y) ~l~> (x',y').
129
Proof.
130
131
132
133
  intros Hup1 Hup2 n mz [??] [??]; simpl in *.
  destruct (Hup1 n (fst <$> mz)); [done|by destruct mz|].
  destruct (Hup2 n (snd <$> mz)); [done|by destruct mz|].
  by destruct mz.
134
135
Qed.

136
137
138
139
140
141
142
143
144
145
146
Lemma prod_local_update' {A B : cmraT} (x1 y1 x1' y1' : A) (x2 y2 x2' y2' : B) :
  (x1,y1) ~l~> (x1',y1')  (x2,y2) ~l~> (x2',y2') 
  ((x1,x2),(y1,y2)) ~l~> ((x1',x2'),(y1',y2')).
Proof. intros. by apply prod_local_update. Qed.
Lemma prod_local_update_1 {A B : cmraT} (x1 y1 x1' y1' : A) (x2 y2 : B) :
  (x1,y1) ~l~> (x1',y1')  ((x1,x2),(y1,y2)) ~l~> ((x1',x2),(y1',y2)).
Proof. intros. by apply prod_local_update. Qed.
Lemma prod_local_update_2 {A B : cmraT} (x1 y1 : A) (x2 y2 x2' y2' : B) :
  (x2,y2) ~l~> (x2',y2')  ((x1,x2),(y1,y2)) ~l~> ((x1,x2'),(y1,y2')).
Proof. intros. by apply prod_local_update. Qed.

147
(** * Option *)
148
149
(* TODO: Investigate whether we can use these in proving the very similar local
   updates on finmaps. *)
150
151
152
Lemma option_local_update {A : cmraT} (x y x' y' : A) :
  (x, y) ~l~> (x',y') 
  (Some x, Some y) ~l~> (Some x', Some y').
153
Proof.
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
  intros Hup. apply local_update_unital=>n mz Hxv Hx; simpl in *.
  destruct (Hup n mz); first done.
  { destruct mz as [?|]; inversion_clear Hx; auto. }
  split; first done. destruct mz as [?|]; constructor; auto.
Qed.

Lemma alloc_option_local_update {A : cmraT} (x : A) y :
   x 
  (None, y) ~l~> (Some x, Some x).
Proof.
  move=>Hx. apply local_update_unital=> n z _ /= Heq. split.
  { rewrite Some_validN. apply cmra_valid_validN. done. }
  destruct z as [z|]; last done. destruct y; inversion Heq.
Qed.

Lemma delete_option_local_update {A : cmraT} (x y : A) :
  Exclusive y 
  (Some x, Some y) ~l~> (None, None).
Proof.
  move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
  destruct z as [z|]; last done. exfalso.
  move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
  eapply cmra_validN_le. eapply Hy. omega.
177
178
179
Qed.

(** * Natural numbers  *)
180
181
Lemma nat_local_update (x y x' y' : nat) :
  x + y' = x' + y  (x,y) ~l~> (x',y').
182
Proof.
183
184
  intros ??; apply local_update_unital_discrete=> z _.
  compute -[minus plus]; lia.
185
186
Qed.

187
188
Lemma mnat_local_update (x y x' : mnatUR) :
  x  x'  (x,y) ~l~> (x',x').
189
Proof.
190
191
  intros ??; apply local_update_unital_discrete=> z _.
  compute -[max]; lia.
192
Qed.