RA.v 7.92 KB
Newer Older
1 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 29 30 31 32
(** Resource algebras: Commutative monoids with a decidable validity predicate. *)

Require Import Bool.
Require Export Predom.
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;
        ra_op_invalid t1 t2: ra_valid t1 = false -> ra_valid (ra_op t1 t2) = false
      }.
End Definitions.

Notation "1" := (ra_unit _) : ra_scope.
Notation "p · q" := (ra_op _ p q) (at level 40, left associativity) : ra_scope.
33
Notation "'✓' p" := (ra_valid _ p) (at level 35) : ra_scope.
34 35 36 37 38 39 40 41 42 43 44 45 46

Delimit Scope ra_scope with ra.

(* 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.

47
  Lemma ra_op_invalid2 t1 t2:  t2 = false ->  (t1 · t2) = false.
48 49 50 51
  Proof.
    rewrite comm. now eapply ra_op_invalid.
  Qed.

52
  Lemma ra_op_valid t1 t2:  (t1 · t2) = true ->  t1 = true.
53 54
  Proof.
    intros Hval.
55
    destruct ( t1) eqn:Heq; [reflexivity|].
56 57 58
    rewrite <-Hval. symmetry. now eapply ra_op_invalid.
  Qed.

59
  Lemma ra_op_valid2 t1 t2:  (t1 · t2) = true ->  t2 = true.
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
  Proof.
    rewrite comm. now eapply ra_op_valid.
  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) :=
77
    fun st => match st with (s, t) =>  s &&  t
78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
              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.
    - intros [s1 t1] [s2 t2]. unfold ra_valid; simpl. rewrite !andb_false_iff. intros [Hv|Hv].
      + left. now eapply ra_op_invalid.
      + right. now eapply ra_op_invalid.
  Qed.

End Products.

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

101
  Definition ra_pos: Type := { r |  r = true }.
102 103
  Coercion ra_proj (t:ra_pos): T := proj1_sig t.

104 105
  Definition ra_mk_pos t {VAL:  t = true}: ra_pos := exist _ t VAL.
  Definition ra_cr_pos {t} (VAL:  t = true) := ra_mk_pos t (VAL:=VAL).
106 107 108 109 110 111

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

112 113
  Lemma ra_op_pos_valid t1 t2 t:
    t1 · t2 == ra_proj t ->  t1 = true.
114 115 116 117 118
  Proof.
    destruct t as [t Hval]; simpl. intros Heq. rewrite <-Heq in Hval.
    eapply ra_op_valid. eassumption.
  Qed.

119 120
  Lemma ra_op_pos_valid2 t1 t2 t:
    t1 · t2 == ra_proj t ->  t2 = true.
121
  Proof.
122
    rewrite comm. now eapply ra_op_pos_valid.
123 124 125 126 127 128 129 130 131 132
  Qed.

End PositiveCarrier.
Global Arguments ra_pos T {_}.


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

133 134
  Definition pra_ord (t1 t2 : ra_pos T) :=
    exists td, td · (ra_proj t1) == (ra_proj t2).
135

136
  Global Program Instance pRA_preo : preoType (ra_pos T) | 0 := mkPOType pra_ord.
137 138
  Next Obligation.
    split.
139 140
    - intros x; exists 1. simpl. erewrite ra_op_unit by apply _; reflexivity.
    - intros z yz xyz [y Hyz] [x Hxyz]; unfold pra_ord.
141
      rewrite <- Hyz, assoc in Hxyz; setoid_rewrite <- Hxyz.
142
      exists (x · y). reflexivity.
143 144
  Qed.

145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
  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.
  Global Program Instance ra_preo : preoType T := mkPOType ra_ord.
161 162
  Next Obligation.
    split.
163
    - intros r; exists 1; erewrite ra_op_unit by apply _; reflexivity.
164 165 166 167
    - intros z yz xyz [y Hyz] [x Hxyz]; exists (x · y).
      rewrite <- Hxyz, <- Hyz; symmetry; apply assoc.
  Qed.

168
  Global Instance equiv_pord_ra : Proper (equiv ==> equiv ==> equiv) (pord (T := T)).
169 170 171 172 173 174
  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.

175
  Global Instance ra_op_monic : Proper (pord ++> pord ++> pord) (ra_op _).
176
  Proof.
177
    intros x1 x2 [x EQx] y1 y2 [y EQy]. exists (x · y).
178 179 180 181
    rewrite <- assoc, (comm y), <- assoc, assoc, (comm y1), EQx, EQy; reflexivity.
  Qed.

  Lemma ord_res_optRes r s :
182
    (r  s) <-> (ra_proj r  ra_proj s).
183 184
  Proof.
    split; intros HR.
185 186
    - destruct HR as [d EQ]. exists d. assumption.
    - destruct HR as [d EQ]. exists d. assumption.
187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258
  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.

  Global Program Instance ra_type_ex : Setoid ra_res_ex :=
    mkType ra_res_ex_eq.
  Next Obligation.
    split.
    - intros [t| |]; simpl; now auto.
    - intros [t1| |] [t2| |]; simpl; now auto.
    - intros [t1| |] [t2| |] [t3| |]; simpl; try now auto.
      + intros ? ?. etransitivity; eassumption.
  Qed.
      
  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.