iris-coq/iris/algebra/excl.v at master · JasonGross/iris-coq · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
From iris.algebra Require Export cmra.
From iris.prelude Require Import options.

Local Arguments validN _ _ _ _ !_ /.
Local Arguments valid _ _  !_ /.

Inductive excl (A : Type) :=
  | Excl : A → excl A
  | ExclInvalid : excl A.
Global Arguments Excl {_} _.
Global Arguments ExclInvalid {_}.

Global Instance: Params (@Excl) 1 := {}.
Global Instance: Params (@ExclInvalid) 1 := {}.

Notation excl' A := (option (excl A)).
Notation Excl' x := (Some (Excl x)).
Notation ExclInvalid' := (Some ExclInvalid).

Global Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
  match x with Excl a => Some a | _ => None end.

Section excl.
Context {SI : sidx} {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : excl A.

(* Cofe *)
Inductive excl_equiv : Equiv (excl A) :=
  | Excl_equiv a b : a ≡ b → Excl a ≡ Excl b
  | ExclInvalid_equiv : ExclInvalid ≡ ExclInvalid.
Local Existing Instance excl_equiv.
Inductive excl_dist : Dist (excl A) :=
  | Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b
  | ExclInvalid_dist n : ExclInvalid ≡{n}≡ ExclInvalid.
Local Existing Instance excl_dist.

Global Instance Excl_ne : NonExpansive (@Excl A).
Proof. by constructor. Qed.
Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A).
Proof. by constructor. Qed.
Global Instance Excl_inj : Inj (≡) (≡) (@Excl A).
Proof. by inversion_clear 1. Qed.
Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
Proof. by inversion_clear 1. Qed.

Definition excl_ofe_mixin : OfeMixin (excl A).
Proof.
  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.
Qed.
Canonical Structure exclO : ofe := Ofe (excl A) excl_ofe_mixin.

Global Instance excl_cofe `{!Cofe A} : Cofe exclO.
Proof.
  apply (iso_cofe (from_option Excl ExclInvalid) (maybe Excl)).
  - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
  - by intros []; constructor.
Qed.

Global Instance excl_ofe_discrete : OfeDiscrete A → OfeDiscrete exclO.
Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.

Global Instance Excl_discrete a : Discrete a → Discrete (Excl a).
Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
Global Instance ExclInvalid_discrete : Discrete (@ExclInvalid A).
Proof. by inversion_clear 1; constructor. Qed.

(* CMRA *)
Local Instance excl_valid_instance : Valid (excl A) := λ x,
  match x with Excl _ => True | ExclInvalid => False end.
Local Instance excl_validN_instance : ValidN (excl A) := λ n x,
  match x with Excl _ => True | ExclInvalid => False end.
Local Instance excl_pcore_instance : PCore (excl A) := λ _, None.
Local Instance excl_op_instance : Op (excl A) := λ x y, ExclInvalid.

Lemma excl_cmra_mixin : CmraMixin (excl A).
Proof.
  split; try discriminate.
  - by intros [] n; destruct 1; constructor.
  - by destruct 1; intros ?.
  - intros x; split; [done|]. by move=> /(_ 0ᵢ).
  - intros n m [?|]; simpl; auto.
  - by intros [?|] [?|] [?|]; constructor.
  - by intros [?|] [?|]; constructor.
  - by intros n [?|] [?|].
  - intros n x [?|] [?|] ? Hx; eexists _, _; inversion_clear Hx; eauto.
Qed.
Canonical Structure exclR := Cmra (excl A) excl_cmra_mixin.

Global Instance excl_cmra_discrete : OfeDiscrete A → CmraDiscrete exclR.
Proof. split; first apply _. by intros []. Qed.

Lemma excl_included x y : x ≼ y ↔ y = ExclInvalid.
Proof.
  split.
  - destruct x, y; intros [[] Hxy]; by inv Hxy.
  - intros ->. by exists ExclInvalid.
Qed.
Lemma excl_includedN n x y : x ≼{n} y ↔ y = ExclInvalid.
Proof.
  split.
  - destruct x, y; intros [[] Hxy]; by inv Hxy.
  - intros ->. by exists ExclInvalid.
Qed.

(** Exclusive *)
Global Instance excl_exclusive x : Exclusive x.
Proof. by destruct x; intros n []. Qed.

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

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.
Lemma ExclInvalid_included ea : ea ≼ ExclInvalid.
Proof. by exists ExclInvalid. Qed.
End excl.

(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
  the new unification algorithm. The old unification algorithm sometimes gets
  confused by going from [ucmra]'s to [cmra]'s and back. *)
Global Hint Extern 0 (_ ≼ ExclInvalid) => apply: ExclInvalid_included : core.

Global Arguments exclO {_} _.
Global Arguments exclR {_} _.

(* Functor *)
Definition excl_map {A B} (f : A → B) (x : excl A) : excl B :=
  match x with Excl a => Excl (f a) | ExclInvalid => ExclInvalid end.
Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
Proof. by destruct x. Qed.
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).
Proof. by destruct x. Qed.
Lemma excl_map_ext {SI : sidx} {A B : ofe} (f g : A → B) x :
  (∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x.
Proof. by destruct x; constructor. Qed.
Global Instance excl_map_ne {SI : sidx} {A B : ofe} n :
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
Global Instance excl_map_cmra_morphism {SI : sidx} {A B : ofe} (f : A → B) :
  NonExpansive f → CmraMorphism (excl_map f).
Proof. split; try done; try apply _. by intros n [a|]. Qed.
Definition exclO_map {SI : sidx} {A B} (f : A -n> B) : exclO A -n> exclO B :=
  OfeMor (excl_map f).
Global Instance exclO_map_ne {SI : sidx} A B : NonExpansive (@exclO_map SI A B).
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.

Program Definition exclRF {SI : sidx} (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)
|}.
Next Obligation.
  intros ? F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??.
  by apply exclO_map_ne, oFunctor_map_ne.
Qed.
Next Obligation.
  intros ? F A ? B ? x; simpl. rewrite -{2}(excl_map_id x).
  apply excl_map_ext=>y. by rewrite oFunctor_map_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 oFunctor_map_compose.
Qed.

Global Instance exclRF_contractive {SI : sidx} F :
  oFunctorContractive F → rFunctorContractive (exclRF F).
Proof.
  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??.
  by apply exclO_map_ne, oFunctor_map_contractive.
Qed.