option.v 6.03 KB
 Robbert Krebbers committed Jun 11, 2012 1 2 3 4 5 6 7 8 ``````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. `````` Robbert Krebbers committed Aug 21, 2012 9 ``````Instance Some_inj {A} : Injective (=) (=) (@Some A). `````` Robbert Krebbers committed Jun 11, 2012 10 11 12 13 14 15 16 17 ``````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. `````` Robbert Krebbers committed Aug 21, 2012 18 19 20 21 22 23 ``````Definition maybe {A} (a : A) (x : option A) := match x with | None => a | Some a => a end. `````` Robbert Krebbers committed Jun 11, 2012 24 25 26 27 ``````Lemma option_eq {A} (x y : option A) : x = y ↔ ∀ a, x = Some a ↔ y = Some a. Proof. split. `````` Robbert Krebbers committed Aug 21, 2012 28 29 30 31 32 33 `````` * intros. now subst. * intros E. destruct x, y. + now apply E. + symmetry. now apply E. + now apply E. + easy. `````` Robbert Krebbers committed Jun 11, 2012 34 35 36 37 38 ``````Qed. Definition is_Some `(x : option A) := ∃ a, x = Some a. Hint Extern 10 (is_Some _) => solve [eexists; eauto]. `````` Robbert Krebbers committed Aug 21, 2012 39 ``````Ltac simplify_is_Some := repeat intro; repeat `````` Robbert Krebbers committed Jun 11, 2012 40 `````` match goal with `````` Robbert Krebbers committed Aug 21, 2012 41 `````` | _ => progress simplify_eqs `````` Robbert Krebbers committed Jun 11, 2012 42 43 `````` | H : is_Some _ |- _ => destruct H as [??] | |- is_Some _ => eauto `````` Robbert Krebbers committed Aug 21, 2012 44 `````` end. `````` Robbert Krebbers committed Jun 11, 2012 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 `````` 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 => λ _, a↾eq_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. `````` Robbert Krebbers committed Aug 21, 2012 66 67 ``````Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)} (x y : option A) : Decision (x = y) := `````` Robbert Krebbers committed Jun 11, 2012 68 69 70 71 72 73 `````` match x with | Some a => match y with | Some b => match dec a b with | left H => left (f_equal _ H) `````` Robbert Krebbers committed Aug 21, 2012 74 `````` | right H => right (H ∘ injective Some _ _) `````` Robbert Krebbers committed Jun 11, 2012 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 `````` 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. `````` Robbert Krebbers committed Aug 21, 2012 98 99 ``````Definition option_lift_sig `(P : A → Prop) (x : option A) : option_lift P x → option (sig P) := `````` Robbert Krebbers committed Jun 11, 2012 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 `````` 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 (y↾py) ↔ x = Some y. Proof. split. `````` Robbert Krebbers committed Aug 21, 2012 116 117 `````` * destruct x; simpl; intros; now simplify_eqs. * intros. subst. simpl. f_equal. now apply dsig_eq. `````` Robbert Krebbers committed Jun 11, 2012 118 119 120 121 122 123 ``````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. `````` Robbert Krebbers committed Aug 21, 2012 124 125 `````` * intros [[??] ?]. eapply is_Some_2, option_lift_dsig_Some; eauto. * intros [??]. subst. eapply is_Some_2. reflexivity. `````` Robbert Krebbers committed Jun 11, 2012 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 ``````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. `````` Robbert Krebbers committed Jun 14, 2012 141 142 143 144 145 146 147 148 149 150 151 152 ``````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 committed Aug 21, 2012 153 154 ``````Lemma option_fmap_is_Some {A B} (f : A → B) (x : option A) : is_Some x ↔ is_Some (f <\$> x). `````` Robbert Krebbers committed Jun 11, 2012 155 ``````Proof. destruct x; split; intros [??]; subst; compute; eauto; discriminate. Qed. `````` Robbert Krebbers committed Aug 21, 2012 156 157 ``````Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) : x = None ↔ f <\$> x = None. `````` Robbert Krebbers committed Jun 11, 2012 158 159 160 161 162 163 164 165 166 ``````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. `````` Robbert Krebbers committed Aug 21, 2012 167 ``````Instance option_intersection: IntersectionWith option := λ A f x y, `````` Robbert Krebbers committed Jun 11, 2012 168 169 170 171 `````` match x, y with | Some a, Some b => Some (f a b) | _, _ => None end. `````` Robbert Krebbers committed Aug 21, 2012 172 173 174 175 176 177 ``````Instance option_difference: DifferenceWith option := λ A f x y, match x, y with | Some a, Some b => f a b | Some a, None => Some a | None, _ => None end. `````` Robbert Krebbers committed Jun 11, 2012 178 `````` `````` Robbert Krebbers committed Aug 21, 2012 179 ``````Section option_union_intersection. `````` Robbert Krebbers committed Jun 11, 2012 180 181 182 183 184 185 186 187 188 189 190 191 `````` 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. `````` Robbert Krebbers committed Aug 21, 2012 192 193 194 195 196 197 198 199 ``````End option_union_intersection. Section option_difference. Context {A} (f : A → A → option A). Global Instance: RightId (=) None (difference_with f). Proof. now intros [?|]. Qed. End option_difference.``````