optional.v 23.9 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
2
3
4
5
6
7
8
9
From refinedc.typing Require Export type.
From refinedc.typing Require Import programs int.
Set Default Proof Using "Type".

(** We need to use this unbundled approach to ensure that ROptionable
uses the same instances as Optionable.
  TODO: findout if there is a better way, maybe using Canonical Structures?
 *)
Class Optionable `{!typeG Σ} (ty : type) `{!Movable ty} (optty : type) `{!Movable optty} (ot1 ot2 : op_type) := {
10
  opt_pre : val  val  iProp Σ;
Michael Sammler's avatar
Michael Sammler committed
11
  opt_alt_sz : optty.(ty_layout) = ty.(ty_layout);
12
13
14
  opt_bin_op (bty beq : bool) v1 v2 σ v :
    ( opt_pre v1 v2 - (if bty then v1 ◁ᵥ ty else v1 ◁ᵥ optty) - v2 ◁ᵥ optty - state_ctx σ -
        eval_bin_op (if beq then EqOp else NeOp) ot1 ot2 σ v1 v2 v  val_of_int (Z_of_bool (xorb bty beq)) i32 = Some v);
Michael Sammler's avatar
Michael Sammler committed
15
}.
16
Arguments opt_pre {_ _} _ {_ _ _ _ _ _} _ _.
Michael Sammler's avatar
Michael Sammler committed
17
18
19
20
21
22
23
24
25
26
27

Class ROptionable `{!typeG Σ} (r : rtype) `{!RMovable r} (optty : type) `{!Movable optty} (ot1 ot2 : op_type) := {
  ropt_opt x :> Optionable (r.(rty) x) optty ot1 ot2;
}.

Class OptionableAgree `{!typeG Σ} (ty1 ty2 : type) : Prop :=
  optionable_dist : True.

Section optional.
  Context `{!typeG Σ}.

28
29
30
  Global Program Instance optionable_ty_of_rty r `{!RMovable r} `{!Inhabited (r.(rty_type))} optty `{!Movable optty} ot1 ot2 `{!ROptionable r optty ot1 ot2}: Optionable r optty ot1 ot2 := {|
    opt_pre v1 v2 := ( x, opt_pre (r.(rty) x) v1 v2)%I
  |}.
Michael Sammler's avatar
Michael Sammler committed
31
32
  Next Obligation. move => r???????. by rewrite ->opt_alt_sz. Qed.
  Next Obligation.
33
34
35
    iIntros(r??????? bty beq v1 v2 σ v) "Hpre Hv1 Hv2".
    destruct bty. iDestruct "Hv1" as (y) "Hv1".
    all: iApply (opt_bin_op with "Hpre [Hv1] Hv2") => /= //.
Michael Sammler's avatar
Michael Sammler committed
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
    Unshelve.
    apply inhabitant.
  Qed.

  Global Instance optionable_agree_wr1 (ty1 : rtype) p ty2 `{!OptionableAgree ty1 ty2} : OptionableAgree (p @ ty1) ty2.
  Proof. done. Qed.
  Global Instance optionable_agree_wr2 (ty2 : rtype) p ty1 `{!OptionableAgree ty1 ty2} : OptionableAgree ty1 (p @ ty2).
  Proof. done. Qed.
  Global Instance optionable_agree_id ty : OptionableAgree ty ty.
  Proof. done. Qed.

  (* Separate definition such that we can make it typeclasses opaque later. *)
  Program Definition optional_type (ty : type) (optty : type) (b : Prop) : type := {|
      ty_own β l := (b  l◁ₗ{β}ty  ¬b  l◁ₗ{β}optty)%I
  |}.
  Next Obligation.
    iIntros (??????).
    by iDestruct 1 as "[[% H]|[% H]]";iMod (ty_share with "H") => //; iModIntro; [iLeft | iRight ]; iFrame.
  Qed.
  Global Instance optional_type_ne n : Proper ((dist n) ==> (dist n) ==> (dist n) ==> (dist n)) optional_type.
  Proof. solve_type_proper. Qed.
  Global Instance optional_type_proper : Proper (() ==> () ==> () ==> ()) optional_type.
  Proof. solve_type_proper. Qed.

  (* Never use optional without the refinement! This will fail
  horribly since the implicit refinement might not be decidable! Use
  optionalO with () instead. *)
  Program Definition optional (ty : type) (optty : type) : rtype := {|
    rty_type := Prop;
    rty := optional_type ty optty
  |}.

  (* it is important that the layout of an optional computes without
  doing case distrinction on the boolean. Otherwise it is very
  annoying to use. *)
  Global Program Instance rmovable_optional ty  `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2} : RMovable (optional ty optty) := {|
    rmovable b := {|
      ty_layout := optty.(ty_layout);
      ty_own_val v := (b  v◁ᵥty  ¬b  v◁ᵥoptty)%I
  |} |}.
  Next Obligation.
    iIntros (ty?????? b ?). iDestruct 1 as "[[% Hv]|[% Hv]]";iDestruct (ty_aligned with "Hv") as %? => //.
      by rewrite opt_alt_sz.
  Qed.
  Next Obligation.
    iIntros (ty?????? b ?). iDestruct 1 as "[[% Hv]|[% Hv]]";iDestruct (ty_size_eq with "Hv") as %? => //.
      by rewrite opt_alt_sz.
  Qed.
  Next Obligation.
    iIntros (ty ? optty ???? b l) "Hl".
    iDestruct "Hl" as "[[% Hl]|[% Hl]]"; iDestruct (ty_deref with "Hl") as (?) "[? ?]"; eauto with iFrame.
  Qed.
  Next Obligation.
    iIntros (ty ? optty ???? b l v ?) "Hl Hv".
    iDestruct "Hv" as "[[% Hv]|[% Hv]]"; iDestruct (ty_ref with "[] Hl Hv") as "H"; rewrite -?opt_alt_sz//;
       [iLeft | iRight]; by iFrame.
  Qed.
  Next Obligation. done. Qed.

  (* We could add rules like *)
  (* Lemma simplify_optional_goal ty optty l β T b `{!Decision b}: *)
  (*   T (if decide b then l◁ₗ{β}ty else l◁ₗ{β}optty) -∗ *)
  (*   simplify_goal (l◁ₗ{β} b @ optional ty optty) T. *)
  (* but that would lead to the automation doing a case split out of
  despair which is not a good user experience. Thus you should make
  sure that the other rules in this file work for you, which don't
  cause unnecssary case splits. *)

  (* TODO: should be allow different opttys? *)
  Global Instance simple_subsume_place_optional ty1 ty2 optty b1 b2 `{!SimpleSubsumePlace ty1 ty2 P}:
    SimpleSubsumePlace (b1 @ optional ty1 optty) (b2 @ optional ty2 optty) (b1  b2  P).
  Proof.
    iIntros (l β) "HP Hl". iDestruct "HP" as (Hequiv) "HP".
    iDestruct "Hl" as "[[% Hl]|[% Hl]]"; [iLeft | iRight]; rewrite -Hequiv. 2: by iFrame.
    iSplit => //. iApply (@simple_subsume_place with "HP Hl").
  Qed.

  Lemma subsume_optional_optty_ref b ty optty l β T:
    ¬ b  T - subsume (l ◁ₗ{β} optty) (l ◁ₗ{β} b @ optional ty optty) T.
  Proof. iIntros "[Hb $] Hl". iRight. by iFrame. Qed.
  Global Instance subsume_optional_optty_ref_inst b ty optty l β:
    SubsumePlace l β (optty) (b @ optional ty optty)%I :=
    λ T, i2p (subsume_optional_optty_ref b ty optty l β T).

  Lemma subsume_optional_ty_ref b ty ty' optty l β T:
    b  subsume (l ◁ₗ{β} ty') (l ◁ₗ{β} ty) T - subsume (l ◁ₗ{β} ty') (l ◁ₗ{β} b @ optional ty optty) T.
  Proof. iIntros "[Hb Hsub] Hl". iDestruct ("Hsub" with "Hl") as "[? $]". iLeft. by iFrame. Qed.
  Global Instance subsume_optional_ty_ref_inst b ty ty' optty l β `{!OptionableAgree ty ty'}:
    SubsumePlace l β ty' (b @ optional ty optty)%I :=
    λ T, i2p (subsume_optional_ty_ref b ty ty' optty l β T).

  Lemma subsume_optional_val_optty_ref b ty optty v T `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2}:
    ¬ b  T - subsume (v ◁ᵥ optty) (v ◁ᵥ b @ optional ty optty) T.
  Proof. iIntros "[Hb $] Hl". iRight. by iFrame. Qed.
  Global Instance subsume_optional_val_optty_ref_inst b ty optty v `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2}:
    SubsumeVal v (optty) (b @ optional ty optty)%I :=
    λ T, i2p (subsume_optional_val_optty_ref b ty optty v T ot1 ot2).

  Lemma subsume_optional_val_ty_ref b ty ty' optty v T `{!Movable ty} `{!Movable ty'} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2}:
    b  subsume (v ◁ᵥ ty') (v ◁ᵥ ty) T - subsume (v ◁ᵥ ty') (v ◁ᵥ b @ optional ty optty) T.
  Proof. iIntros "[Hb Hsub] Hl". iDestruct ("Hsub" with "Hl") as "[? $]". iLeft. by iFrame. Qed.
  Global Instance subsume_optional_val_ty_ref_inst b ty ty' optty v `{!Movable ty} `{!Movable ty'} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2} `{!OptionableAgree ty ty'}:
    SubsumeVal v ty' (b @ optional ty optty)%I :=
    λ T, i2p (subsume_optional_val_ty_ref b ty ty' optty v T ot1 ot2).

  Inductive destruct_hint_optional :=
Michael Sammler's avatar
Michael Sammler committed
142
143
  | DestructHintOptionalEq (P : Prop)
  | DestructHintOptionalNe (P : Prop).
Michael Sammler's avatar
Michael Sammler committed
144

Michael Sammler's avatar
Michael Sammler committed
145
  Lemma type_eq_optional_refined v1 v2 ty optty `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2} T b :
146
    opt_pre ty v1 v2 
Michael Sammler's avatar
Michael Sammler committed
147
148
    destruct_hint DHintInfo (DestructHintOptionalEq b) (b - v1 ◁ᵥ ty - T (i2v (Z_of_bool false) i32) (t2mt (false @ boolean i32))) 
    destruct_hint DHintInfo (DestructHintOptionalEq (¬ b)) (¬ b - v1 ◁ᵥ optty - T (i2v (Z_of_bool true) i32) (t2mt (true @ boolean i32))) -
Michael Sammler's avatar
Michael Sammler committed
149
150
      typed_bin_op v1 (v1 ◁ᵥ b @ (optional ty optty)) v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 T.
  Proof.
151
    unfold destruct_hint. iIntros "HT Hv1 Hv2" (Φ) "HΦ".
Michael Sammler's avatar
Michael Sammler committed
152
153
    iDestruct "Hv1" as "[[% Hv1]|[% Hv1]]".
    - iApply (wp_binop_det (i2v (Z_of_bool false) i32)). iSplit. {
154
155
        iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
        iDestruct (opt_bin_op true true with "Hpre Hv1 Hv2 Hctx") as %->.
Michael Sammler's avatar
Michael Sammler committed
156
157
158
        iPureIntro. rewrite /i2v.
        have [|v' ->] := val_of_int_is_some i32 (Z_of_bool false) => //.
        naive_solver.
Michael Sammler's avatar
Michael Sammler committed
159
      }
Michael Sammler's avatar
Michael Sammler committed
160
161
162
163
      iDestruct "HT" as "[_ [HT _]]".
      iDestruct ("HT" with "[//] Hv1") as "HT".
      by iApply ("HΦ" with "[] HT").
    - iApply (wp_binop_det (i2v (Z_of_bool true) i32)). iSplit. {
164
165
        iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
        iDestruct (opt_bin_op false true with "Hpre Hv1 Hv2 Hctx") as %->.
Michael Sammler's avatar
Michael Sammler committed
166
167
168
        iPureIntro. rewrite /i2v.
        have [|v' ->] := val_of_int_is_some i32 (Z_of_bool true) => //.
        naive_solver.
Michael Sammler's avatar
Michael Sammler committed
169
      }
Michael Sammler's avatar
Michael Sammler committed
170
171
172
      iDestruct "HT" as "[_ [_ HT]]".
      iDestruct ("HT" with "[//] Hv1") as "HT".
      by iApply ("HΦ" with "[] HT").
Michael Sammler's avatar
Michael Sammler committed
173
  Qed.
Michael Sammler's avatar
Michael Sammler committed
174
  Global Instance type_eq_optional_refined_inst v1 v2 ty optty `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2} b :
Michael Sammler's avatar
Michael Sammler committed
175
176
177
178
    TypedBinOp v1 (v1 ◁ᵥ b @ (optional ty optty))%I v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 :=
    λ T, i2p (type_eq_optional_refined v1 v2 ty optty ot1 ot2 T b).

  Lemma type_eq_optional_neq v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} T :
179
    opt_pre ty v1 v2 
Michael Sammler's avatar
Michael Sammler committed
180
181
182
183
184
    ( v, v1 ◁ᵥ ty - T v (t2mt (false @ boolean i32)) ) -
      typed_bin_op v1 (v1 ◁ᵥ ty) v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 T.
  Proof.
    iIntros "HT Hv1 Hv2". iIntros (Φ) "HΦ".
    have [|v' Hv] := val_of_int_is_some i32 (Z_of_bool false) => //.
185
186
187
188
    iApply (wp_binop_det v'). iSplit. {
      iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
      iDestruct (opt_bin_op true true with "Hpre Hv1 Hv2 Hctx") as %->.
      iPureIntro. by split => ?; simpl in *; simplify_eq.
Michael Sammler's avatar
Michael Sammler committed
189
190
191
192
193
194
195
196
197
    }
    iDestruct ("HT" with "Hv1") as "HT".
    iApply "HΦ" => //. by rewrite /ty_own_val/=.
  Qed.

  Global Instance type_eq_optional_neq_inst v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} :
    TypedBinOp v1 (v1 ◁ᵥ ty) v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 :=
    λ T, i2p (type_eq_optional_neq v1 v2 ty optty ot1 ot2 T).

Michael Sammler's avatar
Michael Sammler committed
198
  Lemma type_neq_optional v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} T b :
199
    opt_pre ty v1 v2 
Michael Sammler's avatar
Michael Sammler committed
200
201
    destruct_hint DHintInfo (DestructHintOptionalNe b) (b - v1 ◁ᵥ ty - T (i2v (Z_of_bool true) i32) (t2mt (true @ boolean i32))) 
    destruct_hint DHintInfo (DestructHintOptionalNe (¬ b)) (¬ b - v1 ◁ᵥ optty - T (i2v (Z_of_bool false) i32) (t2mt (false @ boolean i32))) -
Michael Sammler's avatar
Michael Sammler committed
202
203
      typed_bin_op v1 (v1 ◁ᵥ b @ (optional ty optty)) v2 (v2 ◁ᵥ optty) NeOp ot1 ot2 T.
  Proof.
Michael Sammler's avatar
Michael Sammler committed
204
205
206
    unfold destruct_hint. iIntros "HT Hv1 Hv2" (Φ) "HΦ".
    iDestruct "Hv1" as "[[% Hv1]|[% Hv1]]".
    - iApply (wp_binop_det (i2v (Z_of_bool true) i32)). iSplit. {
207
208
        iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
        iDestruct (opt_bin_op true false with "Hpre Hv1 Hv2 Hctx") as %->.
Michael Sammler's avatar
Michael Sammler committed
209
210
211
        iPureIntro. rewrite /i2v.
        have [|v' ->] := val_of_int_is_some i32 (Z_of_bool true) => //.
        naive_solver.
Michael Sammler's avatar
Michael Sammler committed
212
      }
Michael Sammler's avatar
Michael Sammler committed
213
214
215
216
      iDestruct "HT" as "[_ [HT _]]".
      iDestruct ("HT" with "[//] Hv1") as "HT".
      by iApply ("HΦ" with "[] HT").
    - iApply (wp_binop_det (i2v (Z_of_bool false) i32)). iSplit. {
217
218
        iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
        iDestruct (opt_bin_op false false with "Hpre Hv1 Hv2 Hctx") as %->.
Michael Sammler's avatar
Michael Sammler committed
219
220
221
        iPureIntro. rewrite /i2v.
        have [|v' ->] := val_of_int_is_some i32 (Z_of_bool false) => //.
        naive_solver.
Michael Sammler's avatar
Michael Sammler committed
222
      }
Michael Sammler's avatar
Michael Sammler committed
223
224
225
      iDestruct "HT" as "[_ [_ HT]]".
      iDestruct ("HT" with "[//] Hv1") as "HT".
      by iApply ("HΦ" with "[] HT").
Michael Sammler's avatar
Michael Sammler committed
226
  Qed.
Michael Sammler's avatar
Michael Sammler committed
227
  Global Instance type_neq_optional_inst v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} b :
Michael Sammler's avatar
Michael Sammler committed
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
    TypedBinOp v1 (v1 ◁ᵥ b @ (optional ty optty))%I v2 (v2 ◁ᵥ optty) NeOp ot1 ot2 :=
    λ T, i2p (type_neq_optional v1 v2 ty optty ot1 ot2 T b).

  Global Instance strip_guarded_optional b ty ty' optty E1 E2 β `{!StripGuarded β E1 E2 ty ty'}:
    StripGuarded β E1 E2 (b @ optional ty optty) (b @ optional ty' optty ).
  Proof.
    iIntros (l E HE1 HE2) "Hs".
    iDestruct "Hs" as "[[?Hs]|[?Hs]]"; [iLeft|iRight]; iFrame.
    1: by iDestruct (strip_guarded with "Hs") as "Hs".
    iApply step_fupd_intro => //. solve_ndisj.
  Qed.

  Global Program Instance optional_copyable b ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} `{!Copyable ty} `{!Copyable optty} : Copyable (b @ optional ty optty).
  Next Obligation.
    iIntros (b ty optty ot1 ot2 ? ? ? ? ? E l ?) "[[% Hl]|[% Hl]]".
    all: iMod (copy_shr_acc with "Hl") as (?? ?) "[?[??]]" => //.
    all: iModIntro; iSplit => //; rewrite /=?opt_alt_sz => //; iExists _, _; iFrame.
    by iLeft; iFrame.
    by iRight; iFrame.
  Qed.

End optional.
Typeclasses Opaque optional_type.

Michael Sammler's avatar
Michael Sammler committed
252
253
254
Notation "'optional' == ... : P" := (DestructHintOptionalEq P) (at level 100, only printing).
Notation "'optional' != ... : P" := (DestructHintOptionalNe P) (at level 100, only printing).

Michael Sammler's avatar
Michael Sammler committed
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
Section optionalO.
  Context `{!typeG Σ}.

  Program Definition optionalO {A : Type} (ty : A  type) (optty : type) : rtype := {|
    rty_type := option A;
    rty b := if b is Some x return _ then ty x else optty
  |}.

  Global Program Instance rmovable_optionalO A (ty : A  type) ot1 ot2 `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2} : RMovable (optionalO ty optty) := {|
    rmovable b := {|
      ty_layout := optty.(ty_layout);
      ty_own_val v := (if b is Some x return _ then v◁ᵥ(ty x) else v◁ᵥoptty)%I
  |} |}.
  Next Obligation.
    iIntros (A ty?????? [x|] ?) "Hv";iDestruct (ty_aligned with "Hv") as %Ha => //.
    by rewrite -opt_alt_sz in Ha.
  Qed.
  Next Obligation.
    iIntros (A ty?????? [] v) "Hv";iDestruct (ty_size_eq with "Hv") as %Ha => //.
    by rewrite -opt_alt_sz in Ha.
  Qed.
  Next Obligation.
    iIntros (A ty ? optty ???? [] l) "Hl"; rewrite /with_refinement/ty_own/=; iDestruct (ty_deref with "Hl") as (?) "[? ?]"; eauto with iFrame.
  Qed.
  Next Obligation.
    iIntros (A ty ? optty ???? [] l v ?) "Hl Hv"; iApply (ty_ref with "[] Hl Hv") => //.
    by rewrite -opt_alt_sz.
  Qed.
  Next Obligation. done. Qed.

285
286
287
288
289
290
291
  Global Instance optionalO_loc_in_bounds A (ty : A  type) e ot β `{! x, LocInBounds (ty x) β} `{!LocInBounds ot β}:
    LocInBounds (e @ optionalO ty ot) β.
  Proof.
    constructor. iIntros (l) "Hl". rewrite /with_refinement /=.
    destruct e; by iApply (loc_in_bounds_in_bounds with "Hl").
  Qed.

Michael Sammler's avatar
Michael Sammler committed
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
  (* TODO: should be allow different opttys? *)
  Global Instance simple_subsume_place_optionalO A (ty1 : A  _) ty2 optty b `{! x, SimpleSubsumePlace (ty1 x) (ty2 x) P}:
    SimpleSubsumePlaceR (optionalO ty1 optty) (optionalO ty2 optty) b b P.
  Proof. iIntros (l β) "HP Hl". destruct b. 2: by iFrame. iApply (@simple_subsume_place with "HP Hl"). Qed.

  Lemma subsume_optionalO_optty A (ty : A  type) optty l β T b:
    b = None  T - subsume (l ◁ₗ{β} optty) (l ◁ₗ{β} b @ optionalO ty optty) T.
  Proof. by iIntros "[-> $] Hl". Qed.
  Global Instance subsume_optionalO_optty_inst A (ty : A  type) optty l β b:
    SubsumePlace l β (optty) (b @ optionalO ty optty)%I | 10 :=
    λ T, i2p (subsume_optionalO_optty A ty optty l β T b).

  Lemma subsume_optionalO_ty A (ty : A  type) optty l β T b ty':
    (is_Some b   x, b = Some x - subsume (l ◁ₗ{β} ty') (l ◁ₗ{β} ty x) T) - subsume (l ◁ₗ{β} ty') (l ◁ₗ{β} b @ optionalO ty optty) T.
  Proof. iDestruct 1 as ([x ->]) "Hsub". iIntros "Hl". by iApply "Hsub". Qed.
  Global Instance subsume_optionalO_ty_inst A (ty : A  type) optty l β b ty' `{! x, OptionableAgree (ty x) ty'}:
    SubsumePlace l β ty' (b @ optionalO ty optty)%I | 20 :=
    λ T, i2p (subsume_optionalO_ty A ty optty l β T b ty').

  Lemma subsume_optionalO_optty_val A (ty : A  type) optty v T b `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2}:
    b = None  T - subsume (v ◁ᵥ optty) (v ◁ᵥ b @ optionalO ty optty) T.
  Proof. by iIntros "[-> $] Hl". Qed.
  Global Instance subsume_optionalO_optty_val_inst A (ty : A  type) optty v b `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2}:
    SubsumeVal v (optty) (b @ optionalO ty optty)%I | 10 :=
    λ T, i2p (subsume_optionalO_optty_val A ty optty v T b).

  Lemma subsume_optionalO_ty_val A (ty : A  type) optty v T b ty' `{!Movable ty'} `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2}:
    (is_Some b   x, b = Some x - subsume (v ◁ᵥ ty') (v ◁ᵥ ty x) T) - subsume (v ◁ᵥ ty') (v ◁ᵥ b @ optionalO ty optty) T.
  Proof. iDestruct 1 as ([x ->]) "Hsub". iIntros "Hl". by iApply "Hsub". Qed.
  Global Instance subsume_optionalO_ty_val_inst A (ty : A  type) optty v b ty' `{!Movable ty'} `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2} `{! x, OptionableAgree (ty x) ty'}:
    SubsumeVal v ty' (b @ optionalO ty optty)%I | 20 :=
    λ T, i2p (subsume_optionalO_ty_val A ty optty v T b ty').

  Lemma subsume_optional_optionalO_val ty optty b T v `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2}:
    T -
    subsume (v ◁ᵥ b @ optional ty optty) (v ◁ᵥ optionalO (λ _ : (), ty) optty) T.
  Proof. iIntros "$ [[% ?]|[% ?]]"; [iExists (Some ())|iExists None]; iFrame. Qed.
  Global Instance subsume_optional_optionalO_val_inst ty optty b v `{!Movable ty} `{!Movable optty} ot1 ot2 `{!Optionable ty optty ot1 ot2} :
    SubsumeVal v (b @ optional ty optty) (optionalO (λ _ : (), ty) optty) :=
    λ T, i2p (subsume_optional_optionalO_val ty optty b T v ot1 ot2).

  Inductive destruct_hint_optionalO :=
  | DestructHintOptionalO.

  Lemma type_eq_optionalO A v1 v2 (ty : A  type) optty ot1 ot2 `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2} T b `{!Inhabited A} :
337
    opt_pre (ty (default inhabitant b)) v1 v2 
Michael Sammler's avatar
Michael Sammler committed
338
339
340
341
342
343
    destruct_hint (DHintDestruct _ b) DestructHintOptionalO
      ( v, (if b  is Some x then v1 ◁ᵥ ty x else v1 ◁ᵥ optty) - T v (t2mt ((if b is Some x then false else true) @ boolean i32))) -
      typed_bin_op v1 (v1 ◁ᵥ b @ optionalO ty optty) v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 T.
  Proof.
    unfold destruct_hint. iIntros "HT Hv1 Hv2". iIntros (Φ) "HΦ".
    destruct b.
344
345
346
347
348
    - have [|v' Hv] := val_of_int_is_some i32 (Z_of_bool false) => //.
      iApply (wp_binop_det v'). iSplit. {
        iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
        iDestruct (opt_bin_op true true with "Hpre [Hv1] [Hv2] Hctx") as %->.
        iFrame. iFrame. iPureIntro. by split => ?; simpl in *; simplify_eq.
Michael Sammler's avatar
Michael Sammler committed
349
350
351
      }
      iDestruct ("HT" with "Hv1") as "HT".
      iApply "HΦ" => //. by rewrite /ty_own_val/=.
352
353
354
355
356
    - have [|v' Hv] := val_of_int_is_some i32 (Z_of_bool true) => //.
      iApply (wp_binop_det v'). iSplit. {
        iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
        iDestruct (opt_bin_op false true with "Hpre [Hv1] [Hv2] Hctx") as %->.
        iFrame. iFrame. iPureIntro. by split => ?; simpl in *; simplify_eq.
Michael Sammler's avatar
Michael Sammler committed
357
358
359
360
361
362
363
364
365
366
      }
      iDestruct ("HT" with "Hv1") as "HT".
      iApply "HΦ" => //. by rewrite /ty_own_val/=.
  Qed.

  Global Instance type_eq_optionalO_inst A v1 v2 (ty : A  type) optty ot1 ot2 `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2} b `{!Inhabited A} :
    TypedBinOp v1 (v1 ◁ᵥ b @ optionalO ty optty)%I v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 :=
    λ T, i2p (type_eq_optionalO A v1 v2 ty optty ot1 ot2 T b).

  Lemma type_neq_optionalO A v1 v2 (ty : A  type) optty ot1 ot2 `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2} T b `{!Inhabited A} :
367
    opt_pre (ty (default inhabitant b)) v1 v2 
Michael Sammler's avatar
Michael Sammler committed
368
369
370
371
372
373
    destruct_hint (DHintDestruct _ b) DestructHintOptionalO
      ( v, (if b is Some x then v1 ◁ᵥ ty x else v1 ◁ᵥ optty) - T v (t2mt ((if b is Some x then true else false) @ boolean i32))) -
      typed_bin_op v1 (v1 ◁ᵥ b @ optionalO ty optty) v2 (v2 ◁ᵥ optty) NeOp ot1 ot2 T.
  Proof.
    unfold destruct_hint. iIntros "HT Hv1 Hv2". iIntros (Φ) "HΦ".
    destruct b.
374
375
376
377
378
    - have [|v' Hv] := val_of_int_is_some i32 (Z_of_bool true) => //.
      iApply (wp_binop_det v'). iSplit. {
        iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
        iDestruct (opt_bin_op true false with "Hpre [Hv1] [Hv2] Hctx") as %->.
        iFrame. iFrame. iPureIntro. by split => ?; simpl in *; simplify_eq.
Michael Sammler's avatar
Michael Sammler committed
379
380
381
      }
      iDestruct ("HT" with "Hv1") as "HT".
      iApply "HΦ" => //. by rewrite /ty_own_val/=.
382
383
384
385
386
    - have [|v' Hv] := val_of_int_is_some i32 (Z_of_bool false) => //.
      iApply (wp_binop_det v'). iSplit. {
        iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
        iDestruct (opt_bin_op false false with "Hpre [Hv1] [Hv2] Hctx") as %->.
        iFrame. iFrame. iPureIntro. by split => ?; simpl in *; simplify_eq.
Michael Sammler's avatar
Michael Sammler committed
387
388
389
390
391
392
393
394
      }
      iDestruct ("HT" with "Hv1") as "HT".
      iApply "HΦ" => //. by rewrite /ty_own_val/=.
  Qed.
  Global Instance type_neq_optionalO_inst A v1 v2 (ty : A  type) optty ot1 ot2 `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2} b `{!Inhabited A} :
    TypedBinOp v1 (v1 ◁ᵥ b @ optionalO ty optty)%I v2 (v2 ◁ᵥ optty) NeOp ot1 ot2 :=
    λ T, i2p (type_neq_optionalO A v1 v2 ty optty ot1 ot2 T b).

395
396
397
  Lemma read_optionalO_case A l b (ty : A  type) optty ly (T : val  type  _) a:
    destruct_hint (DHintDestruct _ b) DestructHintOptionalO (typed_read_end a l Own (if b is Some x then ty x else optty) ly T) -
      typed_read_end a l Own (b @ optionalO ty optty) ly T.
Michael Sammler's avatar
Michael Sammler committed
398
399
  Proof. by destruct b. Qed.
  (* This should be tried very late *)
400
401
402
  Global Instance read_optionalO_case_inst A l b (ty : A  type) optty ly a:
    TypedReadEnd a l Own (b @ optionalO ty optty) ly | 1001 :=
    λ T, i2p (read_optionalO_case A l b ty optty ly T a).
Michael Sammler's avatar
Michael Sammler committed
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435


  Global Instance strip_guarded_optionalO A x E1 E2 (ty : A  type) ty' optty β `{! y, StripGuarded β E1 E2 (ty y) (ty' y)}:
    StripGuarded β E1 E2 (x @ optionalO ty optty) (x @ optionalO ty' optty).
  Proof.
    iIntros (l E HE1 HE2) "Hs".
    destruct x as [x|]; first by iDestruct (strip_guarded with "Hs") as "Hs".
    iFrame. iApply step_fupd_intro => //. solve_ndisj.
  Qed.

  Global Instance strip_guarded_optionalO_unrefined A E1 E2 (ty : A  type) ty' optty β `{! y, StripGuarded β E1 E2 (ty y) (ty' y)}:
    StripGuarded β E1 E2 (optionalO ty optty) (optionalO ty' optty).
  Proof.
    iIntros (l E HE1 HE2). iDestruct 1 as (x) "Hs". iExists x.
    destruct x as [x|]; first by iDestruct (strip_guarded with "Hs") as "Hs".
    iFrame. iApply step_fupd_intro => //. solve_ndisj.
  Qed.

  Global Program Instance optionalO_copyable A (ty : A  type) optty x ot1 ot2 `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2} `{! x, Copyable (ty x)} `{!Copyable optty} : Copyable (x @ optionalO ty optty).
  Next Obligation.
    iIntros (A ty optty x ot1 ot2 ? ? ? ? ? E l ?). destruct x.
    all: iIntros "Hl".
    all: iMod (copy_shr_acc with "Hl") as (Hl ? ?) "[?[??]]" => //.
    all: iModIntro; iSplit => //=.
    1: by rewrite -opt_alt_sz in Hl.
    all: iExists _, _; iFrame.
  Qed.
End optionalO.


Section int_optional.
  Context `{!typeG Σ}.

436
437
438
439
440
  Global Program Instance int_neg_optional (n : nat) it :
    Optionable (n @ int it) ((-1) @ int it)%I (IntOp it) (IntOp it) := {|
    opt_pre _ _ := True%I
  |}.
  Next Obligation. move => ??.  done. Qed.
Michael Sammler's avatar
Michael Sammler committed
441
  Next Obligation.
442
    move => ?? [] [] ????; iIntros "_" (Hv1 Hv2) "_ !%";
Michael Sammler's avatar
Michael Sammler committed
443
444
445
446
447
448
449
    rewrite val_of_int_bool;
    move: (Hv1) (Hv2) => /val_to_of_int? /val_to_of_int?;
    split => Hin; first [
       by simplify_eq; econstructor => //; case_bool_decide => //; lia |
       by inversion Hin; simplify_eq; case_bool_decide => //; lia].
  Qed.
End int_optional.