option.v 11.2 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2014, 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
Lemma option_guard_True {A} P `{Decision P} (x : option A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
150 151
  P  guard P; x = x.
Proof. intros. by case_option_guard. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Lemma option_guard_False {A} P `{Decision P} (x : option A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
153 154
  ¬P  guard P; x = None.
Proof. intros. by case_option_guard. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157
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
158

Robbert Krebbers's avatar
Robbert Krebbers committed
159
Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
160 161 162 163 164
  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
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
166
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
167
  | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ =>
168 169 170
    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
171 172 173
  | H : context [ match ?o with _ => _ end ] |- _ =>
    match type of o with
    | option ?A =>
174
      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
175 176
    end
  | |- context [mbind (M:=option) (A:=?A) ?f ?o] =>
177
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
178
  | |- context [fmap (M:=option) (A:=?A) ?f ?o] =>
179 180 181 182 183
    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
184 185 186
  | |- context [ match ?o with _ => _ end ] =>
    match type of o with
    | option ?A =>
187
      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
188
    end
189 190 191 192
  | _ => 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
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
  end.
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
  | _ => progress simplify_equality'
  | _ => progress simpl_option_monad by tac
  | H : mbind (M:=option) _ ?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 = mbind (M:=option) _ ?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) _ ?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) _ ?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:?
218
  | _ => progress case_decide
219
  | _ => progress case_option_guard
220
  end.
221
Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto.
222 223

(** * Union, intersection and difference *)
Robbert Krebbers's avatar
Robbert Krebbers committed
224
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
226
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
227 228 229 230
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
231 232 233
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,
234 235 236 237 238
  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
239

Robbert Krebbers's avatar
Robbert Krebbers committed
240 241
Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
Robbert Krebbers's avatar
Robbert Krebbers committed
242
  Global Instance: LeftId (=) None (union_with f).
243
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
  Global Instance: RightId (=) None (union_with f).
245
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
247
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
248 249 250 251
  Global Instance: LeftAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: RightAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
252
  Global Instance: Commutative (=) f  Commutative (=) (intersection_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
253
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
254
  Global Instance: RightId (=) None (difference_with f).
255
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
End option_union_intersection_difference.