option.v 11.5 KB
Newer Older
1
(* Copyright (c) 2012-2013, Robbert Krebbers. *)
2
3
4
(* 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
Require Export base tactics decidable.
6
7
8

(** * General definitions and theorems *)
(** Basic properties about equality. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10
11
12
13
14
Lemma None_ne_Some `(a : A) : None  Some a.
Proof. congruence. Qed.
Lemma Some_ne_None `(a : A) : Some a  None.
Proof. congruence. Qed.
Lemma eq_None_ne_Some `(x : option A) a : x = None  x  Some a.
Proof. congruence. Qed.
15
Instance Some_inj {A} : Injective (=) (=) (@Some A).
Robbert Krebbers's avatar
Robbert Krebbers committed
16
17
Proof. congruence. Qed.

18
19
(** The non dependent elimination principle on the option type. *)
Definition option_case {A B} (f : A  B) (b : B) (x : option A) : B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
20
21
22
23
24
  match x with
  | None => b
  | Some a => f a
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
27
(** The [from_option] function allows us to get the value out of the option
type by specifying a default value. *)
Definition from_option {A} (a : A) (x : option A) : A :=
28
29
  match x with
  | None => a
30
  | Some b => b
31
32
  end.

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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
37
38
Lemma option_eq {A} (x y : option A) :
  x = y   a, x = Some a  y = Some a.
Proof.
  split.
39
  { intros. by subst. }
40
  intros E. destruct x, y.
41
42
43
44
  + by apply E.
  + symmetry. by apply E.
  + by apply E.
  + done.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
Qed.

47
48
Inductive is_Some {A} : option A  Prop :=
  make_is_Some x : is_Some (Some x).
Robbert Krebbers's avatar
Robbert Krebbers committed
49

50
51
52
53
54
55
56
57
58
59
60
61
62
Instance is_Some_pi {A} (x : option A) : ProofIrrel (is_Some x).
Proof.
  intros [?] p2. by refine
    match p2 in is_Some o return
      match o with
      | Some y => (make_is_Some y =)
      | _ => λ _, False
      end p2
    with
    | make_is_Some y => _
    end.
Qed.

63
64
65
66
67
68
69
70
71
72
73
Lemma make_is_Some_alt `(x : option A) a : x = Some a  is_Some x.
Proof. intros. by subst. Qed.
Hint Resolve make_is_Some_alt.
Lemma is_Some_None {A} : ¬is_Some (@None A).
Proof. by inversion 1. Qed.
Hint Resolve is_Some_None.

Lemma is_Some_alt `(x : option A) : is_Some x   y, x = Some y.
Proof. split. inversion 1; eauto. intros [??]. by subst. Qed.

Ltac inv_is_Some := repeat
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  match goal with
75
  | H : is_Some _ |- _ => inversion H; clear H; subst
76
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
77

Robbert Krebbers's avatar
Robbert Krebbers committed
78
Definition is_Some_proj `{x : option A} : is_Some x  A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  match x with
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  | Some a => λ _, a
81
82
  | None => False_rect _  is_Some_None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
84
85
86
87
Definition Some_dec `(x : option A) : { a | x = Some a } + { x = None } :=
  match x return { a | x = Some a } + { x = None } with
  | Some a => inleft (a  eq_refl _)
  | None => inright eq_refl
  end.
88
89
90
91
Instance is_Some_dec `(x : option A) : Decision (is_Some x) :=
  match x with
  | Some x => left (make_is_Some x)
  | None => right is_Some_None
Robbert Krebbers's avatar
Robbert Krebbers committed
92
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
97
Instance None_dec `(x : option A) : Decision (x = None) :=
  match x with
  | Some x => right (Some_ne_None x)
  | None => left eq_refl
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
99

Lemma eq_None_not_Some `(x : option A) : x = None  ¬is_Some x.
100
101
Proof. split. by destruct 2. destruct x. by intros []. done. Qed.
Lemma not_eq_None_Some `(x : option A) : x  None  is_Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
103

104
Lemma make_eq_Some {A} (x : option A) a :
Robbert Krebbers's avatar
Robbert Krebbers committed
105
  is_Some x  ( b, x = Some b  b = a)  x = Some a.
106
Proof. destruct 1. intros. f_equal. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
107

108
109
110
(** Equality on [option] is decidable. *)
Instance option_eq_dec `{dec :  x y : A, Decision (x = y)}
    (x y : option A) : Decision (x = y) :=
111
112
113
114
115
  match x, y with
  | Some a, Some b =>
     match dec a b with
     | left H => left (f_equal _ H)
     | right H => right (H  injective Some _ _)
Robbert Krebbers's avatar
Robbert Krebbers committed
116
     end
117
118
119
  | Some _, None => right (Some_ne_None _)
  | None, Some _ => right (None_ne_Some _)
  | None, None => left eq_refl
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
  end.

122
(** * Monadic operations *)
123
124
Instance option_ret: MRet option := @Some.
Instance option_bind: MBind option := λ A B f x,
Robbert Krebbers's avatar
Robbert Krebbers committed
125
126
127
128
  match x with
  | Some a => f a
  | None => None
  end.
129
Instance option_join: MJoin option := λ A x,
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
132
133
  match x with
  | Some x => x
  | None => None
  end.
134
135
136
Instance option_fmap: FMap option := @option_map.
Instance option_guard: MGuard option := λ P dec A x,
  if dec then x else None.
Robbert Krebbers's avatar
Robbert Krebbers committed
137

138
139
140
141
142
143
144
145
Definition mapM `{!MBind M} `{!MRet M} {A B}
    (f : A  M B) : list A  M (list B) :=
  fix go l :=
  match l with
  | [] => mret []
  | x :: l => y  f x; k  go l; mret (y :: k)
  end.

146
147
148
149
150
151
152
153
Lemma fmap_is_Some {A B} (f : A  B) (x : option A) :
  is_Some (f <$> x)  is_Some x.
Proof. split; inversion 1. by destruct x. done. Qed.
Lemma fmap_Some {A B} (f : A  B) (x : option A) y :
  f <$> x = Some y   x', x = Some x'  y = f x'.
Proof. unfold fmap, option_fmap. destruct x; naive_solver. Qed.
Lemma fmap_None {A B} (f : A  B) (x : option A) :
  f <$> x = None  x = None.
154
Proof. unfold fmap, option_fmap. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155

156
157
158
Lemma option_fmap_id {A} (x : option A) :
  id <$> x = x.
Proof. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
161
Lemma option_bind_assoc {A B C} (f : A  option B)
    (g : B  option C) (x : option A) : (x = f) = g = x = (mbind g  f).
Proof. by destruct x; simpl. Qed.
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
Lemma option_bind_ext {A B} (f g : A  option B) x y :
  ( a, f a = g a) 
  x = y 
  x = f = y = g.
Proof. intros. destruct x, y; simplify_equality; simpl; auto. Qed.
Lemma option_bind_ext_fun {A B} (f g : A  option B) x :
  ( a, f a = g a) 
  x = f = x = g.
Proof. intros. by apply option_bind_ext. Qed.

Section mapM.
  Context {A B : Type} (f : A  option B).

  Lemma mapM_ext (g : A  option B) l :
    ( x, f x = g x)  mapM f l = mapM g l.
  Proof. intros Hfg. by induction l; simpl; rewrite ?Hfg, ?IHl. Qed.
  Lemma Forall2_mapM_ext (g : A  option B) l k :
    Forall2 (λ x y, f x = g y) l k  mapM f l = mapM g k.
  Proof.
    induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH.
  Qed.
  Lemma Forall_mapM_ext (g : A  option B) l :
    Forall (λ x, f x = g x) l  mapM f l = mapM g l.
  Proof.
    induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH.
  Qed.

  Lemma mapM_Some_1 l k :
    mapM f l = Some k  Forall2 (λ x y, f x = Some y) l k.
  Proof.
    revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
    * destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
    * destruct (f x) eqn:?; simpl; [|discriminate].
      destruct (mapM f l); intros; simplify_equality. constructor; auto.
  Qed.
  Lemma mapM_Some_2 l k :
    Forall2 (λ x y, f x = Some y) l k  mapM f l = Some k.
  Proof.
    induction 1 as [|???? Hf ? IH]; simpl; [done |].
    rewrite Hf. simpl. by rewrite IH.
  Qed.
  Lemma mapM_Some l k :
    mapM f l = Some k  Forall2 (λ x y, f x = Some y) l k.
  Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed.
End mapM.
Robbert Krebbers's avatar
Robbert Krebbers committed
207

208
Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
209
  match goal with
210
  | _ => first [progress simpl in * | progress simplify_equality]
Robbert Krebbers's avatar
Robbert Krebbers committed
211
  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
212
    let Hx := fresh in
Robbert Krebbers's avatar
Robbert Krebbers committed
213
214
215
216
217
    first
      [ let x := fresh in evar (x:A);
        let x' := eval unfold x in x in clear x;
        assert (o = Some x') as Hx by tac
      | assert (o = None) as Hx by tac ];
218
    rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
  | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ =>
    let Hx := fresh in
    first
      [ let x := fresh in evar (x:A);
        let x' := eval unfold x in x in clear x;
        assert (o = Some x') as Hx by tac
      | assert (o = None) as Hx by tac ];
    rewrite Hx in H; clear Hx
  | H : context [ match ?o with _ => _ end ] |- _ =>
    match type of o with
    | option ?A =>
      let Hx := fresh in
      first
        [ let x := fresh in evar (x:A);
          let x' := eval unfold x in x in clear x;
          assert (o = Some x') as Hx by tac
        | assert (o = None) as Hx by tac ];
      rewrite Hx in H; clear Hx
    end
238
  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
239
240
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
241
    destruct o eqn:?
Robbert Krebbers's avatar
Robbert Krebbers committed
242
243
244
245
246
247
248
249
250
251
252
253
254
  | H : ?x = mbind (M:=option) ?f ?o |- _ =>
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
    destruct o eqn:?
  | H : fmap (M:=option) ?f ?o = ?x |- _ =>
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
    destruct o eqn:?
  | H : ?x = fmap (M:=option) ?f ?o |- _ =>
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
    destruct o eqn:?
  | |- context [mbind (M:=option) (A:=?A) ?f ?o] =>
255
    let Hx := fresh in
Robbert Krebbers's avatar
Robbert Krebbers committed
256
257
258
259
260
    first
      [ let x := fresh in evar (x:A);
        let x' := eval unfold x in x in clear x;
        assert (o = Some x') as Hx by tac
      | assert (o = None) as Hx by tac ];
261
    rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
  | |- context [fmap (M:=option) (A:=?A) ?f ?o] =>
    let Hx := fresh in
    first
      [ let x := fresh in evar (x:A);
        let x' := eval unfold x in x in clear x;
        assert (o = Some x') as Hx by tac
      | assert (o = None) as Hx by tac ];
    rewrite Hx; clear Hx
  | |- context [ match ?o with _ => _ end ] =>
    match type of o with
    | option ?A =>
      let Hx := fresh in
      first
        [ let x := fresh in evar (x:A);
          let x' := eval unfold x in x in clear x;
          assert (o = Some x') as Hx by tac
        | assert (o = None) as Hx by tac ];
      rewrite Hx; clear Hx
    end
281
282
  | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
    let X := context C [ if dec then x else None ] in
283
    change X in H; destruct_decide dec
284
285
  | |- context C [@mguard option _ ?P ?dec _ ?x] =>
    let X := context C [ if dec then x else None ] in
286
    change X; destruct_decide dec
Robbert Krebbers's avatar
Robbert Krebbers committed
287
288
289
290
  | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
    assert (y = x) by congruence; clear H2
  | H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
    congruence
291
  | H : mapM _ _ = Some _ |- _ => apply mapM_Some in H
292
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
293
294
295
Tactic Notation "simplify_option_equality" :=
  simplify_option_equality by eauto.

296
297
Hint Extern 800 =>
  progress simplify_option_equality : simplify_option_equality.
298
299

(** * Union, intersection and difference *)
Robbert Krebbers's avatar
Robbert Krebbers committed
300
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
301
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
302
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
303
304
305
306
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
308
Instance option_intersection_with {A} :
    IntersectionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
309
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
310
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
311
312
  | _, _ => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
313
314
Instance option_difference_with {A} :
    DifferenceWith A (option A) := λ f x y,
315
316
317
318
319
  match x, y with
  | Some a, Some b => f a b
  | Some a, None => Some a
  | None, _ => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
320

Robbert Krebbers's avatar
Robbert Krebbers committed
321
322
Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
Robbert Krebbers's avatar
Robbert Krebbers committed
323
324

  Global Instance: LeftId (=) None (union_with f).
325
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
  Global Instance: RightId (=) None (union_with f).
327
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
329
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
330
331
332
333
334

  Global Instance: LeftAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: RightAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
335
  Global Instance: Commutative (=) f  Commutative (=) (intersection_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
336
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
337

338
  Global Instance: RightId (=) None (difference_with f).
339
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
End option_union_intersection_difference.