option.v 11.2 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
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
61
  match goal with
62
  | H : is_Some _ |- _ => inversion H; clear H; subst
63
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
64

Robbert Krebbers's avatar
Robbert Krebbers committed
65
Definition is_Some_proj `{x : option A} : is_Some x  A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  match x with
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  | Some a => λ _, a
68
69
  | None => False_rect _  is_Some_None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
72
73
74
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.
75
76
77
78
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
79
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
82
83
84
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
85
86

Lemma eq_None_not_Some `(x : option A) : x = None  ¬is_Some x.
87
88
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
89
Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
90

91
Lemma make_eq_Some {A} (x : option A) a :
Robbert Krebbers's avatar
Robbert Krebbers committed
92
  is_Some x  ( b, x = Some b  b = a)  x = Some a.
93
Proof. destruct 1. intros. f_equal. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
94

95
96
97
(** Equality on [option] is decidable. *)
Instance option_eq_dec `{dec :  x y : A, Decision (x = y)}
    (x y : option A) : Decision (x = y) :=
98
99
100
101
102
  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
103
     end
104
105
106
  | Some _, None => right (Some_ne_None _)
  | None, Some _ => right (None_ne_Some _)
  | None, None => left eq_refl
Robbert Krebbers's avatar
Robbert Krebbers committed
107
108
  end.

109
(** * Monadic operations *)
110
111
Instance option_ret: MRet option := @Some.
Instance option_bind: MBind option := λ A B f x,
Robbert Krebbers's avatar
Robbert Krebbers committed
112
113
114
115
  match x with
  | Some a => f a
  | None => None
  end.
116
Instance option_join: MJoin option := λ A x,
Robbert Krebbers's avatar
Robbert Krebbers committed
117
118
119
120
  match x with
  | Some x => x
  | None => None
  end.
121
122
123
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
124

125
126
127
128
129
130
131
132
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.

133
134
135
136
137
138
139
140
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.
141
Proof. unfold fmap, option_fmap. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
142

143
144
145
Lemma option_fmap_id {A} (x : option A) :
  id <$> x = x.
Proof. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
148
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.
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
186
187
188
189
190
191
192
193
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
194

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

283
284
Hint Extern 800 =>
  progress simplify_option_equality : simplify_option_equality.
285
286

(** * Union, intersection and difference *)
Robbert Krebbers's avatar
Robbert Krebbers committed
287
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
288
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
289
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
290
291
292
293
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
294
295
Instance option_intersection_with {A} :
    IntersectionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
296
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
297
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
298
299
  | _, _ => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
301
Instance option_difference_with {A} :
    DifferenceWith A (option A) := λ f x y,
302
303
304
305
306
  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
307

Robbert Krebbers's avatar
Robbert Krebbers committed
308
309
Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
Robbert Krebbers's avatar
Robbert Krebbers committed
310
311

  Global Instance: LeftId (=) None (union_with f).
312
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
313
  Global Instance: RightId (=) None (union_with f).
314
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
315
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
316
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
317
318
319
320
321

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

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