ra.v 6.39 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
Require Export prelude.collections prelude.relations prelude.fin_maps.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
Require Export modures.base.
Robbert Krebbers's avatar
Robbert Krebbers committed
3 4 5

Class Valid (A : Type) := valid : A  Prop.
Instance: Params (@valid) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Notation "✓" := valid (at level 1).
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9 10 11 12 13 14 15

Class Unit (A : Type) := unit : A  A.
Instance: Params (@unit) 2.

Class Op (A : Type) := op : A  A  A.
Instance: Params (@op) 2.
Infix "⋅" := op (at level 50, left associativity) : C_scope.
Notation "(⋅)" := op (only parsing) : C_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
16
Definition included `{Equiv A, Op A} (x y : A) :=  z, y  x  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
17 18
Infix "≼" := included (at level 70) : C_scope.
Notation "(≼)" := included (only parsing) : C_scope.
19
Hint Extern 0 (?x  ?y) => reflexivity.
Robbert Krebbers's avatar
Robbert Krebbers committed
20
Instance: Params (@included) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
21 22 23 24 25

Class Minus (A : Type) := minus : A  A  A.
Instance: Params (@minus) 2.
Infix "⩪" := minus (at level 40) : C_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
26
Class RA A `{Equiv A, Valid A, Unit A, Op A, Minus A} : Prop := {
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28 29 30
  (* setoids *)
  ra_equivalence :> Equivalence (() : relation A);
  ra_op_proper x :> Proper (() ==> ()) (op x);
  ra_unit_proper :> Proper (() ==> ()) unit;
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  ra_valid_proper :> Proper (() ==> impl) ;
Robbert Krebbers's avatar
Robbert Krebbers committed
32 33 34 35 36 37
  ra_minus_proper :> Proper (() ==> () ==> ()) minus;
  (* monoid *)
  ra_associative :> Associative () ();
  ra_commutative :> Commutative () ();
  ra_unit_l x : unit x  x  x;
  ra_unit_idempotent x : unit (unit x)  unit x;
Robbert Krebbers's avatar
Robbert Krebbers committed
38
  ra_unit_preserving x y : x  y  unit x  unit y;
Robbert Krebbers's avatar
Robbert Krebbers committed
39
  ra_valid_op_l x y :  (x  y)   x;
40 41
  ra_op_minus x y : x  y  x  y  x  y
}.
42
Class RAIdentity A `{Equiv A, Valid A, Op A, Empty A} : Prop := {
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  ra_empty_valid :  ;
44
  ra_empty_l :> LeftId ()  ()
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
47 48 49
Class RAMonotone
    `{Equiv A, Op A, Valid A, Equiv B, Op B, Valid B} (f : A  B) := {
  included_preserving x y : x  y  f x  f y;
Robbert Krebbers's avatar
Robbert Krebbers committed
50
  valid_preserving x :  x   (f x)
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52
}.

53 54 55 56 57 58
(** Big ops *)
Fixpoint big_op `{Op A, Empty A} (xs : list A) : A :=
  match xs with [] =>  | x :: xs => x  big_op xs end.
Arguments big_op _ _ _ !_ /.
Instance: Params (@big_op) 3.

59 60 61
Definition big_opM `{FinMapToList K A M, Op A, Empty A} (m : M) : A :=
  big_op (snd <$> map_to_list m).
Instance: Params (@big_opM) 6.
62

Robbert Krebbers's avatar
Robbert Krebbers committed
63 64
(** Updates *)
Definition ra_update_set `{Op A, Valid A} (x : A) (P : A  Prop) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
65
   z,  (x  z)   y, P y   (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67 68
Instance: Params (@ra_update_set) 3.
Infix "⇝:" := ra_update_set (at level 70).
Definition ra_update `{Op A, Valid A} (x y : A) :=  z,
Robbert Krebbers's avatar
Robbert Krebbers committed
69
   (x  z)   (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71 72 73 74 75 76
Infix "⇝" := ra_update (at level 70).
Instance: Params (@ra_update) 3.

(** Properties **)
Section ra.
Context `{RA A}.
Implicit Types x y z : A.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Implicit Types xs ys zs : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
78

Robbert Krebbers's avatar
Robbert Krebbers committed
79
Global Instance ra_valid_proper' : Proper (() ==> iff) .
Robbert Krebbers's avatar
Robbert Krebbers committed
80 81 82 83
Proof. by intros ???; split; apply ra_valid_proper. Qed.
Global Instance ra_op_proper' : Proper (() ==> () ==> ()) ().
Proof.
  intros x1 x2 Hx y1 y2 Hy.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
  by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Lemma ra_valid_op_r x y :  (x  y)   y.
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89 90
Proof. rewrite (commutative _ x); apply ra_valid_op_l. Qed.

(** ** Units *)
Lemma ra_unit_r x : x  unit x  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
Proof. by rewrite (commutative _ x) ra_unit_l. Qed.
92
Lemma ra_unit_unit x : unit x  unit x  unit x.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Proof. by rewrite -{2}(ra_unit_idempotent x) ra_unit_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95

(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Instance ra_included_proper' : Proper (() ==> () ==> impl) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
97
Proof. intros x1 x2 Hx y1 y2 Hy [z Hz]; exists z. by rewrite -Hy Hz Hx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
98 99 100 101 102 103
Global Instance ra_included_proper : Proper (() ==> () ==> iff) ().
Proof. by split; apply ra_included_proper'. Qed.
Lemma ra_included_l x y : x  x  y.
Proof. by exists y. Qed.
Lemma ra_included_r x y : y  x  y.
Proof. rewrite (commutative op); apply ra_included_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
104 105
Global Instance: PreOrder included.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
106 107 108
  split; first by intros x; exists (unit x); rewrite ra_unit_r.
  intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2).
  by rewrite (associative _) -Hy -Hz.
Robbert Krebbers's avatar
Robbert Krebbers committed
109 110
Qed.
Lemma ra_included_unit x : unit x  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
Proof. by exists x; rewrite ra_unit_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
Lemma ra_preserving_l x y z : x  y  z  x  z  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative ()). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
Lemma ra_preserving_r x y z : x  y  x  z  y  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
115
Proof. by intros; rewrite -!(commutative _ z); apply ra_preserving_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
116

117
(** ** RAs with empty element *)
118
Context `{Empty A, !RAIdentity A}.
119 120

Global Instance ra_empty_r : RightId ()  ().
Robbert Krebbers's avatar
Robbert Krebbers committed
121
Proof. by intros x; rewrite (commutative op) (left_id _ _). Qed.
122
Lemma ra_unit_empty : unit   .
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Proof. by rewrite -{2}(ra_unit_l ) (right_id _ _). Qed.
124
Lemma ra_empty_least x :   x.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Proof. by exists x; rewrite (left_id _ _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
126 127 128 129 130 131

(** * Big ops *)
Global Instance big_op_permutation : Proper (() ==> ()) big_op.
Proof.
  induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
  * by rewrite IH.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
  * by rewrite !(associative _) (commutative _ x).
Robbert Krebbers's avatar
Robbert Krebbers committed
133 134 135 136 137 138
  * by transitivity (big_op xs2).
Qed.
Global Instance big_op_proper : Proper (() ==> ()) big_op.
Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
Lemma big_op_app xs ys : big_op (xs ++ ys)  big_op xs  big_op ys.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
139 140
  induction xs as [|x xs IH]; simpl; first by rewrite ?(left_id _ _).
  by rewrite IH (associative _).
Robbert Krebbers's avatar
Robbert Krebbers committed
141 142 143
Qed.

Context `{FinMap K M}.
144 145 146 147
Lemma big_opM_empty : big_opM ( : M A)  .
Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
Lemma big_opM_insert (m : M A) i x :
  m !! i = None  big_opM (<[i:=x]> m)  x  big_opM m.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
149 150 151 152 153
Lemma big_opM_delete (m : M A) i x :
  m !! i = Some x  x  big_opM (delete i m)  big_opM m.
Proof.
  intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete.
Qed.
154
Lemma big_opM_singleton i x : big_opM ({[i  x]} : M A)  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
156 157
  rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
  by rewrite big_opM_empty (right_id _ _).
Robbert Krebbers's avatar
Robbert Krebbers committed
158
Qed.
159
Global Instance big_opM_proper : Proper (() ==> ()) (big_opM : M A  _).
Robbert Krebbers's avatar
Robbert Krebbers committed
160
Proof.
161
  intros m1; induction m1 as [|i x m1 ? IH] using map_ind.
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163 164
  { by intros m2; rewrite (symmetry_iff ()) map_equiv_empty; intros ->. }
  intros m2 Hm2; rewrite big_opM_insert //.
  rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
Robbert Krebbers's avatar
Robbert Krebbers committed
165 166
  destruct (map_equiv_lookup (<[i:=x]> m1) m2 i x)
    as (y&?&Hxy); auto using lookup_insert.
Robbert Krebbers's avatar
Robbert Krebbers committed
167 168
  rewrite Hxy -big_opM_insert; last auto using lookup_delete.
  by rewrite insert_delete.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
End ra.