option.v 5.54 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131
Require Export base decidable orders.

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.
Lemma Some_inj {A} (a b : A) : Some a = Some b  a = b.
Proof. congruence. Qed.

Definition option_case {A B} (f : A  B) (b : B) (x : option A) :=
  match x with
  | None => b
  | Some a => f a
  end.

Lemma option_eq {A} (x y : option A) :
  x = y   a, x = Some a  y = Some a.
Proof.
  split.
   intros. now subst.
  intros E. destruct x, y.
     now apply E.
    symmetry. now apply E.
   now apply E.
  easy.
Qed.

Definition is_Some `(x : option A) :=  a, x = Some a.
Hint Extern 10 (is_Some _) => solve [eexists; eauto].

Ltac simplify_is_Some := repeat intro; repeat (
  match goal with
  | H : is_Some _ |- _ => destruct H as [??]
  | |- is_Some _ => eauto
  end || simplify_eqs).

Lemma Some_is_Some `(a : A) : is_Some (Some a).
Proof. simplify_is_Some. Qed.
Lemma None_not_is_Some {A} : ¬is_Some (@None A).
Proof. simplify_is_Some. Qed.

Definition is_Some_1 `(x : option A) : is_Some x  { a | x = Some a } :=
  match x with
  | None => False_rect _  ex_ind None_ne_Some
  | Some a => λ _, aeq_refl
  end.
Lemma is_Some_2 `(x : option A) a : x = Some a  is_Some x.
Proof. simplify_is_Some. Qed.

Lemma eq_None_not_Some `(x : option A) : x = None  ¬is_Some x.
Proof. destruct x; simpl; firstorder congruence. Qed.

Lemma make_eq_Some {A} (x : option A) a : 
  is_Some x  ( b, x = Some b  b = a)  x = Some a.
Proof. intros [??] H. subst. f_equal. auto. Qed.

Instance option_eq_dec `{dec :  x y : A, Decision (x = y)} (x y : option A) : Decision (x = y) :=
  match x with
  | Some a =>
    match y with
    | Some b =>
      match dec a b with
      | left H => left (f_equal _ H)
      | right H => right (H  Some_inj _ _)
      end
    | None => right (Some_ne_None _)
    end
  | None =>
    match y with
    | Some _ => right (None_ne_Some _)
    | None => left eq_refl
    end
  end.

Inductive option_lift `(P : A  Prop) : option A  Prop :=
  | option_lift_some x : P x  option_lift P (Some x)
  | option_lift_None : option_lift P None.

Ltac option_lift_inv := repeat
  match goal with
  | H : option_lift _ (Some _) |- _ => inversion H; clear H; subst
  | H : option_lift _ None |- _ => inversion H
  end.

Lemma option_lift_inv_Some `(P : A  Prop) x : option_lift P (Some x)  P x.
Proof. intros. now option_lift_inv. Qed.

Definition option_lift_sig `(P : A  Prop) (x : option A) : option_lift P x  option (sig P) :=
  match x with
  | Some a => λ p, Some (exist _ a (option_lift_inv_Some P a p))
  | None => λ _, None
  end.

Definition option_lift_dsig `(P : A  Prop) `{ x : A, Decision (P x)} 
    (x : option A) : option_lift P x  option (dsig P) :=
  match x with
  | Some a => λ p, Some (dexist a (option_lift_inv_Some P a p))
  | None => λ _, None
  end.

Lemma option_lift_dsig_Some `(P : A  Prop) `{ x : A, Decision (P x)} x y px py :
  option_lift_dsig P x px = Some (ypy)  x = Some y.
Proof.
  split.
   destruct x; simpl; intros; now simplify_eqs.
  intros. subst. simpl. f_equal. now apply dsig_eq.
Qed.

Lemma option_lift_dsig_is_Some `(P : A  Prop) `{ x : A, Decision (P x)} x px :
  is_Some (option_lift_dsig P x px)  is_Some x.
Proof.
  split.
   intros [[??] ?]. eapply is_Some_2, option_lift_dsig_Some; eauto.
  intros [??]. subst. eapply is_Some_2. reflexivity.
Qed.

Instance option_ret: MRet option := @Some.
Instance option_bind: MBind option := λ A B f x,
  match x with
  | Some a => f a
  | None => None
  end.
Instance option_join: MJoin option := λ A x,
  match x with
  | Some x => x
  | None => None
  end.
Instance option_fmap: FMap option := @option_map.

132 133 134 135 136 137 138 139 140 141 142 143
Ltac simplify_options := repeat
  match goal with
  | _ => progress simplify_eqs
  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
    change (option_bind _ _ f o = x) in H;
    destruct o; simpl in H; try discriminate
  | H : context [ ?o = _ ] |- mbind (M:=option) ?f ?o = ?x =>
    change (option_bind _ _ f o = x);
    erewrite H by eauto;
    simpl
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
144 145 146 147 148 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
Lemma option_fmap_is_Some {A B} (f : A  B) (x : option A) : is_Some x  is_Some (f <$> x).
Proof. destruct x; split; intros [??]; subst; compute; eauto; discriminate. Qed.
Lemma option_fmap_is_None {A B} (f : A  B) (x : option A) : x = None  f <$> x = None.
Proof. unfold fmap, option_fmap. destruct x; simpl; split; congruence. Qed.

Instance option_union: UnionWith option := λ A f x y,
  match x, y with
  | Some a, Some b => Some (f a b)
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
Instance option_intersect: IntersectWith option := λ A f x y,
  match x, y with
  | Some a, Some b => Some (f a b)
  | _, _ => None
  end.

Section option_union_intersect.
  Context {A} (f : A  A  A).

  Global Instance: LeftId (=) None (union_with f).
  Proof. now intros [?|]. Qed.
  Global Instance: RightId (=) None (union_with f).
  Proof. now intros [?|]. Qed.
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
  Proof. intros ? [?|] [?|]; compute; try reflexivity. now rewrite (commutative f). Qed.
  Global Instance: Associative (=) f  Associative (=) (union_with f).
  Proof. intros ? [?|] [?|] [?|]; compute; try reflexivity. now rewrite (associative f). Qed.
  Global Instance: Idempotent (=) f  Idempotent (=) (union_with f).
  Proof. intros ? [?|]; compute; try reflexivity. now rewrite (idempotent f). Qed.
End option_union_intersect.