excl.v 6.87 KB
Newer Older
1
From iris.algebra Require Export cmra.
2
From iris.base_logic Require Import base_logic.
3
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _  !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11

Inductive excl (A : Type) :=
  | Excl : A  excl A
  | ExclBot : excl A.
Arguments Excl {_} _.
Arguments ExclBot {_}.
Robbert Krebbers's avatar
Robbert Krebbers committed
12

13
Notation excl' A := (option (excl A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16
Notation Excl' x := (Some (Excl x)).
Notation ExclBot' := (Some ExclBot).

Robbert Krebbers's avatar
Robbert Krebbers committed
17 18
Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
  match x with Excl a => Some a | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
19

20
Section excl.
21
Context {A : ofeT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
22 23
Implicit Types a b : A.
Implicit Types x y : excl A.
24

Robbert Krebbers's avatar
Robbert Krebbers committed
25
(* Cofe *)
26
Inductive excl_equiv : Equiv (excl A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
27
  | Excl_equiv a b : a  b  Excl a  Excl b
Robbert Krebbers's avatar
Robbert Krebbers committed
28 29
  | ExclBot_equiv : ExclBot  ExclBot.
Existing Instance excl_equiv.
30
Inductive excl_dist : Dist (excl A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  | Excl_dist a b n : a {n} b  Excl a {n} Excl b
32
  | ExclBot_dist n : ExclBot {n} ExclBot.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
Existing Instance excl_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
34

Robbert Krebbers's avatar
Robbert Krebbers committed
35
Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A).
36 37 38
Proof. by constructor. Qed.
Global Instance Excl_proper : Proper (() ==> ()) (@Excl A).
Proof. by constructor. Qed.
39
Global Instance Excl_inj : Inj () () (@Excl A).
40
Proof. by inversion_clear 1. Qed.
41
Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
42
Proof. by inversion_clear 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
43

44
Definition excl_ofe_mixin : OfeMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
  - intros x y; split; [by destruct 1; constructor; apply equiv_dist|].
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49
    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
    by intros n; feed inversion (Hxy n).
50
  - intros n; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
    + by intros []; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
    + by destruct 1; constructor.
53
    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
54
  - by inversion_clear 1; constructor; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Qed.
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
Canonical Structure exclC : ofeT := OfeT (excl A) excl_ofe_mixin.

Program Definition excl_chain (c : chain exclC) (a : A) : chain A :=
  {| chain_car n := match c n return _ with Excl y => y | _ => a end |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Definition excl_compl `{Cofe A} : Compl exclC := λ c,
  match c 0 with Excl a => Excl (compl (excl_chain c a)) | x => x end.
Global Program Instance excl_cofe `{Cofe A} : Cofe exclC :=
  {| compl := excl_compl |}.
Next Obligation.
  intros ? n c; rewrite /compl /excl_compl.
  feed inversion (chain_cauchy c 0 n); auto with omega.
  rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver.
Qed.

71 72 73 74
Global Instance excl_discrete : Discrete A  Discrete exclC.
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Global Instance excl_leibniz : LeibnizEquiv A  LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
75

Robbert Krebbers's avatar
Robbert Krebbers committed
76
Global Instance Excl_timeless a : Timeless a  Timeless (Excl a).
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
78
Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Proof. by inversion_clear 1; constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
80 81

(* CMRA *)
82
Instance excl_valid : Valid (excl A) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
83
  match x with Excl _ => True | ExclBot => False end.
84
Instance excl_validN : ValidN (excl A) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86 87
  match x with Excl _ => True | ExclBot => False end.
Instance excl_pcore : PCore (excl A) := λ _, None.
Instance excl_op : Op (excl A) := λ x y, ExclBot.
Robbert Krebbers's avatar
Robbert Krebbers committed
88

89
Lemma excl_cmra_mixin : CMRAMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  split; try discriminate.
92 93
  - by intros n []; destruct 1; constructor.
  - by destruct 1; intros ?.
94
  - intros x; split. done. by move=> /(_ 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96 97 98
  - intros n [?|]; simpl; auto with lia.
  - by intros [?|] [?|] [?|]; constructor.
  - by intros [?|] [?|]; constructor.
  - by intros n [?|] [?|].
99
  - intros n x [?|] [?|] ?; inversion_clear 1; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Qed.
101
Canonical Structure exclR :=
102
  CMRAT (excl A) excl_ofe_mixin excl_cmra_mixin.
103

104
Global Instance excl_cmra_discrete : Discrete A  CMRADiscrete exclR.
105 106
Proof. split. apply _. by intros []. Qed.

107 108
(** Internalized properties *)
Lemma excl_equivI {M} (x y : excl A) :
109 110 111 112 113
  x  y  (match x, y with
            | Excl a, Excl b => a  b
            | ExclBot, ExclBot => True
            | _, _ => False
            end : uPred M).
114 115 116
Proof.
  uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
117
Lemma excl_validI {M} (x : excl A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
118
   x  (if x is ExclBot then False else True : uPred M).
119
Proof. uPred.unseal. by destruct x. Qed.
120

121 122 123
(** Exclusive *)
Global Instance excl_exclusive x : Exclusive x.
Proof. by destruct x; intros n []. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
124 125 126 127 128 129

(** Option excl *)
Lemma excl_validN_inv_l n mx a : {n} (Excl' a  mx)  mx = None.
Proof. by destruct mx. Qed.
Lemma excl_validN_inv_r n mx a : {n} (mx  Excl' a)  mx = None.
Proof. by destruct mx. Qed.
130 131 132 133 134

Lemma Excl_includedN n a b  : Excl' a {n} Excl' b  a {n} b.
Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
Lemma Excl_included a b : Excl' a  Excl' b  a  b.
Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
135 136 137
End excl.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
140
(* Functor *)
141
Definition excl_map {A B} (f : A  B) (x : excl A) : excl B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
142
  match x with Excl a => Excl (f a) | ExclBot => ExclBot end.
143
Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
144
Proof. by destruct x. Qed.
145 146
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).
147
Proof. by destruct x. Qed.
148
Lemma excl_map_ext {A B : ofeT} (f g : A  B) x :
149 150
  ( x, f x  g x)  excl_map f x  excl_map g x.
Proof. by destruct x; constructor. Qed.
151
Instance excl_map_ne {A B : ofeT} n :
152
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
153
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
154
Instance excl_map_cmra_monotone {A B : ofeT} (f : A  B) :
155
  ( n, Proper (dist n ==> dist n) f)  CMRAMonotone (excl_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
  split; try apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  - by intros n [a|].
Robbert Krebbers's avatar
Robbert Krebbers committed
159 160
  - intros x y [z Hy]; exists (excl_map f z); apply equiv_dist=> n.
    move: Hy=> /equiv_dist /(_ n) ->; by destruct x, z.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
Qed.
162
Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
163
  CofeMor (excl_map f).
164
Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
165
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
Ralf Jung's avatar
Ralf Jung committed
166

Robbert Krebbers's avatar
Robbert Krebbers committed
167 168 169
Program Definition exclRF (F : cFunctor) : rFunctor := {|
  rFunctor_car A B := (exclR (cFunctor_car F A B));
  rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
170
|}.
171 172 173
Next Obligation.
  intros F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
Qed.
174 175 176 177 178 179 180 181
Next Obligation.
  intros F A B x; simpl. rewrite -{2}(excl_map_id x).
  apply excl_map_ext=>y. by rewrite cFunctor_id.
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -excl_map_compose.
  apply excl_map_ext=>y; apply cFunctor_compose.
Qed.
182

Robbert Krebbers's avatar
Robbert Krebbers committed
183 184
Instance exclRF_contractive F :
  cFunctorContractive F  rFunctorContractive (exclRF F).
185
Proof.
186
  intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
187
Qed.