From d496bc8ff5f9968e29cac6e9e0abefe33e84c6db Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 15 Dec 2015 13:34:28 +0100 Subject: [PATCH] Extensionality of map on setoid equality on finite maps. --- theories/fin_maps.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/theories/fin_maps.v b/theories/fin_maps.v index ef37ebd..daaa5c6 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -536,6 +536,12 @@ Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed. Lemma map_fmap_compose {A B C} (f : A → B) (g : B → C) (m : M A) : g ∘ f <\$> m = g <\$> f <\$> m. Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed. +Lemma map_fmap_setoid_ext `{Equiv A, Equiv B} (f1 f2 : A → B) m : + (∀ i x, m !! i = Some x → f1 x ≡ f2 x) → f1 <\$> m ≡ f2 <\$> m. +Proof. + intros Hi i; rewrite !lookup_fmap. + destruct (m !! i) eqn:?; constructor; eauto. +Qed. Lemma map_fmap_ext {A B} (f1 f2 : A → B) m : (∀ i x, m !! i = Some x → f1 x = f2 x) → f1 <\$> m = f2 <\$> m. Proof. -- GitLab