option.v 11.4 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
(** The non dependent elimination principle on the option type. *)
19 20
Definition default {A B} (b : B) (x : option A) (f : A  B)  : B :=
  match x with None => b | Some a => f a end.
Robbert Krebbers's avatar
Robbert Krebbers committed
21

Robbert Krebbers's avatar
Robbert Krebbers committed
22 23 24
(** 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 :=
25
  match x with None => a | Some b => b end.
26

27 28
(** 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
29 30 31
Lemma option_eq {A} (x y : option A) :
  x = y   a, x = Some a  y = Some a.
Proof.
32
  split; [by intros; by subst |]. intros E. destruct x, y.
33 34 35 36
  + by apply E.
  + symmetry. by apply E.
  + by apply E.
  + done.
Robbert Krebbers's avatar
Robbert Krebbers committed
37 38
Qed.

39
Inductive is_Some {A} : option A  Prop :=
40
  mk_is_Some x : is_Some (Some x).
Robbert Krebbers's avatar
Robbert Krebbers committed
41

42 43 44 45
Instance is_Some_pi {A} (x : option A) : ProofIrrel (is_Some x).
Proof.
  intros [?] p2. by refine
    match p2 in is_Some o return
46 47
      match o with Some y => (mk_is_Some y =) | _ => λ _, False end p2
    with mk_is_Some y => _ end.
48 49
Qed.

50
Lemma mk_is_Some_alt `(x : option A) a : x = Some a  is_Some x.
51
Proof. intros. by subst. Qed.
52
Hint Resolve mk_is_Some_alt.
53 54 55 56 57 58 59 60
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
61
  match goal with H : is_Some _ |- _ => inversion H; clear H; subst end.
Robbert Krebbers's avatar
Robbert Krebbers committed
62

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

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

89
Lemma mk_eq_Some {A} (x : option A) a :
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  is_Some x  ( b, x = Some b  b = a)  x = Some a.
91
Proof. destruct 1. intros. f_equal. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
92

93 94 95
(** Equality on [option] is decidable. *)
Instance option_eq_dec `{dec :  x y : A, Decision (x = y)}
    (x y : option A) : Decision (x = y) :=
96 97 98 99 100
  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
101
     end
102 103 104
  | Some _, None => right (Some_ne_None _)
  | None, Some _ => right (None_ne_Some _)
  | None, None => left eq_refl
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106
  end.

107
(** * Monadic operations *)
108 109
Instance option_ret: MRet option := @Some.
Instance option_bind: MBind option := λ A B f x,
110
  match x with Some a => f a | None => None end.
111
Instance option_join: MJoin option := λ A x,
112
  match x with Some x => x | None => None end.
113 114
Instance option_fmap: FMap option := @option_map.
Instance option_guard: MGuard option := λ P dec A x,
115
  match dec with left H => x H | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
116

117 118 119 120 121 122 123 124
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.

125 126 127 128 129 130 131 132
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.
133
Proof. unfold fmap, option_fmap. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
134

135
Lemma option_fmap_id {A} (x : option A) : id <$> x = x.
136
Proof. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138 139
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.
140
Lemma option_bind_ext {A B} (f g : A  option B) x y :
141
  ( a, f a = g a)  x = y  x = f = y = g.
142 143
Proof. intros. destruct x, y; simplify_equality; simpl; auto. Qed.
Lemma option_bind_ext_fun {A B} (f g : A  option B) x :
144
  ( a, f a = g a)  x = f = x = g.
145 146 147 148 149
Proof. intros. by apply option_bind_ext. Qed.

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

150
  Lemma mapM_ext (g : A  option B) l : ( x, f x = g x)  mapM f l = mapM g l.
151 152 153
  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.
154
  Proof. induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
155 156
  Lemma Forall_mapM_ext (g : A  option B) l :
    Forall (λ x, f x = g x) l  mapM f l = mapM g l.
157
  Proof. induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
158

159
  Lemma mapM_Some_1 l k : mapM f l = Some k  Forall2 (λ x y, f x = Some y) l k.
160 161 162 163 164 165
  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.
166
  Lemma mapM_Some_2 l k : Forall2 (λ x y, f x = Some y) l k  mapM f l = Some k.
167 168 169 170
  Proof.
    induction 1 as [|???? Hf ? IH]; simpl; [done |].
    rewrite Hf. simpl. by rewrite IH.
  Qed.
171
  Lemma mapM_Some l k : mapM f l = Some k  Forall2 (λ x y, f x = Some y) l k.
172 173
  Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed.
End mapM.
Robbert Krebbers's avatar
Robbert Krebbers committed
174

175
Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
176
  match goal with
177
  | _ => progress (unfold default in *)
178
  | _ => first [progress simpl in * | progress simplify_equality]
Robbert Krebbers's avatar
Robbert Krebbers committed
179
  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
180
    let Hx := fresh in
Robbert Krebbers's avatar
Robbert Krebbers committed
181 182 183 184 185
    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 ];
186
    rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
  | 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
206
  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
207 208
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
209
    destruct o eqn:?
Robbert Krebbers's avatar
Robbert Krebbers committed
210 211 212 213 214 215 216 217 218 219 220 221 222
  | 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] =>
223
    let Hx := fresh in
Robbert Krebbers's avatar
Robbert Krebbers committed
224 225 226 227 228
    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 ];
229
    rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248
  | |- 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
249
  | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
250
    let X := context C [ match dec with left H => x H | _ => None end ] in
251
    change X in H; destruct_decide dec
252
  | |- context C [@mguard option _ ?P ?dec _ ?x] =>
253
    let X := context C [ match dec with left H => x H | _ => None end ] in
254
    change X; destruct_decide dec
Robbert Krebbers's avatar
Robbert Krebbers committed
255 256 257 258
  | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
    assert (y = x) by congruence; clear H2
  | H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
    congruence
259
  | H : mapM _ _ = Some _ |- _ => apply mapM_Some in H
260
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
261 262 263
Tactic Notation "simplify_option_equality" :=
  simplify_option_equality by eauto.

264 265
Hint Extern 800 =>
  progress simplify_option_equality : simplify_option_equality.
266 267

(** * Union, intersection and difference *)
Robbert Krebbers's avatar
Robbert Krebbers committed
268
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
269
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
270
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
271 272 273 274
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
275 276 277
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,
278 279 280 281 282
  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
283

Robbert Krebbers's avatar
Robbert Krebbers committed
284 285
Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
Robbert Krebbers's avatar
Robbert Krebbers committed
286 287

  Global Instance: LeftId (=) None (union_with f).
288
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
289
  Global Instance: RightId (=) None (union_with f).
290
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
292
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
293 294 295 296 297

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

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