RA.v 10.3 KB
Newer Older
1 2 3
(** Resource algebras: Commutative monoids with a decidable validity predicate. *)

Require Import Bool.
Ralf Jung's avatar
Ralf Jung committed
4 5
Require Import Predom.
Require Import CSetoid.
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
Require Import MetricCore.
Require Import PreoMet.

Class Associative {T} `{eqT : Setoid T} (op : T -> T -> T) :=
  assoc : forall t1 t2 t3, op t1 (op t2 t3) == op (op t1 t2) t3.
Class Commutative {T} `{eqT : Setoid T} (op : T -> T -> T) :=
  comm  : forall t1 t2, op t1 t2 == op t2 t1.

Section Definitions.
  Context (T : Type) `{Setoid T}.

  Class RA_unit := ra_unit : T.
  Class RA_op   := ra_op : T -> T -> T.
  Class RA_valid:= ra_valid : T -> bool.
  Class RA {TU : RA_unit} {TOP : RA_op} {TV : RA_valid}: Prop :=
    mkRA {
        ra_op_proper       :> Proper (equiv ==> equiv ==> equiv) ra_op;
        ra_op_assoc        :> Associative ra_op;
        ra_op_comm         :> Commutative ra_op;
        ra_op_unit t       : ra_op ra_unit t == t;
        ra_valid_proper    :> Proper (equiv ==> eq) ra_valid;
        ra_valid_unit      : ra_valid ra_unit = true;
Ralf Jung's avatar
Ralf Jung committed
28
        ra_op_valid t1 t2  : ra_valid (ra_op t1 t2) = true -> ra_valid t1 = true
29 30
      }.
End Definitions.
Ralf Jung's avatar
Ralf Jung committed
31
Arguments ra_valid {T} {_} t.
32 33 34

Notation "1" := (ra_unit _) : ra_scope.
Notation "p · q" := (ra_op _ p q) (at level 40, left associativity) : ra_scope.
Ralf Jung's avatar
Ralf Jung committed
35 36
Notation "'✓' p" := (ra_valid p = true) (at level 35) : ra_scope.
Notation "'~' '✓' p" := (ra_valid p <> true) (at level 35) : ra_scope.
37
Delimit Scope ra_scope with ra.
Ralf Jung's avatar
Ralf Jung committed
38

Ralf Jung's avatar
Ralf Jung committed
39
Tactic Notation "decide✓" ident(t1) "as" ident(H) := destruct (ra_valid t1) eqn:H; [|apply not_true_iff_false in H].
40 41 42 43 44 45 46 47 48 49 50


(* General RA lemmas *)
Section RAs.
  Context {T} `{RA T}.
  Local Open Scope ra_scope.

  Lemma ra_op_unit2 t: t · 1 == t.
  Proof.
    rewrite comm. now eapply ra_op_unit.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
51 52
  
  Lemma ra_op_valid2 t1 t2:  (t1 · t2) ->  t2.
53
  Proof.
Ralf Jung's avatar
Ralf Jung committed
54
    rewrite comm. now eapply ra_op_valid.
55 56
  Qed.

Ralf Jung's avatar
Ralf Jung committed
57
  Lemma ra_op_invalid t1 t2: ~t1 -> ~(t1 · t2).
58
  Proof.
Ralf Jung's avatar
Ralf Jung committed
59 60 61
    intros Hinval Hval.
    apply Hinval.
    eapply ra_op_valid; now eauto.
62 63
  Qed.

Ralf Jung's avatar
Ralf Jung committed
64
  Lemma ra_op_invalid2 t1 t2: ~t2 -> ~(t1 · t2).
65
  Proof.
Ralf Jung's avatar
Ralf Jung committed
66
    rewrite comm. now eapply ra_op_invalid.
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
  Qed.
End RAs.

(* RAs with cartesian products of carriers. *)
Section Products.
  Context S T `{raS : RA S, raT : RA T}.
  Local Open Scope ra_scope.

  Global Instance ra_unit_prod : RA_unit (S * T) := (ra_unit S, ra_unit T).
  Global Instance ra_op_prod : RA_op (S * T) :=
    fun st1 st2 =>
      match st1, st2 with
        | (s1, t1), (s2, t2) => (s1 · s2, t1 · t2)
      end.
  Global Instance ra_valid_prod : RA_valid (S * T) :=
Ralf Jung's avatar
Ralf Jung committed
82
    fun st => match st with (s, t) => ra_valid s && ra_valid t
83 84 85 86 87 88 89 90 91 92 93 94
              end.
  Global Instance ra_prod : RA (S * T).
  Proof.
    split.
    - intros [s1 t1] [s2 t2] [Heqs Heqt]. intros [s'1 t'1] [s'2 t'2] [Heqs' Heqt']. simpl in *.
      split; [rewrite Heqs, Heqs'|rewrite Heqt, Heqt']; reflexivity.
    - intros [s1 t1] [s2 t2] [s3 t3]. simpl; split; now rewrite ra_op_assoc.
    - intros [s1 t1] [s2 t2]. simpl; split; now rewrite ra_op_comm.
    - intros [s t]. simpl; split; now rewrite ra_op_unit.
    - intros [s1 t1] [s2 t2] [Heqs Heqt]. unfold ra_valid; simpl in *.
      rewrite Heqs, Heqt. reflexivity.
    - unfold ra_unit, ra_valid; simpl. erewrite !ra_valid_unit by apply _. reflexivity.
Ralf Jung's avatar
Ralf Jung committed
95 96 97
    - intros [s1 t1] [s2 t2]. unfold ra_valid; simpl. rewrite !andb_true_iff. intros [H1 H2]. split.
      + eapply ra_op_valid; now eauto.
      + eapply ra_op_valid; now eauto.
98 99 100
  Qed.
End Products.

Ralf Jung's avatar
Ralf Jung committed
101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134
Section ProductLemmas.
  Context {S T} `{raS : RA S, raT : RA T}.
  Local Open Scope ra_scope.
    
  Lemma ra_op_prod_fst (st1 st2: S*T):
    fst (st1 · st2) = fst st1 · fst st2.
  Proof.
    destruct st1 as [s1 t1]. destruct st2 as [s2 t2]. reflexivity.
  Qed.
  
  Lemma ra_op_prod_snd (st1 st2: S*T):
    snd (st1 · st2) = snd st1 · snd st2.
  Proof.
    destruct st1 as [s1 t1]. destruct st2 as [s2 t2]. reflexivity.
  Qed.

  Lemma ra_prod_valid (s: S) (t: T):
    (s, t) <-> s /\ t.
  Proof.
    unfold ra_valid, ra_valid_prod.
    rewrite andb_true_iff.
    reflexivity.
  Qed.

  Lemma ra_prod_valid2 (st: S*T):
    st <-> (fst st) /\ (snd st).
  Proof.
    destruct st as [s t]. unfold ra_valid, ra_valid_prod.
    rewrite andb_true_iff.
    tauto.
  Qed.

End ProductLemmas.

135 136 137 138
Section PositiveCarrier.
  Context {T} `{raT : RA T}.
  Local Open Scope ra_scope.

Ralf Jung's avatar
Ralf Jung committed
139
  Definition ra_pos: Type := { r |  r }.
140 141
  Coercion ra_proj (t:ra_pos): T := proj1_sig t.

Ralf Jung's avatar
Ralf Jung committed
142
  Definition ra_mk_pos t {VAL:  t}: ra_pos := exist _ t VAL.
143 144 145 146 147 148

  Program Definition ra_pos_unit: ra_pos := exist _ 1 _.
  Next Obligation.
    now erewrite ra_valid_unit by apply _.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
149 150 151 152 153 154
  Lemma ra_proj_cancel r (VAL: r):
    ra_proj (ra_mk_pos r (VAL:=VAL)) = r.
  Proof.
    reflexivity.
  Qed.

155
  Lemma ra_op_pos_valid t1 t2 t:
Ralf Jung's avatar
Ralf Jung committed
156
    t1 · t2 == ra_proj t ->  t1.
157 158
  Proof.
    destruct t as [t Hval]; simpl. intros Heq. rewrite <-Heq in Hval.
Ralf Jung's avatar
Ralf Jung committed
159
    eapply ra_op_valid; eassumption.
160 161
  Qed.

162
  Lemma ra_op_pos_valid2 t1 t2 t:
Ralf Jung's avatar
Ralf Jung committed
163
    t1 · t2 == ra_proj t ->  t2.
164
  Proof.
165
    rewrite comm. now eapply ra_op_pos_valid.
166 167
  Qed.

Ralf Jung's avatar
Ralf Jung committed
168 169 170 171 172 173 174
  Lemma ra_pos_valid (r : ra_pos):
    (ra_proj r).
  Proof.
    destruct r as [r VAL].
    exact VAL.
  Qed.

175 176
End PositiveCarrier.
Global Arguments ra_pos T {_}.
177 178 179 180 181 182 183 184 185 186 187 188

(** Validity automation tactics *)
Ltac auto_valid_inner :=
  solve [ eapply ra_op_pos_valid; (eassumption || rewrite comm; eassumption)
        | eapply ra_op_pos_valid2; (eassumption || rewrite comm; eassumption)
        | eapply ra_op_valid; (eassumption || rewrite comm; eassumption) ].
Ltac auto_valid := match goal with
                     | |- @ra_valid ?T _ _ = true =>
                       let H := fresh in assert (H : RA T) by apply _; auto_valid_inner
                   end.

(* FIXME put the common parts into a helper tactic, and allow arbitrary tactics after "by" *)
189
Tactic Notation "exists✓" constr(t) := let H := fresh "Hval" in assert(H:(t)%ra); [|exists (ra_mk_pos t (VAL:=H) ) ].
190 191 192
Tactic Notation "exists✓" constr(t) "by" "auto_valid" := let H := fresh "Hval" in assert(H:(t)%ra); [auto_valid|exists (ra_mk_pos t (VAL:=H) ) ].
Tactic Notation "pose✓" ident(name) ":=" constr(t) := let H := fresh "Hval" in assert(H:(t)%ra); [|pose (name := ra_mk_pos t (VAL:=H) ) ].
Tactic Notation "pose✓" ident(name) ":=" constr(t) "by" "auto_valid" := let H := fresh "Hval" in assert(H:(t)%ra); [auto_valid|pose (name := ra_mk_pos t (VAL:=H) ) ].
193 194 195 196 197 198


Section Order.
  Context T `{raT : RA T}.
  Local Open Scope ra_scope.

199 200
  Definition pra_ord (t1 t2 : ra_pos T) :=
    exists td, td · (ra_proj t1) == (ra_proj t2).
201

Ralf Jung's avatar
Ralf Jung committed
202 203
  Global Instance pra_ord_preo: PreOrder pra_ord.
  Proof.
204
    split.
205 206
    - intros x; exists 1. simpl. erewrite ra_op_unit by apply _; reflexivity.
    - intros z yz xyz [y Hyz] [x Hxyz]; unfold pra_ord.
207
      rewrite <- Hyz, assoc in Hxyz; setoid_rewrite <- Hxyz.
208
      exists (x · y). reflexivity.
209 210
  Qed.

Ralf Jung's avatar
Ralf Jung committed
211 212
  Global Program Instance pRA_preo : preoType (ra_pos T) | 0 := mkPOType pra_ord.

213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
  Global Instance equiv_pord_pra : Proper (equiv ==> equiv ==> equiv) (pord (T := ra_pos T)).
  Proof.
    intros s1 s2 EQs t1 t2 EQt; split; intros [s HS].
    - exists s; rewrite <- EQs, <- EQt; assumption.
    - exists s; rewrite EQs, EQt; assumption.
  Qed.

  Lemma unit_min r : ra_pos_unit  r.
  Proof.
    exists (ra_proj r). simpl.
    now erewrite ra_op_unit2 by apply _.
  Qed.

  Definition ra_ord (t1 t2 : T) :=
    exists t, t · t1 == t2.
Ralf Jung's avatar
Ralf Jung committed
228 229 230

  Global Instance ra_ord_preo: PreOrder ra_ord.
  Proof.
231
    split.
232
    - intros r; exists 1; erewrite ra_op_unit by apply _; reflexivity.
233 234 235
    - intros z yz xyz [y Hyz] [x Hxyz]; exists (x · y).
      rewrite <- Hxyz, <- Hyz; symmetry; apply assoc.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
236 237
  
  Global Program Instance ra_preo : preoType T := mkPOType ra_ord.
238

239
  Global Instance equiv_pord_ra : Proper (equiv ==> equiv ==> equiv) (pord (T := T)).
240 241 242 243 244 245
  Proof.
    intros s1 s2 EQs t1 t2 EQt; split; intros [s HS].
    - exists s; rewrite <- EQs, <- EQt; assumption.
    - exists s; rewrite EQs, EQt; assumption.
  Qed.

246
  Global Instance ra_op_monic : Proper (pord ++> pord ++> pord) (ra_op _).
247
  Proof.
248
    intros x1 x2 [x EQx] y1 y2 [y EQy]. exists (x · y).
249 250 251
    rewrite <- assoc, (comm y), <- assoc, assoc, (comm y1), EQx, EQy; reflexivity.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
252
  Lemma ord_res_pres r s :
253
    (r  s) <-> (ra_proj r  ra_proj s).
254 255
  Proof.
    split; intros HR.
256 257
    - destruct HR as [d EQ]. exists d. assumption.
    - destruct HR as [d EQ]. exists d. assumption.
258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278
  Qed.

End Order.

Section Exclusive.
  Context (T: Type) `{Setoid T}.
  Local Open Scope ra_scope.

  Inductive ra_res_ex: Type :=
  | ex_own: T -> ra_res_ex
  | ex_unit: ra_res_ex
  | ex_bot: ra_res_ex.

  Definition ra_res_ex_eq e1 e2: Prop :=
    match e1, e2 with
      | ex_own s1, ex_own s2 => s1 == s2
      | ex_unit, ex_unit => True
      | ex_bot, ex_bot => True
      | _, _ => False
    end.

279 280 281 282 283 284 285
  Global Instance ra_eq_equiv : Equivalence ra_res_ex_eq.
  Proof.
    split.
    - intros [t| |]; simpl; now auto.
    - intros [t1| |] [t2| |]; simpl; now auto.
    - intros [t1| |] [t2| |] [t3| |]; simpl; try now auto.
      + intros ? ?. etransitivity; eassumption.
Ralf Jung's avatar
Ralf Jung committed
286 287 288 289
  Qed.

  Global Program Instance ra_type_ex : Setoid ra_res_ex :=
    mkType ra_res_ex_eq.
290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331
      
  Global Instance ra_unit_ex : RA_unit ra_res_ex := ex_unit.
  Global Instance ra_op_ex : RA_op ra_res_ex :=
    fun e1 e2 =>
      match e1, e2 with
        | ex_own s1, ex_unit => ex_own s1
        | ex_unit, ex_own s2 => ex_own s2
        | ex_unit, ex_unit   => ex_unit
        | _, _               => ex_bot
      end.
  Global Instance ra_valid_ex : RA_valid ra_res_ex :=
    fun e => match e with
               | ex_bot => false
               | _      => true
             end.
  
  Global Instance ra_ex : RA ra_res_ex.
  Proof.
    split.
    - intros [t1| |] [t2| |] Heqt [t'1| |] [t'2| |] Heqt'; simpl; now auto.  
    - intros [s1| |] [s2| |] [s3| |]; reflexivity.
    - intros [s1| |] [s2| |]; reflexivity.
    - intros [s1| |]; reflexivity.
    - intros [t1| |] [t2| |] Heqt; unfold ra_valid; simpl in *; now auto.
    - reflexivity.
    - intros [t1| |] [t2| |]; unfold ra_valid; simpl; now auto.
  Qed.

End Exclusive.


(* Package of a monoid as a module type (for use with other modules). *)
Module Type RA_T.

  Parameter res : Type.
  Declare Instance res_type : Setoid res.
  Declare Instance res_op : RA_op res.
  Declare Instance res_unit : RA_unit res.
  Declare Instance res_valid : RA_valid res.
  Declare Instance res_ra : RA res.

End RA_T.