excl.v 8.5 KB
Newer Older
1
From algebra Require Export cmra.
2
From algebra Require Import upred.
Robbert Krebbers's avatar
Robbert Krebbers committed
3 4
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _  !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6 7

Inductive excl (A : Type) :=
  | Excl : A  excl A
Robbert Krebbers's avatar
Robbert Krebbers committed
8
  | ExclUnit : excl A
Robbert Krebbers's avatar
Robbert Krebbers committed
9 10 11 12
  | ExclBot : excl A.
Arguments Excl {_} _.
Arguments ExclUnit {_}.
Arguments ExclBot {_}.
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14
Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
  match x with Excl a => Some a | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
15

16 17
Section excl.
Context {A : cofeT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
18 19
Implicit Types a b : A.
Implicit Types x y : excl A.
20

Robbert Krebbers's avatar
Robbert Krebbers committed
21
(* Cofe *)
22
Inductive excl_equiv : Equiv (excl A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  | Excl_equiv a b : a  b  Excl a  Excl b
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  | ExclUnit_equiv : ExclUnit  ExclUnit
Robbert Krebbers's avatar
Robbert Krebbers committed
25 26
  | ExclBot_equiv : ExclBot  ExclBot.
Existing Instance excl_equiv.
27
Inductive excl_dist : Dist (excl A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  | Excl_dist a b n : a {n} b  Excl a {n} Excl b
29 30
  | ExclUnit_dist n : ExclUnit {n} ExclUnit
  | ExclBot_dist n : ExclBot {n} ExclBot.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Existing Instance excl_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
32

Robbert Krebbers's avatar
Robbert Krebbers committed
33
Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A).
34 35 36
Proof. by constructor. Qed.
Global Instance Excl_proper : Proper (() ==> ()) (@Excl A).
Proof. by constructor. Qed.
37
Global Instance Excl_inj : Inj () () (@Excl A).
38
Proof. by inversion_clear 1. Qed.
39
Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
40
Proof. by inversion_clear 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
41

42
Program Definition excl_chain
43
    (c : chain (excl A)) (a : A) (H : maybe Excl (c 0) = Some a) : chain A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  {| chain_car n := match c n return _ with Excl y => y | _ => a end |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
Next Obligation.
46 47 48
  intros c a ? n i ?; simpl.
  destruct (c 0) eqn:?; simplify_eq/=.
  by feed inversion (chain_cauchy c n i).
Robbert Krebbers's avatar
Robbert Krebbers committed
49
Qed.
50
Instance excl_compl : Compl (excl A) := λ c,
51 52
  match Some_dec (maybe Excl (c 0)) with
  | inleft (exist a H) => Excl (compl (excl_chain c a H)) | inright _ => c 0
Robbert Krebbers's avatar
Robbert Krebbers committed
53
  end.
54
Definition excl_cofe_mixin : CofeMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  - intros x y; split; [by destruct 1; constructor; apply equiv_dist|].
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59
    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
    by intros n; feed inversion (Hxy n).
60
  - intros n; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
    + by intros []; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
    + by destruct 1; constructor.
63
    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
64
  - by inversion_clear 1; constructor; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  - intros n c; unfold compl, excl_compl.
66 67 68 69
    destruct (Some_dec (maybe Excl (c 0))) as [[a Ha]|].
    { assert (c 0 = Excl a) by (by destruct (c 0); simplify_eq/=).
      assert ( b, c n = Excl b) as [b Hb].
      { feed inversion (chain_cauchy c 0 n); eauto with lia congruence. }
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71
      rewrite Hb; constructor.
      by rewrite (conv_compl n (excl_chain c a Ha)) /= Hb. }
72 73
    feed inversion (chain_cauchy c 0 n); first lia;
       constructor; destruct (c 0); simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Qed.
75
Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
76 77 78 79
Global Instance excl_discrete : Discrete A  Discrete exclC.
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Global Instance excl_leibniz : LeibnizEquiv A  LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
80

Robbert Krebbers's avatar
Robbert Krebbers committed
81
Global Instance Excl_timeless a : Timeless a  Timeless (Excl a).
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
83
Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Proof. by inversion_clear 1; constructor. Qed.
85
Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Proof. by inversion_clear 1; constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88

(* CMRA *)
89 90
Instance excl_valid : Valid (excl A) := λ x,
  match x with Excl _ | ExclUnit => True | ExclBot => False end.
91
Instance excl_validN : ValidN (excl A) := λ n x,
92
  match x with Excl _ | ExclUnit => True | ExclBot => False end.
93 94 95
Global Instance excl_empty : Empty (excl A) := ExclUnit.
Instance excl_unit : Unit (excl A) := λ _, .
Instance excl_op : Op (excl A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
96
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  | Excl a, ExclUnit | ExclUnit, Excl a => Excl a
Robbert Krebbers's avatar
Robbert Krebbers committed
98 99 100
  | ExclUnit, ExclUnit => ExclUnit
  | _, _=> ExclBot
  end.
101
Instance excl_div : Div (excl A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103 104 105 106
  match x, y with
  | _, ExclUnit => x
  | Excl _, Excl _ => ExclUnit
  | _, _ => ExclBot
  end.
107
Definition excl_cmra_mixin : CMRAMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
108 109
Proof.
  split.
110 111 112 113
  - by intros n []; destruct 1; constructor.
  - constructor.
  - by destruct 1; intros ?.
  - by destruct 1; inversion_clear 1; constructor.
114
  - intros x; split. done. by move=> /(_ 0).
115 116 117 118 119
  - intros n [?| |]; simpl; auto with lia.
  - by intros [?| |] [?| |] [?| |]; constructor.
  - by intros [?| |] [?| |]; constructor.
  - by intros [?| |]; constructor.
  - constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
  - by intros [?| |] [?| |]; exists .
121
  - by intros n [?| |] [?| |].
Robbert Krebbers's avatar
Robbert Krebbers committed
122
  - by intros [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
123 124 125 126 127 128
  - intros n x y1 y2 ? Hx.
    by exists match y1, y2 with
      | Excl a1, Excl a2 => (Excl a1, Excl a2)
      | ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot)
      | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
      end; destruct y1, y2; inversion_clear Hx; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
Qed.
130 131
Canonical Structure exclR : cmraT := CMRAT excl_cofe_mixin excl_cmra_mixin.
Global Instance excl_cmra_identity : CMRAIdentity exclR.
132
Proof. split. done. by intros []. apply _. Qed.
133
Global Instance excl_cmra_discrete : Discrete A  CMRADiscrete exclR.
134 135
Proof. split. apply _. by intros []. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
136
Lemma excl_validN_inv_l n x a : {n} (Excl a  x)  x = .
Robbert Krebbers's avatar
Robbert Krebbers committed
137
Proof. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
138 139 140
Lemma excl_validN_inv_r n x a : {n} (x  Excl a)  x = .
Proof. by destruct x. Qed.
Lemma Excl_includedN n a x : {n} x  Excl a {n} x  x {n} Excl a.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
Proof.
142
  intros Hvalid; split; [|by intros ->].
Robbert Krebbers's avatar
Robbert Krebbers committed
143
  intros [z ?]; cofe_subst. by rewrite (excl_validN_inv_l n z a).
Robbert Krebbers's avatar
Robbert Krebbers committed
144
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
145

146 147 148 149 150 151 152
(** Internalized properties *)
Lemma excl_equivI {M} (x y : excl A) :
  (x  y)%I  (match x, y with
               | Excl a, Excl b => a  b
               | ExclUnit, ExclUnit | ExclBot, ExclBot => True
               | _, _ => False
               end : uPred M)%I.
153 154 155
Proof.
  uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
156 157
Lemma excl_validI {M} (x : excl A) :
  ( x)%I  (if x is ExclBot then False else True : uPred M)%I.
158
Proof. uPred.unseal. by destruct x. Qed.
159

160
(** ** Local updates *)
Robbert Krebbers's avatar
Robbert Krebbers committed
161 162 163
Global Instance excl_local_update y :
  LocalUpdate (λ x, if x is Excl _ then  y else False) (λ _, y).
Proof. split. apply _. by destruct y; intros n [a| |] [b'| |]. Qed.
164

165
(** Updates *)
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Lemma excl_update a y :  y  Excl a ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
Proof. destruct y; by intros ?? [?| |]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
Lemma excl_updateP (P : excl A  Prop) a y :  y  P y  Excl a ~~>: P.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
Proof. intros ?? n z ?; exists y. by destruct y, z as [?| |]. Qed.
170 171 172
End excl.

Arguments exclC : clear implicits.
173
Arguments exclR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
174

Robbert Krebbers's avatar
Robbert Krebbers committed
175
(* Functor *)
176
Definition excl_map {A B} (f : A  B) (x : excl A) : excl B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178 179
  match x with
  | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
  end.
180
Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
181
Proof. by destruct x. Qed.
182 183
Lemma excl_map_compose {A B C} (f : A  B) (g : B  C) (x : excl A) :
  excl_map (g  f) x = excl_map g (excl_map f x).
184
Proof. by destruct x. Qed.
185 186 187 188 189
Lemma excl_map_ext {A B : cofeT} (f g : A  B) x :
  ( x, f x  g x)  excl_map f x  excl_map g x.
Proof. by destruct x; constructor. Qed.
Instance excl_map_cmra_ne {A B : cofeT} n :
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
190
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
191 192
Instance excl_map_cmra_monotone {A B : cofeT} (f : A  B) :
  ( n, Proper (dist n ==> dist n) f)  CMRAMonotone (excl_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
193
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
  split; try apply _.
195
  - by intros n [a| |].
Robbert Krebbers's avatar
Robbert Krebbers committed
196 197
  - intros x y [z Hy]; exists (excl_map f z); apply equiv_dist=> n.
    move: Hy=> /equiv_dist /(_ n) ->; by destruct x, z.
Robbert Krebbers's avatar
Robbert Krebbers committed
198
Qed.
199
Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
200
  CofeMor (excl_map f).
201
Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
202
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
Ralf Jung's avatar
Ralf Jung committed
203

204
Program Definition exclRF (F : cFunctor) : rFunctor := {|
205 206
  rFunctor_car A B := exclR (cFunctor_car F A B);
  rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
207
|}.
208 209 210
Next Obligation.
  intros F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
Qed.
211 212 213 214 215 216 217 218
Next Obligation.
  intros F A B x; simpl. rewrite -{2}(excl_map_id x).
  apply excl_map_ext=>y. by rewrite cFunctor_id.
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -excl_map_compose.
  apply excl_map_ext=>y; apply cFunctor_compose.
Qed.
219 220 221 222

Instance exclRF_contractive F :
  cFunctorContractive F  rFunctorContractive (exclRF F).
Proof.
223
  intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
224
Qed.