diff --git a/prelude/option.v b/prelude/option.v index dfaf08a43e647d7e7ce6140f062c512438661122..2dee5a724d29f0241a8344a1249df3802f37cdc2 100644 --- a/prelude/option.v +++ b/prelude/option.v @@ -42,6 +42,10 @@ Proof. congruence. Qed. Definition is_Some {A} (mx : option A) := ∃ x, mx = Some x. Instance: Params (@is_Some) 1. +Lemma is_Some_alt {A} (mx : option A) : + is_Some mx ↔ match mx with Some _ => True | None => False end. +Proof. unfold is_Some. destruct mx; naive_solver. Qed. + Lemma mk_is_Some {A} (mx : option A) x : mx = Some x → is_Some mx. Proof. intros; red; subst; eauto. Qed. Hint Resolve mk_is_Some. @@ -49,6 +53,11 @@ Lemma is_Some_None {A} : ¬is_Some (@None A). Proof. by destruct 1. Qed. Hint Resolve is_Some_None. +Lemma eq_None_not_Some {A} (mx : option A) : mx = None ↔ ¬is_Some mx. +Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed. +Lemma not_eq_None_Some {A} (mx : option A) : mx ≠ None ↔ is_Some mx. +Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed. + Instance is_Some_pi {A} (mx : option A) : ProofIrrel (is_Some mx). Proof. set (P (mx : option A) := match mx with Some _ => True | _ => False end). @@ -59,6 +68,7 @@ Proof. assert (∀ mx H, f mx (g mx H) = H) as f_g by (by intros ? [??]; subst). intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct mx, p1. Qed. + Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) := match mx with | Some x => left (ex_intro _ x eq_refl) @@ -67,17 +77,13 @@ Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) := Definition is_Some_proj {A} {mx : option A} : is_Some mx → A := match mx with Some x => λ _, x | None => False_rect _ ∘ is_Some_None end. + Definition Some_dec {A} (mx : option A) : { x | mx = Some x } + { mx = None } := match mx return { x | mx = Some x } + { mx = None } with | Some x => inleft (x ↾ eq_refl _) | None => inright eq_refl end. -Lemma eq_None_not_Some {A} (mx : option A) : mx = None ↔ ¬is_Some mx. -Proof. destruct mx; unfold is_Some; naive_solver. Qed. -Lemma not_eq_None_Some {A} (mx : option A) : mx ≠ None ↔ is_Some mx. -Proof. rewrite eq_None_not_Some; apply dec_stable; tauto. Qed. - (** Lifting a relation point-wise to option *) Inductive option_Forall2 {A B} (R: A → B → Prop) : option A → option B → Prop := | Some_Forall2 x y : R x y → option_Forall2 R (Some x) (Some y)