excl.v 7.49 KB
Newer Older
1
Require Export algebra.cmra.
Ralf Jung's avatar
Ralf Jung committed
2
Require Import algebra.functor.
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 26 27 28 29 30
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.
31 32 33 34 35 36 37 38
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.
39
Program Definition excl_chain
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41 42
    (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.
43
  intros c x ? n i ?; simpl; destruct (c 1) eqn:?; simplify_equality'.
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45 46 47 48
  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.
49
Instance excl_compl : Compl (excl A) := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51 52
  match Some_dec (maybe Excl (c 1)) with
  | inleft (exist x H) => Excl (compl (excl_chain c x H)) | inright _ => c 1
  end.
53
Definition excl_cofe_mixin : CofeMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75
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.
76 77 78
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
79
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
80
Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Proof. by inversion_clear 1; constructor. Qed.
82
Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Proof. by inversion_clear 1; constructor. Qed.
84
Global Instance excl_timeless :
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86
  ( x : A, Timeless x)   x : excl A, Timeless x.
Proof. intros ? []; apply _. Qed.
87 88
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
89 90

(* CMRA *)
91
Instance excl_validN : ValidN (excl A) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
92
  match x with Excl _ | ExclUnit => True | ExclBot => n = 0 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 97 98 99 100
  match x, y with
  | Excl x, ExclUnit | ExclUnit, Excl x => Excl x
  | ExclUnit, ExclUnit => ExclUnit
  | _, _=> ExclBot
  end.
101
Instance excl_minus : Minus (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.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
  * by intros n []; destruct 1; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  * constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
112 113 114 115
  * 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
116 117 118 119
  * by intros [?| |] [?| |] [?| |]; constructor.
  * by intros [?| |] [?| |]; constructor.
  * by intros [?| |]; constructor.
  * constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
120 121 122
  * by intros n [?| |] [?| |]; exists .
  * by intros n [?| |] [?| |].
  * by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Qed.
124
Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
125 126 127 128 129 130 131 132
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.
133 134
Canonical Structure exclRA : cmraT :=
  CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
135 136
Global Instance excl_cmra_identity : CMRAIdentity exclRA.
Proof. split. done. by intros []. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138 139 140
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
141 142 143 144 145
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
146 147

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

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

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

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.