Commit a7f54bc4 authored by Robbert Krebbers's avatar Robbert Krebbers

Add `fmap_Some_1` and `fmap_Some_2`.

parent 6117c3e4
...@@ -183,6 +183,11 @@ Proof. unfold is_Some; destruct mx; naive_solver. Qed. ...@@ -183,6 +183,11 @@ Proof. unfold is_Some; destruct mx; naive_solver. Qed.
Lemma fmap_Some {A B} (f : A B) mx y : Lemma fmap_Some {A B} (f : A B) mx y :
f <$> mx = Some y x, mx = Some x y = f x. f <$> mx = Some y x, mx = Some x y = f x.
Proof. destruct mx; naive_solver. Qed. Proof. destruct mx; naive_solver. Qed.
Lemma fmap_Some_1 {A B} (f : A B) mx y :
f <$> mx = Some y x, mx = Some x y = f x.
Proof. apply fmap_Some. Qed.
Lemma fmap_Some_2 {A B} (f : A B) mx x : mx = Some x f <$> mx = Some (f x).
Proof. intros. apply fmap_Some; eauto. Qed.
Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (() : relation B)} Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (() : relation B)}
(f : A B) mx y : (f : A B) mx y :
f <$> mx Some y x, mx = Some x y f x. f <$> mx Some y x, mx = Some x y f x.
......
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