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

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

(* CMRA *)
80
Instance excl_valid : Valid (excl A) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
81
  match x with Excl _ | ExclUnit => True | ExclBot => False end.
82
Instance excl_validN : ValidN (excl A) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
83
  match x with Excl _ | ExclUnit => True | ExclBot => n = 0 end.
84 85 86
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
87 88 89 90 91
  match x, y with
  | Excl x, ExclUnit | ExclUnit, Excl x => Excl x
  | ExclUnit, ExclUnit => ExclUnit
  | _, _=> ExclBot
  end.
92
Instance excl_minus : Minus (excl A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94 95 96 97
  match x, y with
  | _, ExclUnit => x
  | Excl _, Excl _ => ExclUnit
  | _, _ => ExclBot
  end.
98
Definition excl_cmra_mixin : CMRAMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
99 100
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
  * by intros n []; destruct 1; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
  * constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
103 104 105 106 107 108
  * 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
109 110 111 112
  * by intros [?| |] [?| |] [?| |]; constructor.
  * by intros [?| |] [?| |]; constructor.
  * by intros [?| |]; constructor.
  * constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114 115
  * by intros n [?| |] [?| |]; exists .
  * by intros n [?| |] [?| |].
  * by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
Qed.
117
Global Instance excl_empty_ra : RAIdentity (excl A).
118
Proof. split. done. by intros []. Qed.
119
Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
120 121 122 123 124 125 126 127
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.
128 129
Canonical Structure exclRA : cmraT :=
  CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
130 131

(* Updates *)
132
Lemma excl_update (x : A) y :  y  Excl x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
Proof. by destruct y; intros ? [?| |]. Qed.
134 135 136 137
End excl.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
139 140 141 142 143
(* Functor *)
Instance excl_fmap : FMap excl := λ A B f x,
  match x with
  | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
  end.
144
Instance excl_fmap_cmra_ne {A B : cofeT} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146
  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.
147
Instance excl_fmap_cmra_monotone {A B : cofeT} :
Robbert Krebbers's avatar
Robbert Krebbers committed
148 149 150 151 152 153 154
  ( 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.
155
Definition exclRA_map {A B} (f : A -n> B) : exclRA A -n> exclRA B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
156 157 158
  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.