Notation for set(like) product

Stream: general

[Yury G. Kudryashov]

I want to introduce

class has_set_prod (α β : Type*) (γ : out_param Type*) :=
(prod : α → β → γ)

infix `×ˢ`:72 := has_set_prod.prod

with instances for sets, finsets, sub* structures.

[Yury G. Kudryashov]

For non-sets we'll probably need a class that extends has_set_prod and adds an axiom (x, y) ∈ s ×ˢ t = x ∈ s ∧ y ∈ t.

[Yury G. Kudryashov]

Actually, we can add some has_mem arguments to has_set_prod and require (x, y) ∈ s ×ˢ t = x ∈ s ∧ y ∈ t right away.

[Yury G. Kudryashov]

What do you think? What precedence should I use (72 is just a number above 70 which is used for intersection)?

[Eric Rodriguez]

I'm quite a fan of this. Right now we have to use .prod right?

[Yury G. Kudryashov]

Yes.

[Yury G. Kudryashov]

A downside is that Lean can no longer infer the types of s and t in s ×ˢ t from the type of the expression.

[Adam Topaz]

This is a good idea! An analogue for pi types would be great too!

[Yury G. Kudryashov]

I don't want to do 2 refactors at once. Every time I tried it, I failed and merged none to the master.

[Yury G. Kudryashov]

I'll start by migrating set.prod.

[Kyle Miller]

Here's another sort of design for this that, while isn't quite so universe polymorphic, is able to say how it's related to the Cartesian product:

universes u

class has_set_prod (S : Type u → Type u) :=
(set_prod : Π {α β : Type u}, S α → S β → S (α × β))

infix `×ˢ`:72 := has_set_prod.set_prod

instance : has_set_prod set := ⟨λ α β s t, s.prod t⟩

example (s t u : set ℕ) : s ×ˢ t ×ˢ u = (s.prod t).prod u := rfl

I'm not sure if there's a good way to fix it, except for it taking three functions as arguments. Too bad there's not a way, at the typeclass level, to say "these are all the same function but with different universe variables", since there's not really a good out_param:

class has_set_prod (S : Type* → Type*) (S' : Type* → Type*) (S'' : out_param $ Type* → Type*) :=
(set_prod : Π {α β : Type*}, S α → S' β → S'' (α × β))

infix `×ˢ`:72 := has_set_prod.set_prod

instance : has_set_prod set set set := ⟨λ α β s t, s.prod t⟩

example (s t u : set ℕ) : s ×ˢ t ×ˢ u = (s.prod t).prod u := rfl

[Yury G. Kudryashov]

I don't think that your approach will work better with elaborator. And it won't work with submonoids because submonoid takes M : Type* and [monoid M].

[Yury G. Kudryashov]

#11300

[Floris van Doorn]

In the sphere eversion project I'm getting some unfortunate errors like this:

don't know how to synthesize placeholder
⊢ has_set_prod (set ?m_1) (set (ι → F)) (set (F × (ι → F)))

Is the intended notation now to give the explicit type to univ when using it in a product, like this: @univ A ×ˢ s?

[Johan Commelin]

cc @Yury G. Kudryashov

[Eric Wieser]

Probably (univ : set A) is the intended spelling

[Eric Wieser]

I think the problem is that there is no way for ×ˢ to know that its left and right arguments are the same type of container, as set A and set B are not even the same families of type when A and B are in different universes

[Eric Wieser]

Maybe there's some janky same_family typeclass we can use like

/-- A class that finds a version of `f`, a family of types in universe `u`,
that lives in universe `v` -/
class same_family (f : ι → Sort u) (g : out_param (ι → Sort v)).

which would help the elaborator with this kind of thing

[Anne Baanen]

Would that work for α and β in different universes? Then we can't use the same ι, right?

[Eric Wieser]

Oh, good point

[Yury G. Kudryashov]

/poll It seems that we have the following options:
continue using set.prod, submonoid.prod etc;
introduce different notations for set.prod, submonoid.prod etc;
have to specify the type of univ in univ ×ˢ t (and similarly for the empty set)

[Yaël Dillies]

Given that we can use dot notation, I'm happy to keep the set.prod, submonoid.prod alternative. This also keeps it in line with all the other type-like operations, like docs#finset.sigma, finset.disj_sum (in #11355), docs#finset.pi, docs#finset.dfinsupp, docs#finset.sym, ...

[Eric Wieser]

We can have notation for s.prod t without specifying which prod is meant

[Eric Wieser]

Notation supports that

[Yaël Dillies]

docs#finset.product

[Yury G. Kudryashov]

So, should we revert #11300?

[Johan Commelin]

For what it's worth, I really liked what #11300 did.

[Yaël Dillies]

I don't care much either way, but I'll probably keep using .prod myself.

[Yury G. Kudryashov]

You can't use .prod with #11300

[Yury G. Kudryashov]

(for sets)

[Floris van Doorn]

I think that despite this issue of having to provide explicit arguments to univ, I still prefer the new situation over the old one.

[Yaël Dillies]

Oh

[Yury G. Kudryashov]

I prefer the new notation (otherwise I wouldn't have introduced it) but this is not a strong preference. If someone will really wants to revert this change, then I'm OK with it (especially if I'm not the one who resolves conflicts after git revert 2865d8c2278c86).

[Yaël Dillies]

I genuinely don't mind much either way, so let's keep it like that for now.

[Yury G. Kudryashov]

If we decide to leave this notation for set product, then the next question is whether we should migrate submonoid.prod etc to this notation (e.g., by introducing a typeclass set_like.has_prod that extends has_set_prod and adds an assumption (x, y) ∈ s ×ˢ t ↔ x ∈ s ∧ y ∈ t)?