local_updates.v 5.79 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 51 52 53 54 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
  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.
88 89
End updates.

90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
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.
End updates_unital.

114
(** * Product *)
115 116 117
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').
118
Proof.
119 120 121 122
  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.
123 124
Qed.

125 126 127 128 129 130 131 132 133 134 135
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.

136
(** * Option *)
137 138 139
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').
140
Proof.
141 142 143 144
  intros Hup n mmz Hxv Hx; simpl in *.
  destruct (Hup n (mjoin mmz)); first done.
  { destruct mmz as [[?|]|]; inversion_clear Hx; auto. }
  split; first done. destruct mmz as [[?|]|]; constructor; auto.
145 146 147
Qed.

(** * Natural numbers  *)
148 149
Lemma nat_local_update (x y x' y' : nat) :
  x + y' = x' + y  (x,y) ~l~> (x',y').
150
Proof.
151 152
  intros ??; apply local_update_unital_discrete=> z _.
  compute -[minus plus]; lia.
153 154
Qed.

155 156
Lemma mnat_local_update (x y x' : mnatUR) :
  x  x'  (x,y) ~l~> (x',x').
157
Proof.
158 159
  intros ??; apply local_update_unital_discrete=> z _.
  compute -[max]; lia.
160
Qed.