option.v 11.2 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

(** * 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.

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

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

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

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

125 126 127 128 129 130 131 132
Definition mapM `{!MBind M} `{!MRet M} {A B}
    (f : A  M B) : list A  M (list B) :=
  fix go l :=
  match l with
  | [] => mret []
  | x :: l => y  f x; k  go l; mret (y :: k)
  end.

133 134 135 136 137 138 139 140
Lemma fmap_is_Some {A B} (f : A  B) (x : option A) :
  is_Some (f <$> x)  is_Some x.
Proof. split; inversion 1. by destruct x. done. Qed.
Lemma fmap_Some {A B} (f : A  B) (x : option A) y :
  f <$> x = Some y   x', x = Some x'  y = f x'.
Proof. unfold fmap, option_fmap. destruct x; naive_solver. Qed.
Lemma fmap_None {A B} (f : A  B) (x : option A) :
  f <$> x = None  x = None.
141
Proof. unfold fmap, option_fmap. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
142

143 144 145
Lemma option_fmap_id {A} (x : option A) :
  id <$> x = x.
Proof. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
146 147 148
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.
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 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
Lemma option_bind_ext {A B} (f g : A  option B) x y :
  ( a, f a = g a) 
  x = y 
  x = f = y = g.
Proof. intros. destruct x, y; simplify_equality; simpl; auto. Qed.
Lemma option_bind_ext_fun {A B} (f g : A  option B) x :
  ( a, f a = g a) 
  x = f = x = g.
Proof. intros. by apply option_bind_ext. Qed.

Section mapM.
  Context {A B : Type} (f : A  option B).

  Lemma mapM_ext (g : A  option B) l :
    ( x, f x = g x)  mapM f l = mapM g l.
  Proof. intros Hfg. by induction l; simpl; rewrite ?Hfg, ?IHl. Qed.
  Lemma Forall2_mapM_ext (g : A  option B) l k :
    Forall2 (λ x y, f x = g y) l k  mapM f l = mapM g k.
  Proof.
    induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH.
  Qed.
  Lemma Forall_mapM_ext (g : A  option B) l :
    Forall (λ x, f x = g x) l  mapM f l = mapM g l.
  Proof.
    induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH.
  Qed.

  Lemma mapM_Some_1 l k :
    mapM f l = Some k  Forall2 (λ x y, f x = Some y) l k.
  Proof.
    revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
    * destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
    * destruct (f x) eqn:?; simpl; [|discriminate].
      destruct (mapM f l); intros; simplify_equality. constructor; auto.
  Qed.
  Lemma mapM_Some_2 l k :
    Forall2 (λ x y, f x = Some y) l k  mapM f l = Some k.
  Proof.
    induction 1 as [|???? Hf ? IH]; simpl; [done |].
    rewrite Hf. simpl. by rewrite IH.
  Qed.
  Lemma mapM_Some l k :
    mapM f l = Some k  Forall2 (λ x y, f x = Some y) l k.
  Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed.
End mapM.
Robbert Krebbers's avatar
Robbert Krebbers committed
194

195
Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
196
  match goal with
197
  | _ => first [progress simpl in * | progress simplify_equality]
Robbert Krebbers's avatar
Robbert Krebbers committed
198
  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
199
    let Hx := fresh in
Robbert Krebbers's avatar
Robbert Krebbers committed
200 201 202 203 204
    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 ];
205
    rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224
  | 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
225
  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
226 227
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
228
    destruct o eqn:?
Robbert Krebbers's avatar
Robbert Krebbers committed
229 230 231 232 233 234 235 236 237 238 239 240 241
  | 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] =>
242
    let Hx := fresh in
Robbert Krebbers's avatar
Robbert Krebbers committed
243 244 245 246 247
    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 ];
248
    rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267
  | |- 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
268 269
  | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
    let X := context C [ if dec then x else None ] in
270
    change X in H; destruct_decide dec
271 272
  | |- context C [@mguard option _ ?P ?dec _ ?x] =>
    let X := context C [ if dec then x else None ] in
273
    change X; destruct_decide dec
Robbert Krebbers's avatar
Robbert Krebbers committed
274 275 276 277
  | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
    assert (y = x) by congruence; clear H2
  | H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
    congruence
278
  | H : mapM _ _ = Some _ |- _ => apply mapM_Some in H
279
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
280 281 282
Tactic Notation "simplify_option_equality" :=
  simplify_option_equality by eauto.

283 284
Hint Extern 800 =>
  progress simplify_option_equality : simplify_option_equality.
285 286

(** * Union, intersection and difference *)
Robbert Krebbers's avatar
Robbert Krebbers committed
287
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
288
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
289
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
290 291 292 293
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
294 295
Instance option_intersection_with {A} :
    IntersectionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
296
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
297
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
298 299
  | _, _ => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
300 301
Instance option_difference_with {A} :
    DifferenceWith A (option A) := λ f x y,
302 303 304 305 306
  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
307

Robbert Krebbers's avatar
Robbert Krebbers committed
308 309
Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
Robbert Krebbers's avatar
Robbert Krebbers committed
310 311

  Global Instance: LeftId (=) None (union_with f).
312
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
313
  Global Instance: RightId (=) None (union_with f).
314
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
315
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
316
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
317 318 319 320 321

  Global Instance: LeftAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: RightAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
322
  Global Instance: Commutative (=) f  Commutative (=) (intersection_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
323
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
324

325
  Global Instance: RightId (=) None (difference_with f).
326
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
327
End option_union_intersection_difference.