From d101c5621d94883e2b5d2872f32d339a69117f2b Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sun, 20 Sep 2015 14:11:48 +0200 Subject: [PATCH] Indexed map function for finite maps. --- theories/fin_maps.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/theories/fin_maps.v b/theories/fin_maps.v index 4a47d24..5a3b8df 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -104,6 +104,12 @@ index contains a value in the second map as well. *) Instance map_difference `{Merge M} {A} : Difference (M A) := difference_with (λ _ _, None). +(** A stronger variant of map that allows the mapped function to use the index +of the elements. Implemented by conversion to lists, so not very efficient. *) +Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A), + ∀ A, FinMapToList K A (M A)} {A B} (f : K → A → option B) (m : M A) : M B := + map_of_list (omap (λ ix, (fst ix,) <\$> curry f ix) (map_to_list m)). + (** * Theorems *) Section theorems. Context `{FinMap K M}. @@ -585,6 +591,23 @@ Proof. exists i x. rewrite <-elem_of_map_to_list, Hm. by left. Qed. +(** Properties of the imap function *) +Lemma lookup_imap {A B} (f : K → A → option B) m i : + map_imap f m !! i = m !! i ≫= f i. +Proof. + unfold map_imap; destruct (m !! i ≫= f i) as [y|] eqn:Hi; simpl. + * destruct (m !! i) as [x|] eqn:?; simplify_equality'. + apply elem_of_map_of_list_1_help. + { apply elem_of_list_omap; exists (i,x); split; + [by apply elem_of_map_to_list|by simplify_option_equality]. } + intros y'; rewrite elem_of_list_omap; intros ([i' x']&Hi'&?). + by rewrite elem_of_map_to_list in Hi'; simplify_option_equality. + * apply not_elem_of_map_of_list; rewrite elem_of_list_fmap. + intros ([i' x]&->&Hi'); simplify_equality'. + rewrite elem_of_list_omap in Hi'; destruct Hi' as ([j y]&Hj&?). + rewrite elem_of_map_to_list in Hj; simplify_option_equality. +Qed. + (** ** Properties of conversion from collections *) Lemma lookup_map_of_collection {A} `{FinCollection K C} (f : K → option A) X i x : -- GitLab