dra.v 9.35 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
  mixin_dra_op_valid x y :  x   y  x ## y   (x  y);
13
  mixin_dra_core_valid x :  x   core x;
Robbert Krebbers's avatar
Robbert Krebbers committed
14
  (* monoid *)
15
  mixin_dra_assoc x y z :
16 17
     x   y   z  x ## y  x  y ## z  x  (y  z)  (x  y)  z;
  mixin_dra_disjoint_ll x y z :  x   y   z  x ## y  x  y ## z  x ## z;
18
  mixin_dra_disjoint_move_l x y z :
19
     x   y   z  x ## y  x  y ## z  x ## y  z;
20
  mixin_dra_symmetric : Symmetric (@disjoint A _);
21 22
  mixin_dra_comm x y :  x   y  x ## y  x  y  y  x;
  mixin_dra_core_disjoint_l x :  x  core x ## x;
23 24
  mixin_dra_core_l x :  x  core x  x  x;
  mixin_dra_core_idemp x :  x  core (core x)  core x;
25
  mixin_dra_core_mono x y : 
26
     z,  x   y  x ## y  core (x  y)  core x  z   z  core x ## z
Robbert Krebbers's avatar
Robbert Krebbers committed
27
}.
28
Structure draT := DraT {
29 30 31 32 33 34
  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;
35
  dra_mixin : DraMixin dra_car
36
}.
37
Arguments DraT _ {_ _ _ _ _} _.
38 39 40 41 42 43 44 45 46
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
47

48 49 50 51 52 53 54 55 56 57 58 59 60 61
(** 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.
62
  Lemma dra_op_valid x y :  x   y  x ## y   (x  y).
63 64 65
  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.
66
  Lemma dra_assoc x y z :
67
     x   y   z  x ## y  x  y ## z  x  (y  z)  (x  y)  z.
68
  Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed.
69
  Lemma dra_disjoint_ll x y z :  x   y   z  x ## y  x  y ## z  x ## z.
70 71
  Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed.
  Lemma dra_disjoint_move_l x y z :
72
     x   y   z  x ## y  x  y ## z  x ## y  z.
73 74 75
  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.
76
  Lemma dra_comm x y :  x   y  x ## y  x  y  y  x.
77
  Proof. apply (mixin_dra_comm _ (dra_mixin A)). Qed.
78
  Lemma dra_core_disjoint_l x :  x  core x ## x.
79 80 81 82 83
  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.
84
  Lemma dra_core_mono x y : 
85
     z,  x   y  x ## y  core (x  y)  core x  z   z  core x ## z.
86
  Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
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
103
Section dra.
104 105 106
Context (A : draT).
Implicit Types a b : A.
Implicit Types x y z : validity A.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
Arguments valid _ _ !_ /.
108

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

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

133
Lemma dra_disjoint_rl a b c :  a   b   c  b ## c  a ## b  c  a ## b.
134
Proof. intros ???. rewrite !(symmetry_iff _ a). by apply dra_disjoint_ll. Qed.
135
Lemma dra_disjoint_lr a b c :  a   b   c  a ## b  a  b ## c  b ## c.
136
Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
137
Lemma dra_disjoint_move_r a b c :
138
   a   b   c  b ## c  a ## b  c  a  b ## c.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Proof.
140 141
  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
142
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
144

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

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

182
Global Instance validity_disrete_cmra : CmraDiscrete validityR.
183
Proof. apply discrete_cmra_discrete. Qed.
184 185
Global Instance validity_cmra_total : CmraTotal validityR.
Proof. rewrite /CmraTotal; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
186

187
Lemma validity_update x y :
188
  ( c,  x   c  validity_car x ## c   y  validity_car y ## c)  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
189
Proof.
190 191
  intros Hxy; apply cmra_discrete_update=> z [?[??]].
  split_and!; try eapply Hxy; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
Qed.
193

194
Lemma to_validity_op a b :
195
  ( (a  b)   a   b  a ## b) 
196 197
  to_validity (a  b)  to_validity a  to_validity b.
Proof. split; naive_solver eauto using dra_op_valid. Qed.
198

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