dra.v 6.03 KB
Newer Older
1
From iris.algebra Require Export cmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
5
6
7
8

(** 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
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
Add Printing Constructor validity.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
12
13
14
15
16
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
17
Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
20
  (* setoids *)
  dra_equivalence :> Equivalence (() : relation A);
  dra_op_proper :> Proper (() ==> () ==> ()) ();
Ralf Jung's avatar
Ralf Jung committed
21
  dra_core_proper :> Proper (() ==> ()) core;
Robbert Krebbers's avatar
Robbert Krebbers committed
22
  dra_valid_proper :> Proper (() ==> impl) valid;
Robbert Krebbers's avatar
Robbert Krebbers committed
23
24
  dra_disjoint_proper :>  x, Proper (() ==> impl) (disjoint x);
  (* validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  dra_op_valid x y :  x   y  x  y   (x  y);
Ralf Jung's avatar
Ralf Jung committed
26
  dra_core_valid x :  x   core x;
Robbert Krebbers's avatar
Robbert Krebbers committed
27
  (* monoid *)
28
  dra_assoc :> Assoc () ();
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
  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
31
  dra_symmetric :> Symmetric (@disjoint A _);
32
  dra_comm x y :  x   y  x  y  x  y  y  x;
Ralf Jung's avatar
Ralf Jung committed
33
34
35
  dra_core_disjoint_l x :  x  core x  x;
  dra_core_l x :  x  core x  x  x;
  dra_core_idemp x :  x  core (core x)  core x;
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
  dra_core_preserving x y : 
     z,  x   y  x  y  core (x  y)  core x  z   z  core x  z
Robbert Krebbers's avatar
Robbert Krebbers committed
38
39
40
41
42
}.

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

45
46
47
48
49
50
51
52
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.
53
54
55
  - by intros [x px ?]; simpl.
  - intros [x px ?] [y py ?]; naive_solver.
  - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
56
    split; [|intros; trans y]; tauto.
57
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59
60
61
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
62
Instance: Proper (() ==> () ==> iff) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  intros x1 x2 Hx y1 y2 Hy; split.
65
66
  - 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
67
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Lemma dra_disjoint_rl x y z :  x   y   z  y  z  x  y  z  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Lemma dra_disjoint_lr x y z :  x   y   z  x  y  x  y  z  y  z.
71
Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Lemma dra_disjoint_move_r x y z :
Robbert Krebbers's avatar
Robbert Krebbers committed
73
   x   y   z  y  z  x  y  z  x  y  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Proof.
75
76
  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
77
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
79

80
Lemma validity_valid_car_valid (z : T) :  z   validity_car z.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
Proof. apply validity_prf. Qed.
Hint Resolve validity_valid_car_valid.
Ralf Jung's avatar
Ralf Jung committed
83
84
85
Program Instance validity_core : Core T := λ x,
  Validity (core (validity_car x)) ( x) _.
Solve Obligations with naive_solver auto using dra_core_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
87
Program Instance validity_op : Op T := λ x y,
  Validity (validity_car x  validity_car y)
Robbert Krebbers's avatar
Robbert Krebbers committed
88
           ( x   y  validity_car x  validity_car y) _.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Solve Obligations with naive_solver auto using dra_op_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
90

91
Definition validity_ra : RA (discreteC T).
Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
Proof.
  split.
94
  - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
95
    split; intros (?&?&?); split_and!;
Robbert Krebbers's avatar
Robbert Krebbers committed
96
      first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
97
98
99
  - 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
100
      [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
101
      |by intros; rewrite assoc].
102
103
  - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
  - intros [x px ?]; split;
Ralf Jung's avatar
Ralf Jung committed
104
105
      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
106
107
108
109
110
111
  - 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.
112
  - by intros [x px ?] [y py ?] (?&?&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Qed.
114
Definition validityR : cmraT := discreteR validity_ra.
115
Instance validity_cmra_discrete :
116
  CMRADiscrete validityR := discrete_cmra_discrete _.
117

118
Lemma validity_update (x y : validityR) :
119
  ( z,  x   z  validity_car x  z   y  validity_car y  z)  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Proof.
121
122
  intros Hxy; apply cmra_discrete_update=> z [?[??]].
  split_and!; try eapply Hxy; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Qed.
124
125

Lemma to_validity_op (x y : A) :
126
  ( (x  y)   x   y  x  y) 
127
  to_validity (x  y)  to_validity x  to_validity y.
128
Proof. split; naive_solver auto using dra_op_valid. Qed.
129

130
(* TODO: This has to be proven again. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
131
(*
132
133
134
135
136
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
137
138
    destruct Hvl' as [? [? ?]]; split; first done.
    exists (validity_car z); eauto.
139
  - intros (Hvl & z & EQ & ? & ?).
Robbert Krebbers's avatar
Robbert Krebbers committed
140
    assert (✓ y) by (rewrite EQ; by apply dra_op_valid).
141
    split; first done. exists (to_validity z). split; first split.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
    + intros _. simpl. by split_and!.
143
144
145
    + intros _. setoid_subst. by apply dra_op_valid. 
    + intros _. rewrite /= EQ //.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
147
End dra.