excl.v 7.98 KB
Newer Older
1
From algebra Require Export cmra.
2
From algebra Require Import functor 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
18
Section excl.
Context {A : cofeT}.

Robbert Krebbers's avatar
Robbert Krebbers committed
19
(* Cofe *)
20
Inductive excl_equiv : Equiv (excl A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  | Excl_equiv (x y : A) : x  y  Excl x  Excl y
Robbert Krebbers's avatar
Robbert Krebbers committed
22
  | ExclUnit_equiv : ExclUnit  ExclUnit
Robbert Krebbers's avatar
Robbert Krebbers committed
23
24
  | ExclBot_equiv : ExclBot  ExclBot.
Existing Instance excl_equiv.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
Inductive excl_dist `{Dist A} : Dist (excl A) :=
26
27
28
  | Excl_dist (x y : A) n : x {n} y  Excl x {n} Excl y
  | ExclUnit_dist n : ExclUnit {n} ExclUnit
  | ExclBot_dist n : ExclBot {n} ExclBot.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Existing Instance excl_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A).
31
32
33
Proof. by constructor. Qed.
Global Instance Excl_proper : Proper (() ==> ()) (@Excl A).
Proof. by constructor. Qed.
34
Global Instance Excl_inj : Inj () () (@Excl A).
35
Proof. by inversion_clear 1. Qed.
36
Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
37
Proof. by inversion_clear 1. Qed.
38
Program Definition excl_chain
Robbert Krebbers's avatar
Robbert Krebbers committed
39
40
41
    (c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A :=
  {| chain_car n := match c n return _ with Excl y => y | _ => x end |}.
Next Obligation.
42
  intros c x ? n [|i] ?; [omega|]; simpl.
43
  destruct (c 1) eqn:?; simplify_eq/=.
44
  by feed inversion (chain_cauchy c n (S i)).
Robbert Krebbers's avatar
Robbert Krebbers committed
45
Qed.
46
Instance excl_compl : Compl (excl A) := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
49
  match Some_dec (maybe Excl (c 1)) with
  | inleft (exist x H) => Excl (compl (excl_chain c x H)) | inright _ => c 1
  end.
50
Definition excl_cofe_mixin : CofeMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
51
52
Proof.
  split.
53
  - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
    by intros n; feed inversion (Hxy n).
56
  - intros n; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
    + by intros [x| |]; constructor.
    + by destruct 1; constructor.
59
    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
60
  - by inversion_clear 1; constructor; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  - intros n c; unfold compl, excl_compl.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
    destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|].
63
    { assert (c 1 = Excl x) by (by destruct (c 1); simplify_eq/=).
64
65
      assert ( y, c (S n) = Excl y) as [y Hy].
      { feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. }
Robbert Krebbers's avatar
Robbert Krebbers committed
66
      rewrite Hy; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
      by rewrite (conv_compl n (excl_chain c x Hx)) /= Hy. }
68
    feed inversion (chain_cauchy c 0 (S n)); first lia;
69
       constructor; destruct (c 1); simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Qed.
71
72
73
Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.

Global Instance Excl_timeless (x : A) : Timeless x  Timeless (Excl x).
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
75
Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof. by inversion_clear 1; constructor. Qed.
77
Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Proof. by inversion_clear 1; constructor. Qed.
79
Global Instance excl_timeless :
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
  ( x : A, Timeless x)   x : excl A, Timeless x.
Proof. intros ? []; apply _. Qed.
82
83
Global Instance excl_leibniz : LeibnizEquiv A  LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
85

(* CMRA *)
86
Instance excl_validN : ValidN (excl A) := λ n x,
87
  match x with Excl _ | ExclUnit => True | ExclBot => False end.
88
89
90
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
91
92
93
94
95
  match x, y with
  | Excl x, ExclUnit | ExclUnit, Excl x => Excl x
  | ExclUnit, ExclUnit => ExclUnit
  | _, _=> ExclBot
  end.
96
Instance excl_minus : Minus (excl A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
97
98
99
100
101
  match x, y with
  | _, ExclUnit => x
  | Excl _, Excl _ => ExclUnit
  | _, _ => ExclBot
  end.
102
Definition excl_cmra_mixin : CMRAMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
Proof.
  split.
105
106
107
108
109
110
111
112
113
114
115
116
  - by intros n []; destruct 1; constructor.
  - constructor.
  - by destruct 1; intros ?.
  - by destruct 1; inversion_clear 1; constructor.
  - intros n [?| |]; simpl; auto with lia.
  - by intros [?| |] [?| |] [?| |]; constructor.
  - by intros [?| |] [?| |]; constructor.
  - by intros [?| |]; constructor.
  - constructor.
  - by intros n [?| |] [?| |]; exists .
  - by intros n [?| |] [?| |].
  - by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Qed.
118
Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Proof.
120
  intros n x y1 y2 ? Hx.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
123
124
125
126
  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.
Qed.
127
128
Canonical Structure exclRA : cmraT :=
  CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
129
130
Global Instance excl_cmra_identity : CMRAIdentity exclRA.
Proof. split. done. by intros []. apply _. Qed.
131
Lemma excl_validN_inv_l n x y : {n} (Excl x  y)  y = .
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Proof. by destruct y. Qed.
133
Lemma excl_validN_inv_r n x y : {n} (x  Excl y)  x = .
Robbert Krebbers's avatar
Robbert Krebbers committed
134
Proof. by destruct x. Qed.
135
Lemma Excl_includedN n x y : {n} y  Excl x {n} y  y {n} Excl x.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
Proof.
137
  intros Hvalid; split; [|by intros ->].
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
  by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
140

141
142
143
144
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.
Proof. split. by destruct 1. by destruct x, y; try constructor. Qed.
Lemma excl_validI {M} (x : excl A) :
  ( x)%I  (if x is ExclBot then False else True : uPred M)%I.
Proof. by destruct x. Qed.

153
154
155
156
157
(** ** Local updates *)
Global Instance excl_local_update b :
  LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, Excl b).
Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.

158
159
160
161
Global Instance excl_local_update_del :
LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, ExclUnit).
Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.

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

Arguments exclC : clear implicits.
Arguments exclRA : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
171

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

Program Definition exclF : iFunctor :=
  {| ifunctor_car := exclRA; ifunctor_map := @exclC_map |}.
Next Obligation. by intros A x; rewrite /= excl_map_id. Qed.
Next Obligation. by intros A B C f g x; rewrite /= excl_map_compose. Qed.