dra.v 6.25 KB
Newer Older
1
Require Export algebra.cmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28

(** 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.
Instance validity_valid {A} (P : A  Prop) : Valid (validity P) :=
  validity_is_valid.
Instance validity_equiv `{Equiv A} (P : A  Prop) : Equiv (validity P) := λ x y,
  (valid x  valid y)  (valid x  validity_car x  validity_car y).
Instance validity_equivalence `{Equiv A,!Equivalence (() : relation A)} P :
  Equivalence (() : relation (validity P)).
Proof.
  split; unfold equiv, validity_equiv.
  * by intros [x px ?]; simpl.
  * intros [x px ?] [y py ?]; naive_solver.
  * intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
    split; [|intros; transitivity y]; tauto.
Qed.
Instance validity_valid_proper `{Equiv A} (P : A  Prop) :
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  Proper (() ==> iff) ( : validity P  Prop).
Robbert Krebbers's avatar
Robbert Krebbers committed
30 31
Proof. intros ?? [??]; naive_solver. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
32
Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
33
   z, y  x  z   z  x  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35 36 37
Instance: Params (@dra_included) 4.
Local Infix "≼" := dra_included.

Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39 40 41 42 43 44
  (* setoids *)
  dra_equivalence :> Equivalence (() : relation A);
  dra_op_proper :> Proper (() ==> () ==> ()) ();
  dra_unit_proper :> Proper (() ==> ()) unit;
  dra_disjoint_proper :>  x, Proper (() ==> impl) (disjoint x);
  dra_minus_proper :> Proper (() ==> () ==> ()) minus;
  (* validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46 47
  dra_op_valid x y :  x   y  x  y   (x  y);
  dra_unit_valid x :  x   (unit x);
  dra_minus_valid x y :  x   y  x  y   (y  x);
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49
  (* monoid *)
  dra_associative :> Associative () ();
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51
  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
52
  dra_symmetric :> Symmetric (@disjoint A _);
Robbert Krebbers's avatar
Robbert Krebbers committed
53 54 55 56 57 58 59
  dra_commutative x y :  x   y  x  y  x  y  y  x;
  dra_unit_disjoint_l x :  x  unit x  x;
  dra_unit_l x :  x  unit x  x  x;
  dra_unit_idempotent x :  x  unit (unit x)  unit x;
  dra_unit_preserving x y :  x   y  x  y  unit x  unit y;
  dra_disjoint_minus x y :  x   y  x  y  x  y  x;
  dra_op_minus x y :  x   y  x  y  x  y  x  y
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61 62 63 64
}.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
67
Instance: Proper (() ==> () ==> iff) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  intros x1 x2 Hx y1 y2 Hy; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71
  * 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
72
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Lemma dra_disjoint_rl x y z :  x   y   z  y  z  x  y  z  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
Lemma dra_disjoint_lr x y z :  x   y   z  x  y  x  y  z  y  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof. intros ????. rewrite dra_commutative //. by apply dra_disjoint_ll. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Lemma dra_disjoint_move_r x y z :
Robbert Krebbers's avatar
Robbert Krebbers committed
78
   x   y   z  y  z  x  y  z  x  y  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  intros; symmetry; rewrite dra_commutative; eauto using dra_disjoint_rl.
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82
  apply dra_disjoint_move_l; auto; by rewrite dra_commutative.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Hint Unfold dra_included.
Robbert Krebbers's avatar
Robbert Krebbers committed
85

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

102
Definition validity_ra : RA (discreteC T).
Robbert Krebbers's avatar
Robbert Krebbers committed
103 104 105 106
Proof.
  split.
  * intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
    split; intros (?&?&?); split_ands';
Robbert Krebbers's avatar
Robbert Krebbers committed
107
      first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
Robbert Krebbers's avatar
Robbert Krebbers committed
108
  * by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
  * by intros ?? -> ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
  * intros x1 x2 [? Hx] y1 y2 [? Hy];
Robbert Krebbers's avatar
Robbert Krebbers committed
111
      split; simpl; [|by intros (?&?&?); rewrite Hx // Hy].
Robbert Krebbers's avatar
Robbert Krebbers committed
112
    split; intros (?&?&z&?&?); split_ands'; try tauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114
    + exists z. by rewrite -Hy // -Hx.
    + exists z. by rewrite Hx ?Hy; tauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116 117 118 119 120 121 122 123 124 125 126 127
  * intros [x px ?] [y py ?] [z pz ?]; split; simpl;
      [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
      |intros; apply (associative _)].
  * intros [x px ?] [y py ?]; split; naive_solver eauto using dra_commutative.
  * intros [x px ?]; split;
      naive_solver eauto using dra_unit_l, dra_unit_disjoint_l.
  * intros [x px ?]; split; naive_solver eauto using dra_unit_idempotent.
  * intros x y Hxy; exists (unit y  unit x).
    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 *;
      intuition eauto using dra_op_minus, dra_disjoint_minus, dra_unit_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  * by intros [x px ?] [y py ?] (?&?&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130
  * intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
      intuition eauto 10 using dra_disjoint_minus, dra_op_minus.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
Qed.
132
Definition validityRA : cmraT := discreteRA validity_ra.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
Definition validity_update (x y : validityRA) :
134
  ( z,  x   z  validity_car x  z   y  validity_car y  z)  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
Proof.
136
  intros Hxy. apply discrete_update.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
  intros z (?&?&?); split_ands'; try eapply Hxy; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
138 139
Qed.
End dra.