option.v 16.3 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the option
data type that are not in the Coq standard library. *)
5
From iris.prelude Require Export tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
8
9
10
11
12

Inductive option_reflect {A} (P : A  Prop) (Q : Prop) : option A  Type :=
  | ReflectSome x : P x  option_reflect P Q (Some x)
  | ReflectNone : Q  option_reflect P Q None.

(** * General definitions and theorems *)
(** Basic properties about equality. *)
13
Lemma None_ne_Some {A} (x : A) : None  Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
Proof. congruence. Qed.
15
Lemma Some_ne_None {A} (x : A) : Some x  None.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
Proof. congruence. Qed.
17
Lemma eq_None_ne_Some {A} (mx : option A) x : mx = None  mx  Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
Proof. congruence. Qed.
19
Instance Some_inj {A} : Inj (=) (=) (@Some A).
Robbert Krebbers's avatar
Robbert Krebbers committed
20
21
22
Proof. congruence. Qed.

(** The non dependent elimination principle on the option type. *)
23
24
25
Definition default {A B} (y : B) (mx : option A) (f : A  B)  : B :=
  match mx with None => y | Some x => f x end.
Instance: Params (@default) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28

(** The [from_option] function allows us to get the value out of the option
type by specifying a default value. *)
29
30
31
Definition from_option {A} (x : A) (mx : option A) : A :=
  match mx with None => x | Some y => y end.
Instance: Params (@from_option) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
33
34

(** An alternative, but equivalent, definition of equality on the option
data type. This theorem is useful to prove that two options are the same. *)
35
36
37
Lemma option_eq {A} (mx my: option A): mx = my   x, mx = Some x  my = Some x.
Proof. split; [by intros; by subst |]. destruct mx, my; naive_solver. Qed.
Lemma option_eq_1 {A} (mx my: option A) x : mx = my  mx = Some x  my = Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
38
Proof. congruence. Qed.
39
40
Lemma option_eq_1_alt {A} (mx my : option A) x :
  mx = my  my = Some x  mx = Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
Proof. congruence. Qed.

43
44
45
46
Definition is_Some {A} (mx : option A) :=  x, mx = Some x.
Instance: Params (@is_Some) 1.

Lemma mk_is_Some {A} (mx : option A) x : mx = Some x  is_Some mx.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
49
50
51
52
Proof. intros; red; subst; eauto. Qed.
Hint Resolve mk_is_Some.
Lemma is_Some_None {A} : ¬is_Some (@None A).
Proof. by destruct 1. Qed.
Hint Resolve is_Some_None.

53
Instance is_Some_pi {A} (mx : option A) : ProofIrrel (is_Some mx).
Robbert Krebbers's avatar
Robbert Krebbers committed
54
Proof.
55
56
  set (P (mx : option A) := match mx with Some _ => True | _ => False end).
  set (f mx := match mx return P mx  is_Some mx with
Robbert Krebbers's avatar
Robbert Krebbers committed
57
    Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end).
58
59
60
61
  set (g mx (H : is_Some mx) :=
    match H return P mx with ex_intro _ p => eq_rect _ _ I _ (eq_sym p) end).
  assert ( mx H, f mx (g mx H) = H) as f_g by (by intros ? [??]; subst).
  intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct mx, p1.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Qed.
63
64
Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) :=
  match mx with
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
67
68
  | Some x => left (ex_intro _ x eq_refl)
  | None => right is_Some_None
  end.

69
70
71
72
73
Definition is_Some_proj {A} {mx : option A} : is_Some mx  A :=
  match mx with Some x => λ _, x | None => False_rect _  is_Some_None end.
Definition Some_dec {A} (mx : option A) : { x | mx = Some x } + { mx = None } :=
  match mx return { x | mx = Some x } + { mx = None } with
  | Some x => inleft (x  eq_refl _)
Robbert Krebbers's avatar
Robbert Krebbers committed
74
75
76
  | None => inright eq_refl
  end.

77
78
79
80
Lemma eq_None_not_Some {A} (mx : option A) : mx = None  ¬is_Some mx.
Proof. destruct mx; unfold is_Some; naive_solver. Qed.
Lemma not_eq_None_Some {A} (mx : option A) : mx  None  is_Some mx.
Proof. rewrite eq_None_not_Some; apply dec_stable; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96

(** Lifting a relation point-wise to option *)
Inductive option_Forall2 {A B} (P: A  B  Prop) : option A  option B  Prop :=
  | Some_Forall2 x y : P x y  option_Forall2 P (Some x) (Some y)
  | None_Forall2 : option_Forall2 P None None.
Definition option_relation {A B} (R: A  B  Prop) (P: A  Prop) (Q: B  Prop)
    (mx : option A) (my : option B) : Prop :=
  match mx, my with
  | Some x, Some y => R x y
  | Some x, None => P x
  | None, Some y => Q y
  | None, None => True
  end.

(** Setoids *)
Section setoids.
97
  Context `{Equiv A} `{!Equivalence (() : relation A)}.
98

Robbert Krebbers's avatar
Robbert Krebbers committed
99
  Global Instance option_equiv : Equiv (option A) := option_Forall2 ().
100
101
102
103

  Lemma equiv_option_Forall2 mx my : mx  my  option_Forall2 () mx my.
  Proof. split; destruct 1; constructor; auto. Qed.

104
  Global Instance option_equivalence : Equivalence (() : relation (option A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
  Proof.
    split.
107
108
    - by intros []; constructor.
    - by destruct 1; constructor.
109
    - destruct 1; inversion 1; constructor; etrans; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
112
113
  Qed.
  Global Instance Some_proper : Proper (() ==> ()) (@Some A).
  Proof. by constructor. Qed.
  Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
114
  Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
115

116
117
  Lemma equiv_None (mx : option A) : mx  None  mx = None.
  Proof. split; [by inversion_clear 1|by intros ->]. Qed.
118
  Lemma equiv_Some_inv_l (mx my : option A) x :
119
120
    mx  my  mx = Some x   y, my = Some y  x  y.
  Proof. destruct 1; naive_solver. Qed.
121
122
123
124
  Lemma equiv_Some_inv_r (mx my : option A) y :
    mx  my  mx = Some y   x, mx = Some x  x  y.
  Proof. destruct 1; naive_solver. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
125
126
  Global Instance is_Some_proper : Proper (() ==> iff) (@is_Some A).
  Proof. inversion_clear 1; split; eauto. Qed.
127
128
129
  Global Instance from_option_proper :
    Proper (() ==> () ==> ()) (@from_option A).
  Proof. by destruct 2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
132
End setoids.

(** Equality on [option] is decidable. *)
133
134
135
136
137
138
Instance option_eq_None_dec {A} (mx : option A) : Decision (mx = None) :=
  match mx with Some _ => right (Some_ne_None _) | None => left eq_refl end.
Instance option_None_eq_dec {A} (mx : option A) : Decision (None = mx) :=
  match mx with Some _ => right (None_ne_Some _) | None => left eq_refl end.
Instance option_eq_dec {A} {dec :  x y : A, Decision (x = y)}
  (mx my : option A) : Decision (mx = my).
Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
Proof.
 refine
141
142
  match mx, my with
  | Some x, Some y => cast_if (decide (x = y))
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
145
146
147
148
  | None, None => left _ | _, _ => right _
  end; clear dec; abstract congruence.
Defined.

(** * Monadic operations *)
Instance option_ret: MRet option := @Some.
149
150
151
152
Instance option_bind: MBind option := λ A B f mx,
  match mx with Some x => f x | None => None end.
Instance option_join: MJoin option := λ A mmx,
  match mmx with Some mx => mx | None => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
Instance option_fmap: FMap option := @option_map.
154
155
Instance option_guard: MGuard option := λ P dec A f,
  match dec with left H => f H | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
156

157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
Lemma fmap_is_Some {A B} (f : A  B) mx : is_Some (f <$> mx)  is_Some mx.
Proof. unfold is_Some; destruct mx; naive_solver. Qed.
Lemma fmap_Some {A B} (f : A  B) mx y :
  f <$> mx = Some y   x, mx = Some x  y = f x.
Proof. destruct mx; naive_solver. Qed.
Lemma fmap_None {A B} (f : A  B) mx : f <$> mx = None  mx = None.
Proof. by destruct mx. Qed.
Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
Proof. by destruct mx. Qed.
Lemma option_fmap_compose {A B} (f : A  B) {C} (g : B  C) mx :
  g  f <$> mx = g <$> f <$> mx.
Proof. by destruct mx. Qed.
Lemma option_fmap_ext {A B} (f g : A  B) mx :
  ( x, f x = g x)  f <$> mx = g <$> mx.
Proof. intros; destruct mx; f_equal/=; auto. Qed.
Lemma option_fmap_setoid_ext `{Equiv A, Equiv B} (f g : A  B) mx :
  ( x, f x  g x)  f <$> mx  g <$> mx.
Proof. destruct mx; constructor; auto. Qed.
Lemma option_fmap_bind {A B C} (f : A  B) (g : B  option C) mx :
  (f <$> mx) = g = mx = g  f.
Proof. by destruct mx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
Lemma option_bind_assoc {A B C} (f : A  option B)
179
180
181
182
183
184
185
  (g : B  option C) (mx : option A) : (mx = f) = g = mx = (mbind g  f).
Proof. by destruct mx; simpl. Qed.
Lemma option_bind_ext {A B} (f g : A  option B) mx my :
  ( x, f x = g x)  mx = my  mx = f = my = g.
Proof. destruct mx, my; naive_solver. Qed.
Lemma option_bind_ext_fun {A B} (f g : A  option B) mx :
  ( x, f x = g x)  mx = f = mx = g.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
Proof. intros. by apply option_bind_ext. Qed.
187
188
189
190
191
192
193
194
Lemma bind_Some {A B} (f : A  option B) (mx : option A) y :
  mx = f = Some y   x, mx = Some x  f x = Some y.
Proof. destruct mx; naive_solver. Qed.
Lemma bind_None {A B} (f : A  option B) (mx : option A) :
  mx = f = None  mx = None   x, mx = Some x  f x = None.
Proof. destruct mx; naive_solver. Qed.
Lemma bind_with_Some {A} (mx : option A) : mx = Some = mx.
Proof. by destruct mx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223

(** ** Inverses of constructors *)
(** We can do this in a fancy way using dependent types, but rewrite does
not particularly like type level reductions. *)
Class Maybe {A B : Type} (c : A  B) :=
  maybe : B  option A.
Arguments maybe {_ _} _ {_} !_ /.
Class Maybe2 {A1 A2 B : Type} (c : A1  A2  B) :=
  maybe2 : B  option (A1 * A2).
Arguments maybe2 {_ _ _} _ {_} !_ /.
Class Maybe3 {A1 A2 A3 B : Type} (c : A1  A2  A3  B) :=
  maybe3 : B  option (A1 * A2 * A3).
Arguments maybe3 {_ _ _ _} _ {_} !_ /.
Class Maybe4 {A1 A2 A3 A4 B : Type} (c : A1  A2  A3  A4  B) :=
  maybe4 : B  option (A1 * A2 * A3 * A4).
Arguments maybe4 {_ _ _ _ _} _ {_} !_ /.

Instance maybe_comp `{Maybe B C c1, Maybe A B c2} : Maybe (c1  c2) := λ x,
  maybe c1 x = maybe c2.
Arguments maybe_comp _ _ _ _ _ _ _ !_ /.

Instance maybe_inl {A B} : Maybe (@inl A B) := λ xy,
  match xy with inl x => Some x | _ => None end.
Instance maybe_inr {A B} : Maybe (@inr A B) := λ xy,
  match xy with inr y => Some y | _ => None end.
Instance maybe_Some {A} : Maybe (@Some A) := id.
Arguments maybe_Some _ !_ /.

(** * Union, intersection and difference *)
224
225
226
227
228
Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
  match mx, my with
  | Some x, Some y => f x y
  | Some x, None => Some x
  | None, Some y => Some y
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230
231
  | None, None => None
  end.
Instance option_intersection_with {A} : IntersectionWith A (option A) :=
232
233
234
235
236
  λ f mx my, match mx, my with Some x, Some y => f x y | _, _ => None end.
Instance option_difference_with {A} : DifferenceWith A (option A) := λ f mx my,
  match mx, my with
  | Some x, Some y => f x y
  | Some x, None => Some x
Robbert Krebbers's avatar
Robbert Krebbers committed
237
238
239
  | None, _ => None
  end.
Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
240
241
242
243

Lemma option_union_Some {A} (mx my : option A) z :
  mx  my = Some z  mx = Some z  my = Some z.
Proof. destruct mx, my; naive_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
245
246
247
248
249
250

Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
  Global Instance: LeftId (=) None (union_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: RightId (=) None (union_with f).
  Proof. by intros [?|]. Qed.
251
252
  Global Instance: Comm (=) f  Comm (=) (union_with f).
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
254
255
256
  Global Instance: LeftAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: RightAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
257
258
  Global Instance: Comm (=) f  Comm (=) (intersection_with f).
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
260
261
262
263
264
265
266
  Global Instance: RightId (=) None (difference_with f).
  Proof. by intros [?|]. Qed.
End option_union_intersection_difference.

(** * Tactics *)
Tactic Notation "case_option_guard" "as" ident(Hx) :=
  match goal with
  | H : appcontext C [@mguard option _ ?P ?dec] |- _ =>
267
268
    change (@mguard option _ P dec) with (λ A (f : P  option A),
      match @decide P dec with left H' => f H' | _ => None end) in *;
Robbert Krebbers's avatar
Robbert Krebbers committed
269
270
    destruct_decide (@decide P dec) as Hx
  | |- appcontext C [@mguard option _ ?P ?dec] =>
271
272
    change (@mguard option _ P dec) with (λ A (f : P  option A),
      match @decide P dec with left H' => f H' | _ => None end) in *;
Robbert Krebbers's avatar
Robbert Krebbers committed
273
274
275
276
277
    destruct_decide (@decide P dec) as Hx
  end.
Tactic Notation "case_option_guard" :=
  let H := fresh in case_option_guard as H.

278
279
Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
  P  guard P; mx = mx.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
Proof. intros. by case_option_guard. Qed.
281
282
Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
  ¬P  guard P; mx = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
Proof. intros. by case_option_guard. Qed.
284
285
Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) :
  (P  Q)  guard P; mx = guard Q; mx.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
287
Proof. intros [??]. repeat case_option_guard; intuition. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
288
Tactic Notation "simpl_option" "by" tactic3(tac) :=
289
  let assert_Some_None A mx H := first
Robbert Krebbers's avatar
Robbert Krebbers committed
290
    [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x;
291
292
      assert (mx = Some x') as H by tac
    | assert (mx = None) as H by tac ]
Robbert Krebbers's avatar
Robbert Krebbers committed
293
294
295
296
  in repeat match goal with
  | H : appcontext [@mret _ _ ?A] |- _ =>
     change (@mret _ _ A) with (@Some A) in H
  | |- appcontext [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
297
298
299
300
301
302
303
304
305
306
  | H : context [mbind (M:=option) (A:=?A) ?f ?mx] |- _ =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
  | H : context [fmap (M:=option) (A:=?A) ?f ?mx] |- _ =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
  | H : context [default (A:=?A) _ ?mx _] |- _ =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
  | H : context [from_option (A:=?A) _ ?mx] |- _ =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
  | H : context [ match ?mx with _ => _ end ] |- _ =>
    match type of mx with
Robbert Krebbers's avatar
Robbert Krebbers committed
307
    | option ?A =>
308
      let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
309
    end
310
311
312
313
314
315
316
317
318
319
  | |- context [mbind (M:=option) (A:=?A) ?f ?mx] =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
  | |- context [fmap (M:=option) (A:=?A) ?f ?mx] =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
  | |- context [default (A:=?A) _ ?mx _] =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
  | |- context [from_option (A:=?A) _ ?mx] =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
  | |- context [ match ?mx with _ => _ end ] =>
    match type of mx with
Robbert Krebbers's avatar
Robbert Krebbers committed
320
    | option ?A =>
321
      let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
322
323
324
325
326
327
328
329
330
    end
  | H : context [decide _] |- _ => rewrite decide_True in H by tac
  | H : context [decide _] |- _ => rewrite decide_False in H by tac
  | H : context [mguard _ _] |- _ => rewrite option_guard_False in H by tac
  | H : context [mguard _ _] |- _ => rewrite option_guard_True in H by tac
  | _ => rewrite decide_True by tac
  | _ => rewrite decide_False by tac
  | _ => rewrite option_guard_True by tac
  | _ => rewrite option_guard_False by tac
331
332
333
334
  | H : context [None  _] |- _ => rewrite (left_id_L None ()) in H
  | H : context [_  None] |- _ => rewrite (right_id_L None ()) in H
  | |- context [None  _] => rewrite (left_id_L None ())
  | |- context [_  None] => rewrite (right_id_L None ())
Robbert Krebbers's avatar
Robbert Krebbers committed
335
  end.
336
Tactic Notation "simplify_option_eq" "by" tactic3(tac) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
337
  repeat match goal with
338
  | _ => progress simplify_eq/=
Robbert Krebbers's avatar
Robbert Krebbers committed
339
  | _ => progress simpl_option by tac
Robbert Krebbers's avatar
Robbert Krebbers committed
340
341
342
343
344
  | _ : maybe _ ?x = Some _ |- _ => is_var x; destruct x
  | _ : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
  | _ : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
  | _ : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
  | H : _  _ = Some _ |- _ => apply option_union_Some in H; destruct H
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
  | H : mbind (M:=option) ?f ?mx = ?my |- _ =>
    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
    let x := fresh in destruct mx as [x|] eqn:?;
      [change (f x = my) in H|change (None = my) in H]
  | H : ?my = mbind (M:=option) ?f ?mx |- _ =>
    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
    let x := fresh in destruct mx as [x|] eqn:?;
      [change (my = f x) in H|change (my = None) in H]
  | H : fmap (M:=option) ?f ?mx = ?my |- _ =>
    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
    let x := fresh in destruct mx as [x|] eqn:?;
      [change (Some (f x) = my) in H|change (None = my) in H]
  | H : ?my = fmap (M:=option) ?f ?mx |- _ =>
    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
    let x := fresh in destruct mx as [x|] eqn:?;
      [change (my = Some (f x)) in H|change (my = None) in H]
Robbert Krebbers's avatar
Robbert Krebbers committed
365
366
367
  | _ => progress case_decide
  | _ => progress case_option_guard
  end.
368
Tactic Notation "simplify_option_eq" := simplify_option_eq by eauto.