excl.v 5.88 KB
Newer Older
1
Require Export iris.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 65 66 67 68 69 70
Instance Excl_timeless `{Equiv A, Dist A} (x : excl A) :
  Timeless x  Timeless (Excl x).
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
71 72

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149
(* 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.