excl.v 6 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

Robbert Krebbers's avatar
Robbert Krebbers committed
15
(* Cofe *)
Robbert Krebbers's avatar
Robbert Krebbers committed
16
17
Inductive excl_equiv `{Equiv A} : Equiv (excl A) :=
  | Excl_equiv (x y : A) : x  y  Excl x  Excl y
Robbert Krebbers's avatar
Robbert Krebbers committed
18
  | ExclUnit_equiv : ExclUnit  ExclUnit
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20
  | ExclBot_equiv : ExclBot  ExclBot.
Existing Instance excl_equiv.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
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.
Program Definition excl_chain `{Cofe A}
    (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.
  intros A ???? c x ? n i ?; simpl; destruct (c 1) eqn:?; simplify_equality'.
  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.
Instance excl_compl `{Cofe A} : Compl (excl A) := λ c,
  match Some_dec (maybe Excl (c 1)) with
  | inleft (exist x H) => Excl (compl (excl_chain c x H)) | inright _ => c 1
  end.
Local Instance excl_cofe `{Cofe A} : Cofe (excl A).
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Instance Excl_timeless `{Equiv A, Dist A} (x:A) :Timeless x  Timeless (Excl x).
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
67
68
69
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Instance ExclUnit_timeless `{Equiv A, Dist A} : Timeless (@ExclUnit A).
Proof. by inversion_clear 1; constructor. Qed.
Instance ExclBot_timeless `{Equiv A, Dist A} : Timeless (@ExclBot A).
Proof. by inversion_clear 1; constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
72
Instance excl_timeless `{Equiv A, Dist A} :
  ( x : A, Timeless x)   x : excl A, Timeless x.
Proof. intros ? []; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74

(* CMRA *)
Robbert Krebbers's avatar
Robbert Krebbers committed
75
76
Instance excl_valid {A} : Valid (excl A) := λ x,
  match x with Excl _ | ExclUnit => True | ExclBot => False end.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
Instance excl_validN {A} : ValidN (excl A) := λ n x,
  match x with Excl _ | ExclUnit => True | ExclBot => n = 0 end.
79
80
Instance excl_empty {A} : Empty (excl A) := ExclUnit.
Instance excl_unit {A} : Unit (excl A) := λ _, .
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
83
84
85
86
87
88
89
90
91
92
Instance excl_op {A} : Op (excl A) := λ x y,
  match x, y with
  | Excl x, ExclUnit | ExclUnit, Excl x => Excl x
  | ExclUnit, ExclUnit => ExclUnit
  | _, _=> ExclBot
  end.
Instance excl_minus {A} : Minus (excl A) := λ x y,
  match x, y with
  | _, ExclUnit => x
  | Excl _, Excl _ => ExclUnit
  | _, _ => ExclBot
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Instance excl_cmra `{Cofe A} : CMRA (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97
  * apply _.
  * by intros n []; destruct 1; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
  * constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
101
102
103
104
  * by destruct 1 as [? []| | |]; intros ?.
  * by destruct 1; inversion_clear 1; constructor.
  * by intros [].
  * intros n [?| |]; simpl; auto with lia.
  * intros x; split; [by intros ? [|n]; destruct x|].
    by intros Hx; specialize (Hx 1); destruct x.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
107
108
  * by intros [?| |] [?| |] [?| |]; constructor.
  * by intros [?| |] [?| |]; constructor.
  * by intros [?| |]; constructor.
  * constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111
  * by intros n [?| |] [?| |]; exists .
  * by intros n [?| |] [?| |].
  * by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
Qed.
113
Instance excl_empty_ra `{Cofe A} : RAIdentity (excl A).
114
Proof. split. done. by intros []. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
115
116
117
118
119
120
121
122
123
Instance excl_extend `{Cofe A} : CMRAExtend (excl A).
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
Instance excl_valid_timeless {A} (x : excl A) : ValidTimeless x.
Proof. by destruct x; intros ?. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127

(* Updates *)
Robbert Krebbers's avatar
Robbert Krebbers committed
128
Lemma excl_update {A} (x : A) y :  y  Excl x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
Proof. by destruct y; intros ? [?| |]. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
(* Functor *)
Definition exclRA (A : cofeT) : cmraT := CMRAT (excl A).
Instance excl_fmap : FMap excl := λ A B f x,
  match x with
  | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
  end.
Instance excl_fmap_cmra_ne `{Dist A, Dist B} n :
  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.
Instance excl_fmap_cmra_monotone `{Cofe A, Cofe B} :
  ( 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.
Definition exclRA_map {A B : cofeT} (f : A -n> B) : exclRA A -n> exclRA B :=
  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.