excl.v 6.27 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 14
Instance: Params (@Excl) 1 := {}.
Instance: Params (@ExclBot) 1 := {}.
15

16
Notation excl' A := (option (excl A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
17 18 19
Notation Excl' x := (Some (Excl x)).
Notation ExclBot' := (Some ExclBot).

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

23
Section excl.
24
Context {A : ofeT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
25 26
Implicit Types a b : A.
Implicit Types x y : excl A.
27

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

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

47
Definition excl_ofe_mixin : OfeMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Proof.
49 50 51
  apply (iso_ofe_mixin (maybe Excl)).
  - by intros [a|] [b|]; split; inversion_clear 1; constructor.
  - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Qed.
53
Canonical Structure exclO : ofeT := OfeT (excl A) excl_ofe_mixin.
54

55
Global Instance excl_cofe `{!Cofe A} : Cofe exclO.
56
Proof.
57 58 59
  apply (iso_cofe (from_option Excl ExclBot) (maybe Excl)).
  - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
  - by intros []; constructor.
60 61
Qed.

62
Global Instance excl_ofe_discrete : OfeDiscrete A  OfeDiscrete exclO.
63
Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
64 65
Global Instance excl_leibniz : LeibnizEquiv A  LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
66

67 68 69
Global Instance Excl_discrete a : Discrete a  Discrete (Excl a).
Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
Global Instance ExclBot_discrete : Discrete (@ExclBot A).
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Proof. by inversion_clear 1; constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71 72

(* CMRA *)
73
Instance excl_valid : Valid (excl A) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  match x with Excl _ => True | ExclBot => False end.
75
Instance excl_validN : ValidN (excl A) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
76 77 78
  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
79

80
Lemma excl_cmra_mixin : CmraMixin (excl A).
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  split; try discriminate.
83 84
  - by intros n []; destruct 1; constructor.
  - by destruct 1; intros ?.
85
  - intros x; split. done. by move=> /(_ 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
86 87 88 89
  - intros n [?|]; simpl; auto with lia.
  - by intros [?|] [?|] [?|]; constructor.
  - by intros [?|] [?|]; constructor.
  - by intros n [?|] [?|].
90
  - intros n x [?|] [?|] ? Hx; eexists _, _; inversion_clear Hx; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
Qed.
92
Canonical Structure exclR := CmraT (excl A) excl_cmra_mixin.
93

94
Global Instance excl_cmra_discrete : OfeDiscrete A  CmraDiscrete exclR.
95 96
Proof. split. apply _. by intros []. Qed.

97
(** Internalized properties *)
98 99 100 101 102 103
Lemma excl_equivI {M} x y :
  x  y @{uPredI M} match x, y with
                      | Excl a, Excl b => a  b
                      | ExclBot, ExclBot => True
                      | _, _ => False
                      end.
104 105 106
Proof.
  uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
107 108
Lemma excl_validI {M} x :
   x @{uPredI M} if x is ExclBot then False else True.
109
Proof. uPred.unseal. by destruct x. Qed.
110

111 112 113
(** Exclusive *)
Global Instance excl_exclusive x : Exclusive x.
Proof. by destruct x; intros n []. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115 116 117 118 119

(** 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.
120

121 122 123 124 125 126 127 128
Lemma Excl_includedN n a b  : Excl' a {n} Excl' b  a {n} b.
Proof.
  split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
Qed.
Lemma Excl_included a b : Excl' a  Excl' b  a  b.
Proof.
  split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
Qed.
129 130
End excl.

131
Arguments exclO : clear implicits.
132
Arguments exclR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
133

Robbert Krebbers's avatar
Robbert Krebbers committed
134
(* Functor *)
135
Definition excl_map {A B} (f : A  B) (x : excl A) : excl B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
136
  match x with Excl a => Excl (f a) | ExclBot => ExclBot end.
137
Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
138
Proof. by destruct x. Qed.
139 140
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).
141
Proof. by destruct x. Qed.
142
Lemma excl_map_ext {A B : ofeT} (f g : A  B) x :
143 144
  ( x, f x  g x)  excl_map f x  excl_map g x.
Proof. by destruct x; constructor. Qed.
145
Instance excl_map_ne {A B : ofeT} n :
146
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
148
Instance excl_map_cmra_morphism {A B : ofeT} (f : A  B) :
149
  NonExpansive f  CmraMorphism (excl_map f).
150
Proof. split; try done; try apply _. by intros n [a|]. Qed.
151 152 153
Definition exclO_map {A B} (f : A -n> B) : exclO A -n> exclO B :=
  OfeMor (excl_map f).
Instance exclO_map_ne A B : NonExpansive (@exclO_map A B).
154
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
Ralf Jung's avatar
Ralf Jung committed
155

156 157 158
Program Definition exclRF (F : oFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := (exclR (oFunctor_car F A B));
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclO_map (oFunctor_map F fg)
159
|}.
160
Next Obligation.
161
  intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_ne.
162
Qed.
163
Next Obligation.
164
  intros F A ? B ? x; simpl. rewrite -{2}(excl_map_id x).
165
  apply excl_map_ext=>y. by rewrite oFunctor_map_id.
166 167
Qed.
Next Obligation.
168
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -excl_map_compose.
169
  apply excl_map_ext=>y; apply oFunctor_map_compose.
170
Qed.
171

Robbert Krebbers's avatar
Robbert Krebbers committed
172
Instance exclRF_contractive F :
173
  oFunctorContractive F  rFunctorContractive (exclRF F).
174
Proof.
175
  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_contractive.
176
Qed.