option.v 11.5 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 61 62
Instance is_Some_pi {A} (x : option A) : ProofIrrel (is_Some x).
Proof.
  intros [?] p2. by refine
    match p2 in is_Some o return
      match o with
      | Some y => (make_is_Some y =)
      | _ => λ _, False
      end p2
    with
    | make_is_Some y => _
    end.
Qed.

63 64 65 66 67 68 69 70 71 72 73
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
74
  match goal with
75
  | H : is_Some _ |- _ => inversion H; clear H; subst
76
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
77

Robbert Krebbers's avatar
Robbert Krebbers committed
78
Definition is_Some_proj `{x : option A} : is_Some x  A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  match x with
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  | Some a => λ _, a
81 82
  | None => False_rect _  is_Some_None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84 85 86 87
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.
88 89 90 91
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
92
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94 95 96 97
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
98 99

Lemma eq_None_not_Some `(x : option A) : x = None  ¬is_Some x.
100 101
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
102
Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
103

104
Lemma make_eq_Some {A} (x : option A) a :
Robbert Krebbers's avatar
Robbert Krebbers committed
105
  is_Some x  ( b, x = Some b  b = a)  x = Some a.
106
Proof. destruct 1. intros. f_equal. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
107

108 109 110
(** Equality on [option] is decidable. *)
Instance option_eq_dec `{dec :  x y : A, Decision (x = y)}
    (x y : option A) : Decision (x = y) :=
111 112 113 114 115
  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
116
     end
117 118 119
  | Some _, None => right (Some_ne_None _)
  | None, Some _ => right (None_ne_Some _)
  | None, None => left eq_refl
Robbert Krebbers's avatar
Robbert Krebbers committed
120 121
  end.

122
(** * Monadic operations *)
123 124
Instance option_ret: MRet option := @Some.
Instance option_bind: MBind option := λ A B f x,
Robbert Krebbers's avatar
Robbert Krebbers committed
125 126 127 128
  match x with
  | Some a => f a
  | None => None
  end.
129
Instance option_join: MJoin option := λ A x,
Robbert Krebbers's avatar
Robbert Krebbers committed
130 131 132 133
  match x with
  | Some x => x
  | None => None
  end.
134 135 136
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
137

138 139 140 141 142 143 144 145
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.

146 147 148 149 150 151 152 153
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.
154
Proof. unfold fmap, option_fmap. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155

156 157 158
Lemma option_fmap_id {A} (x : option A) :
  id <$> x = x.
Proof. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
159 160 161
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.
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 194 195 196 197 198 199 200 201 202 203 204 205 206
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
207

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

296 297
Hint Extern 800 =>
  progress simplify_option_equality : simplify_option_equality.
298 299

(** * Union, intersection and difference *)
Robbert Krebbers's avatar
Robbert Krebbers committed
300
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
301
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
302
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
303 304 305 306
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
307 308
Instance option_intersection_with {A} :
    IntersectionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
309
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
310
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
311 312
  | _, _ => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
313 314
Instance option_difference_with {A} :
    DifferenceWith A (option A) := λ f x y,
315 316 317 318 319
  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
320

Robbert Krebbers's avatar
Robbert Krebbers committed
321 322
Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
Robbert Krebbers's avatar
Robbert Krebbers committed
323 324

  Global Instance: LeftId (=) None (union_with f).
325
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
  Global Instance: RightId (=) None (union_with f).
327
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
329
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
330 331 332 333 334

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

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