option.v 6.54 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 [maybe] function allows us to get the value out of the option type
by specifying a default value. *)
Definition maybe {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
49
(** We define [is_Some] as a [sig] instead of a [sigT] as extraction of
witnesses can be derived (see [is_Some_sigT] below). *)
Definition is_Some `(x : option A) : Prop :=  a, x = Some a.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
51
Hint Extern 10 (is_Some _) => solve [eexists; eauto].

52
Ltac simplify_is_Some := repeat intro; repeat
Robbert Krebbers's avatar
Robbert Krebbers committed
53
  match goal with
54
  | _ => progress simplify_equality
Robbert Krebbers's avatar
Robbert Krebbers committed
55
56
  | H : is_Some _ |- _ => destruct H as [??]
  | |- is_Some _ => eauto
57
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59
60
61
62
63

Lemma Some_is_Some `(a : A) : is_Some (Some a).
Proof. simplify_is_Some. Qed.
Lemma None_not_is_Some {A} : ¬is_Some (@None A).
Proof. simplify_is_Some. Qed.

64
Definition is_Some_sigT `(x : option A) : is_Some x  { a | x = Some a } :=
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
67
68
  match x with
  | None => False_rect _  ex_ind None_ne_Some
  | Some a => λ _, aeq_refl
  end.
69
Lemma eq_Some_is_Some `(x : option A) a : x = Some a  is_Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
72
73
74
Proof. simplify_is_Some. Qed.

Lemma eq_None_not_Some `(x : option A) : x = None  ¬is_Some x.
Proof. destruct x; simpl; firstorder congruence. Qed.

75
Lemma make_eq_Some {A} (x : option A) a :
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
78
  is_Some x  ( b, x = Some b  b = a)  x = Some a.
Proof. intros [??] H. subst. f_equal. auto. Qed.

79
80
81
(** 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
82
83
84
85
86
87
  match x with
  | Some a =>
    match y with
    | Some b =>
      match dec a b with
      | left H => left (f_equal _ H)
88
      | right H => right (H  injective Some _ _)
Robbert Krebbers's avatar
Robbert Krebbers committed
89
90
91
92
93
94
95
96
97
98
      end
    | None => right (Some_ne_None _)
    end
  | None =>
    match y with
    | Some _ => right (None_ne_Some _)
    | None => left eq_refl
    end
  end.

99
(** * Monadic operations *)
100
Instance option_bind {A B} (f : A  option B) : MBind option f := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
101
102
103
104
  match x with
  | Some a => f a
  | None => None
  end.
105
Instance option_join {A} : MJoin option := λ x : option (option A),
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
108
109
  match x with
  | Some x => x
  | None => None
  end.
110
Instance option_fmap {A B} (f : A  B) : FMap option f := option_map f.
Robbert Krebbers's avatar
Robbert Krebbers committed
111

112
113
Lemma option_fmap_is_Some {A B} (f : A  B) (x : option A) :
  is_Some x  is_Some (f <$> x).
114
Proof. destruct x; split; intros [??]; subst; compute; by eauto. Qed.
115
116
Lemma option_fmap_is_None {A B} (f : A  B) (x : option A) :
  x = None  f <$> x = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
118
Proof. unfold fmap, option_fmap. destruct x; simpl; split; congruence. Qed.

119
Tactic Notation "simplify_option_bind" "by" tactic3(tac) := repeat
120
  match goal with
121
122
123
124
125
126
127
  | _ => first [progress simpl in * | progress simplify_equality]
  | H : mbind (M:=option) (A:=?A) ?f ?o = ?x |- _ =>
    let x := fresh in evar (x:A);
    let x' := eval unfold x in x in clear x;
    let Hx := fresh in
    assert (o = Some x') as Hx by tac;
    rewrite Hx in H; clear Hx
128
  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
129
130
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
131
    destruct o eqn:?
132
133
134
135
136
137
  | |- mbind (M:=option) (A:=?A) ?f ?o = ?x =>
    let x := fresh in evar (x:A);
    let x' := eval unfold x in x in clear x;
    let Hx := fresh in
    assert (o = Some x') as Hx by tac;
    rewrite Hx; clear Hx
138
  end.
139
Tactic Notation "simplify_option_bind" := simplify_option_bind by eauto.
140
141

(** * Union, intersection and difference *)
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
145
146
147
148
Instance option_union: UnionWith option := λ A f x y,
  match x, y with
  | Some a, Some b => Some (f a b)
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
149
Instance option_intersection: IntersectionWith option := λ A f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
  match x, y with
  | Some a, Some b => Some (f a b)
  | _, _ => None
  end.
154
155
156
157
158
159
Instance option_difference: DifferenceWith option := λ A f x y,
  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
160

161
Section option_union_intersection.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
164
  Context {A} (f : A  A  A).

  Global Instance: LeftId (=) None (union_with f).
165
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  Global Instance: RightId (=) None (union_with f).
167
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
169
170
  Proof.
    intros ? [?|] [?|]; compute; try reflexivity.
171
    by rewrite (commutative f).
172
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  Global Instance: Associative (=) f  Associative (=) (union_with f).
174
175
  Proof.
    intros ? [?|] [?|] [?|]; compute; try reflexivity.
176
    by rewrite (associative f).
177
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
  Global Instance: Idempotent (=) f  Idempotent (=) (union_with f).
179
180
  Proof.
    intros ? [?|]; compute; try reflexivity.
181
    by rewrite (idempotent f).
182
183
184
185
186
  Qed.

  Global Instance: Commutative (=) f  Commutative (=) (intersection_with f).
  Proof.
    intros ? [?|] [?|]; compute; try reflexivity.
187
    by rewrite (commutative f).
188
189
190
191
  Qed.
  Global Instance: Associative (=) f  Associative (=) (intersection_with f).
  Proof.
    intros ? [?|] [?|] [?|]; compute; try reflexivity.
192
    by rewrite (associative f).
193
194
195
196
  Qed.
  Global Instance: Idempotent (=) f  Idempotent (=) (intersection_with f).
  Proof.
    intros ? [?|]; compute; try reflexivity.
197
    by rewrite (idempotent f).
198
  Qed.
199
200
201
202
203
204
End option_union_intersection.

Section option_difference.
  Context {A} (f : A  A  option A).

  Global Instance: RightId (=) None (difference_with f).
205
  Proof. by intros [?|]. Qed.
206
End option_difference.