excl.v 6.73 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
Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.

Robbert Krebbers's avatar
Robbert Krebbers committed
69 70 71 72
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.
73
Global Instance Excl_timeless (x : A) : Timeless x  Timeless (Excl x).
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
75
Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof. by inversion_clear 1; constructor. Qed.
77
Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Proof. by inversion_clear 1; constructor. Qed.
79
Global Instance excl_timeless :
Robbert Krebbers's avatar
Robbert Krebbers committed
80 81
  ( x : A, Timeless x)   x : excl A, Timeless x.
Proof. intros ? []; apply _. Qed.
82 83
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
84 85

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
154 155 156 157 158
(* Functor *)
Instance excl_fmap : FMap excl := λ A B f x,
  match x with
  | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
  end.
159
Instance excl_fmap_cmra_ne {A B : cofeT} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161
  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.
162
Instance excl_fmap_cmra_monotone {A B : cofeT} :
Robbert Krebbers's avatar
Robbert Krebbers committed
163 164 165 166 167 168 169
  ( 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.
170
Definition exclRA_map {A B} (f : A -n> B) : exclRA A -n> exclRA B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
171 172 173
  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.