Commit d47d99dd authored by Robbert Krebbers's avatar Robbert Krebbers

Alternative definition of is_Some.

parent 233aa0fa
...@@ -42,6 +42,10 @@ Proof. congruence. Qed. ...@@ -42,6 +42,10 @@ Proof. congruence. Qed.
Definition is_Some {A} (mx : option A) := x, mx = Some x. Definition is_Some {A} (mx : option A) := x, mx = Some x.
Instance: Params (@is_Some) 1. 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. Lemma mk_is_Some {A} (mx : option A) x : mx = Some x is_Some mx.
Proof. intros; red; subst; eauto. Qed. Proof. intros; red; subst; eauto. Qed.
Hint Resolve mk_is_Some. Hint Resolve mk_is_Some.
...@@ -49,6 +53,11 @@ Lemma is_Some_None {A} : ¬is_Some (@None A). ...@@ -49,6 +53,11 @@ Lemma is_Some_None {A} : ¬is_Some (@None A).
Proof. by destruct 1. Qed. Proof. by destruct 1. Qed.
Hint Resolve is_Some_None. 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). Instance is_Some_pi {A} (mx : option A) : ProofIrrel (is_Some mx).
Proof. Proof.
set (P (mx : option A) := match mx with Some _ => True | _ => False end). set (P (mx : option A) := match mx with Some _ => True | _ => False end).
...@@ -59,6 +68,7 @@ Proof. ...@@ -59,6 +68,7 @@ Proof.
assert ( mx H, f mx (g mx H) = H) as f_g by (by intros ? [??]; subst). 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. intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct mx, p1.
Qed. Qed.
Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) := Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) :=
match mx with match mx with
| Some x => left (ex_intro _ x eq_refl) | Some x => left (ex_intro _ x eq_refl)
...@@ -67,17 +77,13 @@ Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) := ...@@ -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 := 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. 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 } := Definition Some_dec {A} (mx : option A) : { x | mx = Some x } + { mx = None } :=
match mx return { x | mx = Some x } + { mx = None } with match mx return { x | mx = Some x } + { mx = None } with
| Some x => inleft (x eq_refl _) | Some x => inleft (x eq_refl _)
| None => inright eq_refl | None => inright eq_refl
end. 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 *) (** Lifting a relation point-wise to option *)
Inductive option_Forall2 {A B} (R: A B Prop) : option A option B Prop := 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) | Some_Forall2 x y : R x y option_Forall2 R (Some x) (Some y)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment