option.v 11.1 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. *)
29 30
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
31

32 33 34 35 36 37 38
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
39

40 41
Instance is_Some_pi {A} (x : option A) : ProofIrrel (is_Some x).
Proof.
42 43 44 45 46 47 48
  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.
49
Qed.
50
Instance is_Some_dec {A} (x : option A) : Decision (is_Some x) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
51
  match x with
52 53
  | Some x => left (ex_intro _ x eq_refl)
  | None => right is_Some_None
54
  end.
55 56 57 58

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
59 60 61 62
  match x return { a | x = Some a } + { x = None } with
  | Some a => inleft (a  eq_refl _)
  | None => inright eq_refl
  end.
63 64
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
65

66 67
Lemma eq_None_not_Some {A} (x : option A) : x = None  ¬is_Some x.
Proof. destruct x; unfold is_Some; naive_solver. Qed.
68
Lemma not_eq_None_Some `(x : option A) : x  None  is_Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
70

71 72 73
(** Equality on [option] is decidable. *)
Instance option_eq_dec `{dec :  x y : A, Decision (x = y)}
    (x y : option A) : Decision (x = y) :=
74 75 76 77 78
  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
79
     end
80 81 82
  | Some _, None => right (Some_ne_None _)
  | None, Some _ => right (None_ne_Some _)
  | None, None => left eq_refl
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
  end.

85
(** * Monadic operations *)
86 87
Instance option_ret: MRet option := @Some.
Instance option_bind: MBind option := λ A B f x,
88
  match x with Some a => f a | None => None end.
89
Instance option_join: MJoin option := λ A x,
90
  match x with Some x => x | None => None end.
91 92
Instance option_fmap: FMap option := @option_map.
Instance option_guard: MGuard option := λ P dec A x,
93
  match dec with left H => x H | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
94

95 96 97 98 99 100 101 102
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.

103 104 105
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 :
106
  f <$> x = Some y   x', x = Some x'  y = f x'.
107 108 109
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
110

111
Lemma option_fmap_id {A} (x : option A) : id <$> x = x.
112
Proof. by destruct x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Lemma option_bind_assoc {A B C} (f : A  option B)
114
  (g : B  option C) (x : option A) : (x = f) = g = x = (mbind g  f).
Robbert Krebbers's avatar
Robbert Krebbers committed
115
Proof. by destruct x; simpl. Qed.
116
Lemma option_bind_ext {A B} (f g : A  option B) x y :
117
  ( a, f a = g a)  x = y  x = f = y = g.
118 119
Proof. intros. destruct x, y; simplify_equality; simpl; auto. Qed.
Lemma option_bind_ext_fun {A B} (f g : A  option B) x :
120
  ( a, f a = g a)  x = f = x = g.
121 122 123 124 125
Proof. intros. by apply option_bind_ext. Qed.

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

126
  Lemma mapM_ext (g : A  option B) l : ( x, f x = g x)  mapM f l = mapM g l.
127 128 129
  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.
130
  Proof. induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
131 132
  Lemma Forall_mapM_ext (g : A  option B) l :
    Forall (λ x, f x = g x) l  mapM f l = mapM g l.
133
  Proof. induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
134

135
  Lemma mapM_Some_1 l k : mapM f l = Some k  Forall2 (λ x y, f x = Some y) l k.
136 137 138 139 140 141
  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.
142
  Lemma mapM_Some_2 l k : Forall2 (λ x y, f x = Some y) l k  mapM f l = Some k.
143 144 145 146
  Proof.
    induction 1 as [|???? Hf ? IH]; simpl; [done |].
    rewrite Hf. simpl. by rewrite IH.
  Qed.
147
  Lemma mapM_Some l k : mapM f l = Some k  Forall2 (λ x y, f x = Some y) l k.
148 149
  Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed.
End mapM.
Robbert Krebbers's avatar
Robbert Krebbers committed
150

151
Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
152
  match goal with
153
  | _ => progress (unfold default in *)
154
  | _ => first [progress simpl in * | progress simplify_equality]
Robbert Krebbers's avatar
Robbert Krebbers committed
155
  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
156
    let Hx := fresh in
Robbert Krebbers's avatar
Robbert Krebbers committed
157 158 159 160 161
    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 ];
162
    rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
  | 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
182
  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
183 184
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
185
    destruct o eqn:?
Robbert Krebbers's avatar
Robbert Krebbers committed
186 187 188 189 190 191 192 193 194 195 196 197 198
  | 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] =>
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; 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
  | |- 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
225
  | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
226
    let X := context C [ match dec with left H => x H | _ => None end ] in
227
    change X in H; destruct_decide dec
228
  | |- context C [@mguard option _ ?P ?dec _ ?x] =>
229
    let X := context C [ match dec with left H => x H | _ => None end ] in
230
    change X; destruct_decide dec
Robbert Krebbers's avatar
Robbert Krebbers committed
231 232 233 234
  | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
    assert (y = x) by congruence; clear H2
  | H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
    congruence
235
  | H : mapM _ _ = Some _ |- _ => apply mapM_Some in H
236
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
237 238 239
Tactic Notation "simplify_option_equality" :=
  simplify_option_equality by eauto.

240 241
Hint Extern 800 =>
  progress simplify_option_equality : simplify_option_equality.
242 243

(** * Union, intersection and difference *)
Robbert Krebbers's avatar
Robbert Krebbers committed
244
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
245
  match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
246
  | Some a, Some b => f a b
Robbert Krebbers's avatar
Robbert Krebbers committed
247 248 249 250
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
251 252 253
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,
254 255 256 257 258
  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
259

Robbert Krebbers's avatar
Robbert Krebbers committed
260 261
Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
Robbert Krebbers's avatar
Robbert Krebbers committed
262 263

  Global Instance: LeftId (=) None (union_with f).
264
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
265
  Global Instance: RightId (=) None (union_with f).
266
  Proof. by intros [?|]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
268
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
269 270 271 272 273

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

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