excl.v 7.07 KB
Newer Older
1
Require Export modures.cmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _  !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
5
6

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

15
16
17
Section excl.
Context {A : cofeT}.

Robbert Krebbers's avatar
Robbert Krebbers committed
18
(* Cofe *)
19
Inductive excl_equiv : Equiv (excl A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
20
  | Excl_equiv (x y : A) : x  y  Excl x  Excl y
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  | ExclUnit_equiv : ExclUnit  ExclUnit
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
  | ExclBot_equiv : ExclBot  ExclBot.
Existing Instance excl_equiv.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
25
26
27
28
29
Inductive excl_dist `{Dist A} : Dist (excl A) :=
  | excl_dist_0 (x y : excl A) : x ={0}= y
  | 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.
Existing Instance excl_dist.
30
31
32
33
34
35
36
37
Global Instance Excl_ne : Proper (dist n ==> dist n) (@Excl A).
Proof. by constructor. Qed.
Global Instance Excl_proper : Proper (() ==> ()) (@Excl A).
Proof. by constructor. Qed.
Global Instance Excl_inj : Injective () () (@Excl A).
Proof. by inversion_clear 1. Qed.
Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A).
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 ?; simpl; destruct (c 1) eqn:?; simplify_equality'.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
45
46
47
  destruct (decide (i = 0)) as [->|].
  { by replace n with 0 by lia. }
  feed inversion (chain_cauchy c 1 i); auto with lia congruence.
  feed inversion (chain_cauchy c n i); simpl; auto with lia congruence.
Qed.
48
Instance excl_compl : Compl (excl A) := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
51
  match Some_dec (maybe Excl (c 1)) with
  | inleft (exist x H) => Excl (compl (excl_chain c x H)) | inright _ => c 1
  end.
52
Definition excl_cofe_mixin : CofeMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
Proof.
  split.
  * intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
    by intros n; feed inversion (Hxy n).
  * intros n; split.
    + by intros [x| |]; constructor.
    + by destruct 1; constructor.
    + destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
  * by inversion_clear 1; constructor; apply dist_S.
  * constructor.
  * intros c n; unfold compl, excl_compl.
    destruct (decide (n = 0)) as [->|]; [constructor|].
    destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|].
    { assert (c 1 = Excl x) by (by destruct (c 1); simplify_equality').
      assert ( y, c n = Excl y) as [y Hy].
      { feed inversion (chain_cauchy c 1 n); try congruence; eauto with lia. }
      rewrite Hy; constructor.
      by rewrite (conv_compl (excl_chain c x Hx) n); simpl; rewrite Hy. }
    feed inversion (chain_cauchy c 1 n); auto with lia; constructor.
    destruct (c 1); simplify_equality'.
Qed.
75
76
77
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
78
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
79
Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Proof. by inversion_clear 1; constructor. Qed.
81
Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Proof. by inversion_clear 1; constructor. Qed.
83
Global Instance excl_timeless :
Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
  ( x : A, Timeless x)   x : excl A, Timeless x.
Proof. intros ? []; apply _. Qed.
86
87
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
88
89

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

(* Updates *)
147
Lemma excl_update (x : A) y :  y  Excl x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
Proof. by destruct y; intros ? [?| |]. Qed.
149
150
Lemma excl_updateP (P : excl A  Prop) x y :  y  P y  Excl x : P.
Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed.
151
152
153
154
End excl.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159
160
(* Functor *)
Instance excl_fmap : FMap excl := λ A B f x,
  match x with
  | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
  end.
161
162
163
164
165
Lemma excl_fmap_id {A} (x : excl A) : id <$> x = x.
Proof. by destruct x. Qed.
Lemma excl_fmap_compose {A B C} (f : A  B) (g : B  C) (x : excl A) :
  g  f <$> x = g <$> f <$> x.
Proof. by destruct x. Qed.
166
Instance excl_fmap_cmra_ne {A B : cofeT} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
167
168
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap excl _ A B).
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
169
Instance excl_fmap_cmra_monotone {A B : cofeT} :
Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
172
173
174
175
176
  ( n, Proper (dist n ==> dist n) f)  CMRAMonotone (fmap f : excl A  excl B).
Proof.
  split.
  * intros n x y [z Hy]; exists (f <$> z); rewrite Hy.
    by destruct x, z; constructor.
  * by intros n [a| |].
Qed.
177
Definition exclRA_map {A B} (f : A -n> B) : exclRA A -n> exclRA B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
178
179
180
  CofeMor (fmap f : exclRA A  exclRA B).
Lemma exclRA_map_ne A B n : Proper (dist n ==> dist n) (@exclRA_map A B).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.