option.v 8.93 KB
Newer Older
1
2
3
4
(* Copyright (c) 2012, 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
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.

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

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

Lemma eq_None_not_Some `(x : option A) : x = None  ¬is_Some x.
87
88
89
Proof. split. by destruct 2. destruct x. by intros []. done. Qed.
Lemma not_eq_None_Some `(x : option A) : x  None  is_Some x.
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) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
98
99
100
101
  match x with
  | Some a =>
    match y with
    | Some b =>
102
103
104
105
       match dec a b with
       | left H => left (f_equal _ H)
       | right H => right (H  injective Some _ _)
       end
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
108
    | None => right (Some_ne_None _)
    end
  | None =>
109
110
111
112
     match y with
     | Some _ => right (None_ne_Some _)
     | None => left eq_refl
     end
Robbert Krebbers's avatar
Robbert Krebbers committed
113
114
  end.

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

131
132
Lemma option_fmap_is_Some {A B} (f : A  B) (x : option A) :
  is_Some x  is_Some (f <$> x).
133
Proof. split; inversion 1. done. by destruct x. Qed.
134
135
Lemma option_fmap_is_None {A B} (f : A  B) (x : option A) :
  x = None  f <$> x = None.
136
137
138
139
140
Proof. unfold fmap, option_fmap. by destruct x. Qed.

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.
Robbert Krebbers's avatar
Robbert Krebbers committed
141

142
Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
143
  match goal with
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
  | _ => first [progress simpl in * | progress simplify_equality]
  | H : context [mbind (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 [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
172
  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
173
174
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
175
    destruct o eqn:?
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
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
  | 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] =>
    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 [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
  | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
    let X := context C [ if dec then x else None ] in
    change X in H; destruct dec
  | |- context C [@mguard option _ ?P ?dec _ ?x] =>
    let X := context C [ if dec then x else None ] in
    change X; destruct dec
  | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
    assert (y = x) by congruence; clear H2
  | H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
    congruence
225
  end.
226
227
228
229
Tactic Notation "simplify_option_equality" :=
  simplify_option_equality by eauto.

Hint Extern 100 => simplify_option_equality : simplify_option_equality.
230
231

(** * Union, intersection and difference *)
232
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
233
  match x, y with
234
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236
237
238
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
239
240
Instance option_intersection_with {A} :
    IntersectionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
241
  match x, y with
242
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
243
244
  | _, _ => None
  end.
245
246
Instance option_difference_with {A} :
    DifferenceWith A (option A) := λ f x y,
247
248
249
250
251
  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
252

253
254
Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
Robbert Krebbers's avatar
Robbert Krebbers committed
255
256

  Global Instance: LeftId (=) None (union_with f).
257
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
  Global Instance: RightId (=) None (union_with f).
259
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
260
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
261
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
262
  Global Instance: Commutative (=) f  Commutative (=) (intersection_with f).
263
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
264
  Global Instance: RightId (=) None (difference_with f).
265
266
  Proof. by intros [?|]. Qed.
End option_union_intersection_difference.