dra.v 9.11 KB
Newer Older
1
From iris.algebra Require Export cmra updates.
2
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
3

4
Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
5
  (* setoids *)
6 7 8 9 10
  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
11
  (* validity *)
12 13
  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
14
  (* monoid *)
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;
24
  mixin_dra_core_mono x y : 
Robbert Krebbers's avatar
Robbert Krebbers committed
25
     z,  x   y  x  y  core (x  y)  core x  z   z  core x  z
Robbert Krebbers's avatar
Robbert Krebbers committed
26
}.
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
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
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
(** 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.
82
  Lemma dra_core_mono x y : 
83
     z,  x   y  x  y  core (x  y)  core x  z   z  core x  z.
84
  Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
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
101
Section dra.
102 103 104
Context (A : draT).
Implicit Types a b : A.
Implicit Types x y z : validity A.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
Arguments valid _ _ !_ /.
106

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

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

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.
134
Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
135 136
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
137
Proof.
138 139
  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
140
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
142

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

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

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

183 184
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
185
Proof.
186 187
  intros Hxy; apply cmra_discrete_update=> z [?[??]].
  split_and!; try eapply Hxy; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
Qed.
189

190 191 192 193
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.
194

195
(* TODO: This has to be proven again. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
196
(*
197 198 199 200 201
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
202 203
    destruct Hvl' as [? [? ?]]; split; first done.
    exists (validity_car z); eauto.
204
  - intros (Hvl & z & EQ & ? & ?).
Robbert Krebbers's avatar
Robbert Krebbers committed
205
    assert (✓ y) by (rewrite EQ; by apply dra_op_valid).
206
    split; first done. exists (to_validity z). split; first split.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
    + intros _. simpl. by split_and!.
208 209 210
    + intros _. setoid_subst. by apply dra_op_valid. 
    + intros _. rewrite /= EQ //.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
212
End dra.