excl.v 7.23 KB
Newer Older
1
Require Export algebra.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
Lemma excl_updateP (P : excl A  Prop) x y :  y  P y  Excl x ~~>: P.
150
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
(* Functor *)
157
Definition excl_map {A B} (f : A  B) (x : excl A) : excl B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
158 159 160
  match x with
  | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
  end.
161
Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
162
Proof. by destruct x. Qed.
163 164
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).
165
Proof. by destruct x. Qed.
166 167 168 169 170
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
171
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
172 173
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
174 175
Proof.
  split.
176
  * intros n x y [z Hy]; exists (excl_map f z); rewrite Hy.
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178 179
    by destruct x, z; constructor.
  * by intros n [a| |].
Qed.
180
Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
181
  CofeMor (excl_map f).
182
Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
183
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.