Some map_zip/map_zip_with properties.

These are some properties of map_zip_with that I am using so far. Perhaps you want me to port the whole thing first, to see what other functions/lemmas will I need?

I would except there to be three variants for the lemma:

• With an fmap in the first argument, i.e. map_zip_with f (g1 <$> m1) m2
• With an fmap in the second argument, i.e. map_zip_with f m1 (g <$> m2)
• With an fmap on the outside, i.e. g <$> map_zip_with f m1 m2

This lemma should follow from the first two lemmas that I mentioned.

Nitpick, use the <$> notation and unicode lambdas.

I would except there to be three variants for the lemma:

I actually use the first variant of the lemma, which follow from the "general" one + map_fmap_id. I guess there are multiple equiprovable sets of lemmas :)

Ah, right, of course!

I still guess that my first lemma is easier to use, you don't first have to massage your goal using map_fmap_id first (which requires a rewrite in opposite direction and thus careful subterm selection).

This one can be written with a prod_map g1 g2 on the LHS.

Looks good! I only have some small comments.

added 1 commit

• cd0b7f48 - Some map_zip/map_zip_with properties.

Compare with previous version

@robbertkrebbers What do you think of the changes now?

merged

Merged, thank you very much!