Zulip Chat Archive

Stream: Is there code for X?

Topic: filter map₂ as map

Bernd Losert (Apr 17 2022 at 18:37):

I couldn't find the following:

example (m : α → β → γ) (f : filter α) (g : filter β): filter.map₂ m f g = filter.map (uncurry m) (f ×ᶠ g) := by library_search

Yaël Dillies (Apr 17 2022 at 18:42):

I didn't add it. Do we have the corresponding set.image2 lemma?

Bernd Losert (Apr 17 2022 at 18:42):

Let me see...

Yaël Dillies (Apr 17 2022 at 18:43):

Doesn't seem so

Bernd Losert (Apr 17 2022 at 18:44):

Nope.

Bernd Losert (Apr 17 2022 at 18:45):

Was it intentional that filter.map₂ was not defined in terms of the applicative instance?

Yaël Dillies (Apr 17 2022 at 18:46):

Yes, because we care about definitional equality.

Yaël Dillies (Apr 17 2022 at 18:47):

So yeah we actually have the two lemmas you ask for, but not quite in your form: docs#set.image_prod, docs#filter.map_prod.

Bernd Losert (Apr 17 2022 at 18:47):

How does defintional equality affect things? I don't follow.

Yaël Dillies (Apr 17 2022 at 18:47):

This is a concern for the end user.

Bernd Losert (Apr 17 2022 at 18:51):

Which end user? I'm an end user and it' affecting me, but I don't see the connection with definitional equality.

Bernd Losert (Apr 17 2022 at 18:55):

Seems that we're also missing this applicative combinator:

example {f : Type u → Type v} [applicative f] (fa : f α) (fb : f β) : f (α × β) := by library_search

Yaël Dillies (Apr 17 2022 at 18:58):

When you have hx : x \in filter.map\2 m f g, you can obtain \<s, t, hs, ht, h\> := hx.

Bernd Losert (Apr 17 2022 at 19:07):

Yes, that is nice. The way I was doing that without map2 was kind of painful.

Bernd Losert (Apr 17 2022 at 19:09):

Anyways, I'll make a PR to add the map2 as map for filter.

Bernd Losert (Apr 17 2022 at 19:26):

Question: why does docs#set.image_prod and docs#filter.map_prod not use uncurry f. Is there some advantage to having the explicit lambda?

Yaël Dillies (Apr 17 2022 at 19:31):

Yeah, this allows rewriting inside the lambda.

Reid Barton (Apr 17 2022 at 19:43):

It makes it easier for Lean to infer f by unification

Bernd Losert (Apr 17 2022 at 19:46):

Bernd Losert (Apr 17 2022 at 20:08):

I've heard the mathlib community prefers to have names of lemmas, definitions etc. in plain ascii although it seems we're not doing this for the map₂ stuff. I guess we're bending the rules here?

Yaël Dillies (Apr 17 2022 at 20:10):

That's not the only place we do this. For example we use numerals in indices to indicate an "iterated" operation: forall₂ refers to ∀ a b, _, exists₂ to ∃ a b, _, etc.

Bernd Losert (Apr 17 2022 at 20:13):

I see. I guess subscript indices are still OK, although they are hard to type in the browser.

Yaël Dillies (Apr 17 2022 at 20:14):

What browser are you using? We have browser extensions to type unicode in the same way as in VScode, as well as a system-wide version.

Bernd Losert (Apr 17 2022 at 20:15):

I use Chrome. I usually copy/paste the fancy unicode into the browser. But Chrome search is pretty aweful, since it has problems distinguishing e.g. fancy unicode letters from plain ascii ones.

Bernd Losert (Apr 17 2022 at 20:17):

For example, searching for 𝓟 gives you all the regular ascii p's.

Yaël Dillies (Apr 17 2022 at 20:17):

Wait, are you not using the API documentation search?

Bernd Losert (Apr 17 2022 at 20:19):

Yes, I use that too.

Yaël Dillies (Apr 17 2022 at 20:19):

The Chrome extension is https://github.com/arthurpaulino/chrome-lean-unicode

Bernd Losert (Apr 17 2022 at 20:20):

Oh, nice.

Bernd Losert (Apr 17 2022 at 21:43):

Here's the PR: https://github.com/leanprover-community/mathlib/pull/13490/files

Last updated: Dec 20 2023 at 11:08 UTC