option.v 10.7 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 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.
25
Hint Extern 1000 => simpl (default _ (Some _) _) || simpl (default _ None _).
Robbert Krebbers's avatar
Robbert Krebbers committed
26

Robbert Krebbers's avatar
Robbert Krebbers committed
27 28 29
(** 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 :=
30
  match x with None => a | Some b => b end.
31

32 33
(** An alternative, but equivalent, definition of equality on the option
data type. This theorem is useful to prove that two options are the same. *)
34 35
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
36

37 38 39 40 41 42 43
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
44

45 46
Instance is_Some_pi {A} (x : option A) : ProofIrrel (is_Some x).
Proof.
47 48 49 50 51 52 53
  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.
54
Qed.
55
Instance is_Some_dec {A} (x : option A) : Decision (is_Some x) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  match x with
57 58
  | Some x => left (ex_intro _ x eq_refl)
  | None => right is_Some_None
59
  end.
60 61 62 63

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
64 65 66 67
  match x return { a | x = Some a } + { x = None } with
  | Some a => inleft (a  eq_refl _)
  | None => inright eq_refl
  end.
68 69
Instance None_dec {A} (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
70

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

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

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

101 102 103
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 :
104
  f <$> x = Some y   x', x = Some x'  y = f x'.
105 106 107
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.
108
Lemma option_fmap_id {A} (x : option A) : id <$> x = x.
109
Proof. by destruct x. Qed.
110 111 112
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.
113 114 115
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
116
Lemma option_bind_assoc {A B C} (f : A  option B)
117
  (g : B  option C) (x : option A) : (x = f) = g = x = (mbind g  f).
Robbert Krebbers's avatar
Robbert Krebbers committed
118
Proof. by destruct x; simpl. Qed.
119
Lemma option_bind_ext {A B} (f g : A  option B) x y :
120
  ( a, f a = g a)  x = y  x = f = y = g.
121 122
Proof. intros. destruct x, y; simplify_equality; simpl; auto. Qed.
Lemma option_bind_ext_fun {A B} (f g : A  option B) x :
123
  ( a, f a = g a)  x = f = x = g.
124
Proof. intros. by apply option_bind_ext. Qed.
125 126 127 128 129 130
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.
131 132
  split; [|by intros [->|(?&->&?)]].
  destruct x; intros; simplify_equality'; eauto.
133
Qed.
134 135
Lemma bind_with_Some {A} (x : option A) : x = Some = x.
Proof. by destruct x. Qed.
136

137 138 139 140 141 142 143 144 145 146 147
Tactic Notation "case_option_guard" "as" ident(Hx) :=
  match goal with
  | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
    let X := context C [ match dec with left H => x H | _ => None end ] in
    change X in H; destruct_decide dec as Hx
  | |- context C [@mguard option _ ?P ?dec _ ?x] =>
    let X := context C [ match dec with left H => x H | _ => None end ] in
    change X; destruct_decide dec as Hx
  end.
Tactic Notation "case_option_guard" :=
  let H := fresh in case_option_guard as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
148

Robbert Krebbers's avatar
Robbert Krebbers committed
149 150 151 152 153 154 155
Lemma option_guard_True {A} (P : Prop) `{Decision P} (x : option A) :
  P  guard P; x = x.
Proof. intros. by case_option_guard. Qed.
Lemma option_guard_False {A} (P : Prop) `{Decision P} (x : option A) :
  ¬P  guard P; x = None.
Proof. intros. by case_option_guard. Qed.

156 157 158 159 160 161
Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
  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
162
  | _ => progress simplify_equality'
Robbert Krebbers's avatar
Robbert Krebbers committed
163
  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
164
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ =>
166 167 168
    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
Robbert Krebbers's avatar
Robbert Krebbers committed
169 170 171
  | H : context [ match ?o with _ => _ end ] |- _ =>
    match type of o with
    | option ?A =>
172
      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
173
    end
174
  | H : mbind (M:=option) _ ?o = ?x |- _ =>
175 176
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
177
    destruct o eqn:?
178
  | H : ?x = mbind (M:=option) _ ?o |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
179 180 181
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
    destruct o eqn:?
182
  | H : fmap (M:=option) _ ?o = ?x |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
183 184 185
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
    destruct o eqn:?
186
  | H : ?x = fmap (M:=option) _ ?o |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
187 188 189 190
    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] =>
191
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
192
  | |- context [fmap (M:=option) (A:=?A) ?f ?o] =>
193 194 195 196 197
    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
198 199 200
  | |- context [ match ?o with _ => _ end ] =>
    match type of o with
    | option ?A =>
201
      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
202
    end
203 204 205 206 207
  | _ => rewrite decide_True by tac
  | _ => rewrite decide_False by tac
  | _ => rewrite option_guard_True by tac
  | _ => rewrite option_guard_False by tac
  | _ => progress case_decide
208
  | _ => progress case_option_guard
209
  end.
210
Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto.
211 212

(** * Union, intersection and difference *)
Robbert Krebbers's avatar
Robbert Krebbers committed
213
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
214
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
215
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
216 217 218 219
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
220 221 222
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,
223 224 225 226 227
  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
228

Robbert Krebbers's avatar
Robbert Krebbers committed
229 230
Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
Robbert Krebbers's avatar
Robbert Krebbers committed
231
  Global Instance: LeftId (=) None (union_with f).
232
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
  Global Instance: RightId (=) None (union_with f).
234
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
236
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
237 238 239 240
  Global Instance: LeftAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: RightAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
241
  Global Instance: Commutative (=) f  Commutative (=) (intersection_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
242
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
243
  Global Instance: RightId (=) None (difference_with f).
244
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
245
End option_union_intersection_difference.