dra.v 7.1 KB
Newer Older
1
From algebra Require Export cmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
5
6
7
8
9
10
11
12
13
14
15

(** From disjoint pcm *)
Record validity {A} (P : A  Prop) : Type := Validity {
  validity_car : A;
  validity_is_valid : Prop;
  validity_prf : validity_is_valid  P validity_car
}.
Arguments Validity {_ _} _ _ _.
Arguments validity_car {_ _} _.
Arguments validity_is_valid {_ _} _.

Definition to_validity {A} {P : A  Prop} (x : A) : validity P :=
  Validity x (P x) id.

Robbert Krebbers's avatar
Robbert Krebbers committed
16
Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
17
   z, y  x  z   z  x  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
20
Instance: Params (@dra_included) 4.
Local Infix "≼" := dra_included.

21
Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Div A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
25
  (* setoids *)
  dra_equivalence :> Equivalence (() : relation A);
  dra_op_proper :> Proper (() ==> () ==> ()) ();
  dra_unit_proper :> Proper (() ==> ()) unit;
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  dra_valid_proper :> Proper (() ==> impl) valid;
Robbert Krebbers's avatar
Robbert Krebbers committed
27
  dra_disjoint_proper :>  x, Proper (() ==> impl) (disjoint x);
28
  dra_div_proper :> Proper (() ==> () ==> ()) div;
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  (* validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  dra_op_valid x y :  x   y  x  y   (x  y);
31
  dra_unit_valid x :  x   unit x;
32
  dra_div_valid x y :  x   y  x  y   (y ÷ x);
Robbert Krebbers's avatar
Robbert Krebbers committed
33
  (* monoid *)
34
  dra_assoc :> Assoc () ();
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
  dra_disjoint_ll x y z :  x   y   z  x  y  x  y  z  x  z;
  dra_disjoint_move_l x y z :  x   y   z  x  y  x  y  z  x  y  z;
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  dra_symmetric :> Symmetric (@disjoint A _);
38
  dra_comm x y :  x   y  x  y  x  y  y  x;
Robbert Krebbers's avatar
Robbert Krebbers committed
39
40
  dra_unit_disjoint_l x :  x  unit x  x;
  dra_unit_l x :  x  unit x  x  x;
41
  dra_unit_idemp x :  x  unit (unit x)  unit x;
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  dra_unit_preserving x y :  x   y  x  y  unit x  unit y;
43
44
  dra_disjoint_div x y :  x   y  x  y  x  y ÷ x;
  dra_op_div x y :  x   y  x  y  x  y ÷ x  y
Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
47
48
49
}.

Section dra.
Context A `{DRA A}.
Arguments valid _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
Hint Immediate dra_op_proper : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
51

52
53
54
55
56
57
58
59
Notation T := (validity (valid : A  Prop)).

Instance validity_valid : Valid T := validity_is_valid.
Instance validity_equiv : Equiv T := λ x y,
  (valid x  valid y)  (valid x  validity_car x  validity_car y).
Instance validity_equivalence : Equivalence (() : relation T).
Proof.
  split; unfold equiv, validity_equiv.
60
61
62
  - by intros [x px ?]; simpl.
  - intros [x px ?] [y py ?]; naive_solver.
  - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
63
    split; [|intros; trans y]; tauto.
64
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
67
68
Instance dra_valid_proper' : Proper (() ==> iff) (valid : A  Prop).
Proof. by split; apply dra_valid_proper. Qed.
Instance to_validity_proper : Proper (() ==> ()) to_validity.
Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Instance: Proper (() ==> () ==> iff) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  intros x1 x2 Hx y1 y2 Hy; split.
72
73
  - 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
74
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
Lemma dra_disjoint_rl x y z :  x   y   z  y  z  x  y  z  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Lemma dra_disjoint_lr x y z :  x   y   z  x  y  x  y  z  y  z.
78
Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Lemma dra_disjoint_move_r x y z :
Robbert Krebbers's avatar
Robbert Krebbers committed
80
   x   y   z  y  z  x  y  z  x  y  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Proof.
82
83
  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
84
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Hint Unfold dra_included.
Robbert Krebbers's avatar
Robbert Krebbers committed
87

88
Lemma validity_valid_car_valid (z : T) :  z   validity_car z.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
90
Proof. apply validity_prf. Qed.
Hint Resolve validity_valid_car_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
Program Instance validity_unit : Unit T := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
92
  Validity (unit (validity_car x)) ( x) _.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Solve Obligations with naive_solver auto using dra_unit_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
Program Instance validity_op : Op T := λ x y,
  Validity (validity_car x  validity_car y)
Robbert Krebbers's avatar
Robbert Krebbers committed
96
           ( x   y  validity_car x  validity_car y) _.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
Solve Obligations with naive_solver auto using dra_op_valid.
98
99
Program Instance validity_div : Div T := λ x y,
  Validity (validity_car x ÷ validity_car y)
Robbert Krebbers's avatar
Robbert Krebbers committed
100
           ( x   y  validity_car y  validity_car x) _.
101
Solve Obligations with naive_solver auto using dra_div_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
102

103
Definition validity_ra : RA (discreteC T).
Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
Proof.
  split.
106
  - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
107
    split; intros (?&?&?); split_and!;
Robbert Krebbers's avatar
Robbert Krebbers committed
108
      first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
109
110
111
  - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
  - intros ?? [??]; naive_solver.
  - intros x1 x2 [? Hx] y1 y2 [? Hy];
Robbert Krebbers's avatar
Robbert Krebbers committed
112
      split; simpl; [|by intros (?&?&?); rewrite Hx // Hy].
113
    split; intros (?&?&z&?&?); split_and!; try tauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
    + exists z. by rewrite -Hy // -Hx.
    + exists z. by rewrite Hx ?Hy; tauto.
116
  - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
Robbert Krebbers's avatar
Robbert Krebbers committed
117
      [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
118
      |by intros; rewrite assoc].
119
120
  - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
  - intros [x px ?]; split;
Robbert Krebbers's avatar
Robbert Krebbers committed
121
      naive_solver eauto using dra_unit_l, dra_unit_disjoint_l.
122
  - intros [x px ?]; split; naive_solver eauto using dra_unit_idemp.
123
  - intros x y Hxy; exists (unit y ÷ unit x).
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
126
127
    destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *.
    assert (py  unit x  unit y)
      by intuition eauto 10 using dra_unit_preserving.
    constructor; [|symmetry]; simpl in *;
128
      intuition eauto using dra_op_div, dra_disjoint_div, dra_unit_valid.
129
130
  - by intros [x px ?] [y py ?] (?&?&?).
  - intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
131
      intuition eauto 10 using dra_disjoint_div, dra_op_div.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Qed.
133
Definition validityRA : cmraT := discreteRA validity_ra.
134
135
136
Instance validity_cmra_discrete :
  CMRADiscrete validityRA := discrete_cmra_discrete _.

137
Lemma validity_update (x y : validityRA) :
138
  ( z,  x   z  validity_car x  z   y  validity_car y  z)  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Proof.
140
141
  intros Hxy; apply cmra_discrete_update=> z [?[??]].
  split_and!; try eapply Hxy; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
Qed.
143
144

Lemma to_validity_op (x y : A) :
145
  ( (x  y)   x   y  x  y) 
146
  to_validity (x  y)  to_validity x  to_validity y.
147
Proof. split; naive_solver auto using dra_op_valid. Qed.
148

149
150
151
152
153
154
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'.
    destruct Hvl' as [? [? ?]].
155
    split; first done.
156
157
158
159
160
161
162
163
164
165
    exists (validity_car z). split_and!; last done.
    + apply EQ. assumption.
    + by apply validity_valid_car_valid.
  - intros (Hvl & z & EQ & ? & ?).
    assert ( y) by (rewrite EQ; apply dra_op_valid; done).
    split; first done. exists (to_validity z). split; first split.
    + intros _. simpl. split_and!; done.
    + intros _. setoid_subst. by apply dra_op_valid. 
    + intros _. rewrite /= EQ //.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
End dra.