Extensionality of omap.

051644fb · Robbert Krebbers · e23aa096 · 051644fb
Commit 051644fb authored Feb 13, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 6 additions and 0 deletions

prelude/fin_maps.v prelude/fin_maps.v +6 -0

No files found.
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -558,6 +558,12 @@ Proof.
  intros Hi; apply map_eq; intros i; rewrite !lookup_fmap.
  by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
 Qed.
+Lemma omap_ext {A B} (f1 f2 : A → option B) m :
+  (∀ i x, m !! i = Some x → f1 x = f2 x) → omap f1 m = omap f2 m.
+Proof.
+  intros Hi; apply map_eq; intros i; rewrite !lookup_omap.
+  by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
+Qed.

 (** ** Properties of conversion to lists *)
 Lemma map_to_list_unique {A} (m : M A) i x y :