add map_zip_diag and the lemmas required for that

Is map_fmap_omap truly new? I was surprised to not find an existing lemma like that.

Is map_fmap_omap truly new? I was surprised to not find an existing lemma like that.

Seems so. The only lemma that relates omap and fmap is list_fmap_omap : g <$> omap f l = omap (λ x, g <$> f x) l. Unfortunately, this is different from your lemma.

I think it would be good to add that lemma for maps too, and add your lemma for lists too, and figure out some way how to name them properly.

added 1 commit

• 17f690be - add map_zip_diag and the lemmas required for that

Compare with previous version

mentioned in merge request iris!620 (merged)

added 1 commit

• e338cd47 - add map_zip_diag and the lemmas required for that

Compare with previous version

added 1 commit

• 00d810eb - add map_zip_diag and the lemmas required for that

Compare with previous version

added 1 commit

• 2a89273d - add list_fmap_alt

Compare with previous version

resolved all threads

I see you added the list lemma, thanks for that. For completeness and consistency, it would be nice to also have a variant of list_fmap_omap : g <$> omap f l = omap (λ x, g <$> f x) l for maps.

mentioned in issue #94 (closed)

added 1 commit

• 3a4a1be7 - add map_fmap_omap

Compare with previous version

resolved all threads

LGTM. Thanks. Merging.

merged

mentioned in commit 2bc4c093