option.v 13.4 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, 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
9
10
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.

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

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

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. *)
Definition from_option {A} (a : A) (x : option A) : A :=
29
  match x with None => a | Some b => b end.
30

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

40
41
42
43
44
45
46
Definition is_Some {A} (x : option A) :=  y, x = Some y.
Lemma mk_is_Some {A} (x : option A) y : x = Some y  is_Some x.
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
47

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

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

72
73
Lemma eq_None_not_Some {A} (x : option A) : x = None  ¬is_Some x.
Proof. destruct x; unfold is_Some; naive_solver. Qed.
74
Lemma not_eq_None_Some `(x : option A) : x  None  is_Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
76

77
(** Equality on [option] is decidable. *)
78
79
80
81
Instance option_eq_None_dec {A} (x : option A) : Decision (x = None) :=
  match x with Some _ => right (Some_ne_None _) | None => left eq_refl end.
Instance option_None_eq_dec {A} (x : option A) : Decision (None = x) :=
  match x with Some _ => right (None_ne_Some _) | None => left eq_refl end.
82
Instance option_eq_dec `{dec :  x y : A, Decision (x = y)}
83
84
85
  (x y : option A) : Decision (x = y).
Proof.
 refine
86
  match x, y with
87
88
  | Some a, Some b => cast_if (decide (a = b))
  | None, None => left _ | _, _ => right _
Robbert Krebbers's avatar
Robbert Krebbers committed
89
  end; clear dec; abstract congruence.
90
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
91

92
(** * Monadic operations *)
93
94
Instance option_ret: MRet option := @Some.
Instance option_bind: MBind option := λ A B f x,
95
  match x with Some a => f a | None => None end.
96
Instance option_join: MJoin option := λ A x,
97
  match x with Some x => x | None => None end.
98
99
Instance option_fmap: FMap option := @option_map.
Instance option_guard: MGuard option := λ P dec A x,
100
  match dec with left H => x H | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
101

102
103
104
Lemma fmap_is_Some {A B} (f : A  B) x : is_Some (f <$> x)  is_Some x.
Proof. unfold is_Some; destruct x; naive_solver. Qed.
Lemma fmap_Some {A B} (f : A  B) x y :
105
  f <$> x = Some y   x', x = Some x'  y = f x'.
106
107
108
Proof. destruct x; naive_solver. Qed.
Lemma fmap_None {A B} (f : A  B) x : f <$> x = None  x = None.
Proof. by destruct x. Qed.
109
Lemma option_fmap_id {A} (x : option A) : id <$> x = x.
110
Proof. by destruct x. Qed.
111
112
113
Lemma option_fmap_compose {A B} (f : A  B) {C} (g : B  C) x :
  g  f <$> x = g <$> f <$> x.
Proof. by destruct x. Qed.
114
115
116
Lemma option_fmap_bind {A B C} (f : A  B) (g : B  option C) x :
  (f <$> x) = g = x = g  f.
Proof. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Lemma option_bind_assoc {A B C} (f : A  option B)
118
  (g : B  option C) (x : option A) : (x = f) = g = x = (mbind g  f).
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Proof. by destruct x; simpl. Qed.
120
Lemma option_bind_ext {A B} (f g : A  option B) x y :
121
  ( a, f a = g a)  x = y  x = f = y = g.
122
Proof. intros. destruct x, y; simplify_equality; csimpl; auto. Qed.
123
Lemma option_bind_ext_fun {A B} (f g : A  option B) x :
124
  ( a, f a = g a)  x = f = x = g.
125
Proof. intros. by apply option_bind_ext. Qed.
126
127
128
129
130
131
Lemma bind_Some {A B} (f : A  option B) (x : option A) b :
  x = f = Some b   a, x = Some a  f a = Some b.
Proof. split. by destruct x as [a|]; [exists a|]. by intros (?&->&?). Qed.
Lemma bind_None {A B} (f : A  option B) (x : option A) :
  x = f = None  x = None   a, x = Some a  f a = None.
Proof.
132
133
  split; [|by intros [->|(?&->&?)]].
  destruct x; intros; simplify_equality'; eauto.
134
Qed.
135
136
Lemma bind_with_Some {A} (x : option A) : x = Some = x.
Proof. by destruct x. Qed.
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
(** ** 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
Instance maybe_Some {A} : Maybe (@Some A) := id.
Arguments maybe_Some _ !_ /.
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
(** * Union, intersection and difference *)
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
  match x, y with
  | Some a, Some b => f a b
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
Instance option_intersection_with {A} : IntersectionWith A (option A) :=
  λ f x y, match x, y with Some a, Some b => f a b | _, _ => None end.
Instance option_difference_with {A} : DifferenceWith A (option A) := λ f x y,
  match x, y with
  | Some a, Some b => f a b
  | Some a, None => Some a
  | None, _ => None
  end.
Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
Lemma option_union_Some {A} (x y : option A) z :
  x  y = Some z  x = Some z  y = Some z.
Proof. destruct x, y; intros; simplify_equality; auto. Qed.

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.
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
  Global Instance: LeftAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: RightAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: Commutative (=) f  Commutative (=) (intersection_with f).
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
  Global Instance: RightId (=) None (difference_with f).
  Proof. by intros [?|]. Qed.
End option_union_intersection_difference.

(** * Tactics *)
205
206
Tactic Notation "case_option_guard" "as" ident(Hx) :=
  match goal with
207
208
209
210
211
212
213
214
  | H : appcontext C [@mguard option _ ?P ?dec] |- _ =>
    change (@mguard option _ P dec) with (λ A (x : P  option A),
      match @decide P dec with left H' => x H' | _ => None end) in *;
    destruct_decide (@decide P dec) as Hx
  | |- appcontext C [@mguard option _ ?P ?dec] =>
    change (@mguard option _ P dec) with (λ A (x : P  option A),
      match @decide P dec with left H' => x H' | _ => None end) in *;
    destruct_decide (@decide P dec) as Hx
215
216
217
  end.
Tactic Notation "case_option_guard" :=
  let H := fresh in case_option_guard as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
218

Robbert Krebbers's avatar
Robbert Krebbers committed
219
Lemma option_guard_True {A} P `{Decision P} (x : option A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
220
221
  P  guard P; x = x.
Proof. intros. by case_option_guard. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
Lemma option_guard_False {A} P `{Decision P} (x : option A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
223
224
  ¬P  guard P; x = None.
Proof. intros. by case_option_guard. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
226
227
Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (x : option A) :
  (P  Q)  guard P; x = guard Q; x.
Proof. intros [??]. repeat case_option_guard; intuition. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
228

Robbert Krebbers's avatar
Robbert Krebbers committed
229
Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
230
231
232
233
234
  let assert_Some_None A o H := first
    [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x;
      assert (o = Some x') as H by tac
    | assert (o = None) as H by tac ]
  in repeat match goal with
235
236
237
  | H : appcontext [@mret _ _ ?A] |- _ =>
     change (@mret _ _ A) with (@Some A) in H
  | |- appcontext [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
Robbert Krebbers's avatar
Robbert Krebbers committed
238
  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
239
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
240
  | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ =>
241
242
243
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
  | H : context [default (A:=?A) _ ?o _] |- _ =>
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
244
245
  | H : context [from_option (A:=?A) _ ?o] |- _ =>
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
246
247
248
  | H : context [ match ?o with _ => _ end ] |- _ =>
    match type of o with
    | option ?A =>
249
      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
250
251
    end
  | |- context [mbind (M:=option) (A:=?A) ?f ?o] =>
252
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
253
  | |- context [fmap (M:=option) (A:=?A) ?f ?o] =>
254
255
256
257
258
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
  | |- context [default (A:=?A) _ ?o _] =>
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
  | |- context [from_option (A:=?A) _ ?o] =>
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
259
260
261
  | |- context [ match ?o with _ => _ end ] =>
    match type of o with
    | option ?A =>
262
      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
263
    end
264
265
266
267
  | _ => rewrite decide_True by tac
  | _ => rewrite decide_False by tac
  | _ => rewrite option_guard_True by tac
  | _ => rewrite option_guard_False by tac
Robbert Krebbers's avatar
Robbert Krebbers committed
268
269
  end.
Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
270
  repeat match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
271
272
  | _ => progress simplify_equality'
  | _ => progress simpl_option_monad by tac
273
274
275
276
  | _ : 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
277
  | H : _  _ = Some _ |- _ => apply option_union_Some in H; destruct H
278
  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
279
280
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
281
282
283
    let y := fresh in destruct o as [y|] eqn:?;
      [change (f y = x) in H|change (None = x) in H]
  | H : ?x = mbind (M:=option) ?f ?o |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
284
285
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
286
287
    let y := fresh in destruct o as [y|] eqn:?;
      [change (x = f y) in H|change (x = None) in H]
288
  | H : fmap (M:=option) ?f ?o = ?x |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
289
290
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
291
292
293
    let y := fresh in destruct o as [y|] eqn:?;
      [change (Some (f y) = x) in H|change (None = x) in H]
  | H : ?x = fmap (M:=option) ?f ?o |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
294
295
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
296
297
    let y := fresh in destruct o as [y|] eqn:?;
      [change (x = Some (f y)) in H|change (x = None) in H]
298
  | _ => progress case_decide
299
  | _ => progress case_option_guard
300
  end.
301
Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto.