option.v 9.3 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
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 136 137
Lemma option_fmap_id {A} (x : option A) :
  id <$> x = x.
Proof. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
138 139 140 141
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.

142
Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
143
  match goal with
144
  | _ => first [progress simpl in * | progress simplify_equality]
Robbert Krebbers's avatar
Robbert Krebbers committed
145
  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
146
    let Hx := fresh in
Robbert Krebbers's avatar
Robbert Krebbers committed
147 148 149 150 151
    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 ];
152
    rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
  | 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
172
  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
173 174
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
175
    destruct o eqn:?
Robbert Krebbers's avatar
Robbert Krebbers committed
176 177 178 179 180 181 182 183 184 185 186 187 188
  | 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] =>
189
    let Hx := fresh in
Robbert Krebbers's avatar
Robbert Krebbers committed
190 191 192 193 194
    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 ];
195
    rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
  | |- 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
215 216
  | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
    let X := context C [ if dec then x else None ] in
217
    change X in H; destruct_decide dec
218 219
  | |- context C [@mguard option _ ?P ?dec _ ?x] =>
    let X := context C [ if dec then x else None ] in
220
    change X; destruct_decide dec
Robbert Krebbers's avatar
Robbert Krebbers committed
221 222 223 224
  | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
    assert (y = x) by congruence; clear H2
  | H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
    congruence
225
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
226 227 228 229
Tactic Notation "simplify_option_equality" :=
  simplify_option_equality by eauto.

Hint Extern 100 => simplify_option_equality : simplify_option_equality.
230 231

(** * Union, intersection and difference *)
Robbert Krebbers's avatar
Robbert Krebbers committed
232
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
233
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
234
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
235 236 237 238
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
239 240
Instance option_intersection_with {A} :
    IntersectionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
241
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
242
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
243 244
  | _, _ => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
245 246
Instance option_difference_with {A} :
    DifferenceWith A (option A) := λ f x y,
247 248 249 250 251
  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
252

Robbert Krebbers's avatar
Robbert Krebbers committed
253 254
Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
Robbert Krebbers's avatar
Robbert Krebbers committed
255 256

  Global Instance: LeftId (=) None (union_with f).
257
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
  Global Instance: RightId (=) None (union_with f).
259
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
260
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
261
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
262 263 264 265 266

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

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