dra.v 9.1 KB
Newer Older
1
From iris.algebra Require Export cmra updates.
Robbert Krebbers's avatar
Robbert Krebbers committed
2

3
Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
4
  (* setoids *)
5 6 7 8 9
  mixin_dra_equivalence : Equivalence (() : relation A);
  mixin_dra_op_proper : Proper (() ==> () ==> ()) ();
  mixin_dra_core_proper : Proper (() ==> ()) core;
  mixin_dra_valid_proper : Proper (() ==> impl) valid;
  mixin_dra_disjoint_proper x : Proper (() ==> impl) (disjoint x);
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  (* validity *)
11 12
  mixin_dra_op_valid x y :  x   y  x  y   (x  y);
  mixin_dra_core_valid x :  x   core x;
Robbert Krebbers's avatar
Robbert Krebbers committed
13
  (* monoid *)
14 15 16 17 18 19 20 21 22 23
  mixin_dra_assoc : Assoc () ();
  mixin_dra_disjoint_ll x y z :  x   y   z  x  y  x  y  z  x  z;
  mixin_dra_disjoint_move_l x y z :
     x   y   z  x  y  x  y  z  x  y  z;
  mixin_dra_symmetric : Symmetric (@disjoint A _);
  mixin_dra_comm x y :  x   y  x  y  x  y  y  x;
  mixin_dra_core_disjoint_l x :  x  core x  x;
  mixin_dra_core_l x :  x  core x  x  x;
  mixin_dra_core_idemp x :  x  core (core x)  core x;
  mixin_dra_core_preserving x y : 
Robbert Krebbers's avatar
Robbert Krebbers committed
24
     z,  x   y  x  y  core (x  y)  core x  z   z  core x  z
Robbert Krebbers's avatar
Robbert Krebbers committed
25
}.
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
Structure draT := DRAT {
  dra_car :> Type;
  dra_equiv : Equiv dra_car;
  dra_core : Core dra_car;
  dra_disjoint : Disjoint dra_car;
  dra_op : Op dra_car;
  dra_valid : Valid dra_car;
  dra_mixin : DRAMixin dra_car
}.
Arguments DRAT _ {_ _ _ _ _} _.
Arguments dra_car : simpl never.
Arguments dra_equiv : simpl never.
Arguments dra_core : simpl never.
Arguments dra_disjoint : simpl never.
Arguments dra_op : simpl never.
Arguments dra_valid : simpl never.
Arguments dra_mixin : simpl never.
Add Printing Constructor draT.
Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
45

46 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 88 89 90 91 92 93 94 95 96 97 98 99
(** Lifting properties from the mixin *)
Section dra_mixin.
  Context {A : draT}.
  Implicit Types x y : A.
  Global Instance dra_equivalence : Equivalence (() : relation A).
  Proof. apply (mixin_dra_equivalence _ (dra_mixin A)). Qed.
  Global Instance dra_op_proper : Proper (() ==> () ==> ()) (@op A _).
  Proof. apply (mixin_dra_op_proper _ (dra_mixin A)). Qed.
  Global Instance dra_core_proper : Proper (() ==> ()) (@core A _).
  Proof. apply (mixin_dra_core_proper _ (dra_mixin A)). Qed.
  Global Instance dra_valid_proper : Proper (() ==> impl) (@valid A _).
  Proof. apply (mixin_dra_valid_proper _ (dra_mixin A)). Qed.
  Global Instance dra_disjoint_proper x : Proper (() ==> impl) (disjoint x).
  Proof. apply (mixin_dra_disjoint_proper _ (dra_mixin A)). Qed.
  Lemma dra_op_valid x y :  x   y  x  y   (x  y).
  Proof. apply (mixin_dra_op_valid _ (dra_mixin A)). Qed.
  Lemma dra_core_valid x :  x   core x.
  Proof. apply (mixin_dra_core_valid _ (dra_mixin A)). Qed.
  Global Instance dra_assoc : Assoc () (@op A _).
  Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed.
  Lemma dra_disjoint_ll x y z :  x   y   z  x  y  x  y  z  x  z.
  Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed.
  Lemma dra_disjoint_move_l x y z :
     x   y   z  x  y  x  y  z  x  y  z.
  Proof. apply (mixin_dra_disjoint_move_l _ (dra_mixin A)). Qed.
  Global Instance  dra_symmetric : Symmetric (@disjoint A _).
  Proof. apply (mixin_dra_symmetric _ (dra_mixin A)). Qed.
  Lemma dra_comm x y :  x   y  x  y  x  y  y  x.
  Proof. apply (mixin_dra_comm _ (dra_mixin A)). Qed.
  Lemma dra_core_disjoint_l x :  x  core x  x.
  Proof. apply (mixin_dra_core_disjoint_l _ (dra_mixin A)). Qed.
  Lemma dra_core_l x :  x  core x  x  x.
  Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
  Lemma dra_core_idemp x :  x  core (core x)  core x.
  Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
  Lemma dra_core_preserving x y : 
     z,  x   y  x  y  core (x  y)  core x  z   z  core x  z.
  Proof. apply (mixin_dra_core_preserving _ (dra_mixin A)). Qed.
End dra_mixin.

Record validity (A : draT) := Validity {
  validity_car : A;
  validity_is_valid : Prop;
  validity_prf : validity_is_valid  valid validity_car
}.
Add Printing Constructor validity.
Arguments Validity {_} _ _ _.
Arguments validity_car {_} _.
Arguments validity_is_valid {_} _.

Definition to_validity {A : draT} (x : A) : validity A :=
  Validity x (valid x) id.

(* The actual construction *)
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Section dra.
101 102 103
Context (A : draT).
Implicit Types a b : A.
Implicit Types x y z : validity A.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
Arguments valid _ _ !_ /.
105

106 107
Instance validity_valid : Valid (validity A) := validity_is_valid.
Instance validity_equiv : Equiv (validity A) := λ x y,
108
  (valid x  valid y)  (valid x  validity_car x  validity_car y).
109
Instance validity_equivalence : Equivalence (@equiv (validity A) _).
110 111
Proof.
  split; unfold equiv, validity_equiv.
112 113 114
  - by intros [x px ?]; simpl.
  - intros [x px ?] [y py ?]; naive_solver.
  - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
115
    split; [|intros; trans y]; tauto.
116
Qed.
117 118
Canonical Structure validityC : cofeT := discreteC (validity A).

Robbert Krebbers's avatar
Robbert Krebbers committed
119
Instance dra_valid_proper' : Proper (() ==> iff) (valid : A  Prop).
120 121
Proof. by split; apply: dra_valid_proper. Qed.
Global Instance to_validity_proper : Proper (() ==> ()) to_validity.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
123
Instance: Proper (() ==> () ==> iff) (disjoint : relation A).
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Proof.
125
  intros x1 x2 Hx y1 y2 Hy; split.
126 127
  - by rewrite Hy (symmetry_iff () x1) (symmetry_iff () x2) Hx.
  - by rewrite -Hy (symmetry_iff () x2) (symmetry_iff () x1) -Hx.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
Qed.
129 130 131 132

Lemma dra_disjoint_rl a b c :  a   b   c  b  c  a  b  c  a  b.
Proof. intros ???. rewrite !(symmetry_iff _ a). by apply dra_disjoint_ll. Qed.
Lemma dra_disjoint_lr a b c :  a   b   c  a  b  a  b  c  b  c.
133
Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
134 135
Lemma dra_disjoint_move_r a b c :
   a   b   c  b  c  a  b  c  a  b  c.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
Proof.
137 138
  intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
  apply dra_disjoint_move_l; auto; by rewrite dra_comm.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Qed.
140
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
141

142
Lemma validity_valid_car_valid z :  z   validity_car z.
Robbert Krebbers's avatar
Robbert Krebbers committed
143 144
Proof. apply validity_prf. Qed.
Hint Resolve validity_valid_car_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146
Program Instance validity_pcore : PCore (validity A) := λ x,
  Some (Validity (core (validity_car x)) ( x) _).
147 148
Solve Obligations with naive_solver eauto using dra_core_valid.
Program Instance validity_op : Op (validity A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  Validity (validity_car x  validity_car y)
Robbert Krebbers's avatar
Robbert Krebbers committed
150
           ( x   y  validity_car x  validity_car y) _.
151
Solve Obligations with naive_solver eauto using dra_op_valid.
152

153
Definition validity_ra_mixin : RAMixin (validity A).
Robbert Krebbers's avatar
Robbert Krebbers committed
154
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
  apply ra_total_mixin; first eauto.
156
  - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
157
    split; intros (?&?&?); split_and!;
158
      first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
159 160 161
  - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
  - intros ?? [??]; naive_solver.
  - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
162
      [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
163
      |intros; by rewrite assoc].
164 165
  - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
  - intros [x px ?]; split;
Ralf Jung's avatar
Ralf Jung committed
166 167
      naive_solver eauto using dra_core_l, dra_core_disjoint_l.
  - intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
168 169 170 171 172 173
  - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
    destruct (dra_core_preserving x z) as (z'&Hz').
    unshelve eexists (Validity z' (px  py  pz) _); [|split; simpl].
    { intros (?&?&?); apply Hz'; tauto. }
    + tauto.
    + intros. rewrite Hy //. tauto.
174
  - by intros [x px ?] [y py ?] (?&?&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
175
Qed.
176 177
Canonical Structure validityR : cmraT :=
  discreteR (validity A) validity_ra_mixin.
178

Robbert Krebbers's avatar
Robbert Krebbers committed
179 180 181
Global Instance validity_cmra_total : CMRATotal validityR.
Proof. rewrite /CMRATotal; eauto. Qed.

182 183
Lemma validity_update x y :
  ( c,  x   c  validity_car x  c   y  validity_car y  c)  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
184
Proof.
185 186
  intros Hxy; apply cmra_discrete_update=> z [?[??]].
  split_and!; try eapply Hxy; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
187
Qed.
188

189 190 191 192
Lemma to_validity_op a b :
  ( (a  b)   a   b  a  b) 
  to_validity (a  b)  to_validity a  to_validity b.
Proof. split; naive_solver eauto using dra_op_valid. Qed.
193

194
(* TODO: This has to be proven again. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
195
(*
196 197 198 199 200
Lemma to_validity_included x y:
  (✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y).
Proof.
  split.
  - move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'.
Robbert Krebbers's avatar
Robbert Krebbers committed
201 202
    destruct Hvl' as [? [? ?]]; split; first done.
    exists (validity_car z); eauto.
203
  - intros (Hvl & z & EQ & ? & ?).
Robbert Krebbers's avatar
Robbert Krebbers committed
204
    assert (✓ y) by (rewrite EQ; by apply dra_op_valid).
205
    split; first done. exists (to_validity z). split; first split.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
    + intros _. simpl. by split_and!.
207 208 209
    + intros _. setoid_subst. by apply dra_op_valid. 
    + intros _. rewrite /= EQ //.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
211
End dra.