!4#4200

Stream: mathlib4

[Chris Hughes]

Does someone want to bump !4#4200 on the queue. I'm very happy but they're big enough changes that I thought maybe someone else would want a look as well.

[Mario Carneiro]

I'm not too sure about the original presupposition of the PR, that lean 4 doesn't handle overloaded notation. Is there a #mwe demonstration of the issue?

[Mario Carneiro]

I suspect the problem is that if you use notation to introduce the notation multiple times, you will introduce overlapping syntax and the parser will not be able to differentiate them, but if you have one syntax and multiple macro_rules then it should be resolved in a type-directed way as desired

[Mario Carneiro]

@Pol'tta / Miyahara Kō

[Pol'tta / Miyahara Kō]

This is MFE:

universe u v

axiom Set (α : Type u) : Type u
axiom Set.prod {α : Type u} {β : Type v} (s : Set α) (t : Set β) : Set (α × β)
infixr:82 " ×ˢ " => Set.prod

axiom Finset (α : Type u) : Type u
axiom Finset.product {α : Type u} {β : Type v} (s : Finset α) (t : Finset β) : Finset (α × β)
infixr:82 " ×ˢ " => Finset.product

axiom Finset.toSet {α : Type u} (s : Finset α) : Set α
noncomputable instance {α : Type u} : CoeTC (Finset α) (Set α) := ⟨Finset.toSet⟩

example {α : Type u} {β : Type v} (s : Finset α) (t : Finset β) : s ×ˢ t = s ×ˢ t := rfl
-- ambiguous, possible interpretations
--   s ×ˢ t : Finset (α × β)
--   ?m.15525 ×ˢ ?m.15619 : Set (?m.15430 × ?m.15431)

[Kyle Miller]

I'm not sure if it breaks anything, but giving the Finset notation a higher priority fixes the ambiguity:

infixr:82 (priority := high) " ×ˢ " => Finset.product

It seems the problem is that the Set.prod notation does apply due to the coercion (though for some reason only on the LHS of the equality, so I had to write s ×ˢ t = (s : Set α) ×ˢ (t : Set β) if I comment out the Finset.product notation)

[Kyle Miller]

We switched to the notation solution in mathlib3 from a typeclass solution because it avoids type ascriptions -- adding these type ascriptions back in mathlib4#4200 is sort of undoing the work from just a year or so ago (though I do appreciate how it turns ×ᶠ back into ×ˢ!).

[Kyle Miller]

Maybe typeclasses are the right solution in the end, but I'd like to see it done where you don't need additional type ascriptions.

[Kyle Miller]

Can we write an elaboration helper that is able to solve for the correct type? sort of like how binop% helps with arithmetic, but we'd have prod% for helping to resolve the prod using the types of the arguments and the expected type all together?

[Kyle Miller]

I think I got a design that works and avoids the type ascriptions:

import Lean
import Mathlib.Data.Set.Prod
import Mathlib.Data.Finset.Prod

universe u v w

/-- Notation type class for the set product `×ˢ`. -/
class HSProd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- The cartesian product `s ×ˢ t` is the set of `(a, b)` such that `a ∈ s` and `b ∈ t`. -/
  hSprod : α → β → γ

class SProd (s : Type u → Type u) (s' : Type u' → Type u')
    (s'' : outParam (Type (max u u') → Type (max u u'))) where
  /-- The cartesian product `s ×ˢ t` using explicit type constructors (see also `HSProd.hSprod`). -/
  sprod : s α → s' β → s'' (α × β)

-- This notation binds more strongly than (pre)images, unions and intersections.
@[inherit_doc HSProd.hSprod] infixr:82 " ×ˢ' " => HSProd.hSprod
-- *Edit:* This line apparently doesn't do anything in this case. Commenting it out
-- macro_rules | `($x ×ˢ' $y)   => `(binop% HSProd.hSprod $x $y)

@[default_instance] instance [SProd s s' s''] : HSProd (s α) (s' β) (s'' (α × β)) := ⟨SProd.sprod⟩

@[default_instance] instance : SProd Set Set Set := ⟨Set.prod⟩

instance : SProd Finset Finset Finset := ⟨Finset.product⟩

example (s : Set α) (t : Set β) : s ×ˢ' t = s ×ˢ' t := rfl
example {α : Type u} {β : Type v} (s : Finset α) (t : Finset β) : s ×ˢ' t = s ×ˢ' t := rfl

example (f : α × α → β) (s : Set (α × α)) : s.InjOn f := sorry
example (f : α × α → β) (s t : Set α) : (s ×ˢ' t).InjOn f := sorry
example (f : α × α → β) (s t : Finset α) : (s ×ˢ' t : Set (α × α)).InjOn f := sorry
example (f : α × α → β) (s t : Finset α) : ((s : Set _) ×ˢ' (t : Set _)).InjOn f := sorry
example (f : α × α → β) (s t : Finset α) : Set.InjOn f (s ×ˢ' t) := sorry

[Kyle Miller]

Hmm, I could have sworn that I did a test where the macro_rules line was necessary, but it doesn't seem to be in any of these examples...

[Kyle Miller]

(And maybe binop% doesn't work for something quite as heterogeneous as set products)

[Kyle Miller]

This is likely still not as good as it can be. Ideally the HSProd default instance could constrain s, s', and s'' to be the same constant modulo universe variables, so perhaps a prod% elaborator is still in order.

[Yaël Dillies]

Also it would be great if we could unify the Prod notation with all the other products. The superscript is particularly annoying for me to enter and there isn't really any reason it's there besides "We couldn't make the notation work in Lean 3"

[Pol'tta / Miyahara Kō]

This idea can be implemented using the new attribute prod_notaion.

[Kyle Miller]

I made a binop%-like elaborator for "functorial" types (Set, Finset, etc.) and coercions between them. The binop% elaborator tries to solve for a single type that everything can be coerced to, but that doesn't work here since the product operator is inherently inhomogeneous. Instead, fbinop% tries to find coercions while swapping out Set, Finset, etc. for another such "functor." (I'm calling these functors in a loose sense, functions Type u -> Type v.)

[Kyle Miller]

If anyone would be kind and test it out, it's at mathlib4#4308

[Kyle Miller]

Here are a few things it lets you do without type ascriptions:

example (s : Finset α) (t : Set β) (u : Finset γ) : Nat.card (s ×ˢ t ×ˢ u) = 0
-- After elaboration: Nat.card ↑(↑s ×ˢ t ×ˢ ↑u) with the Finsets as Sets

example (s : Set α) (t : Set (α × ℕ)) : s ×ˢ {1, 2, 3} = t
-- The {1, 2, 3} is a Set

example (s : Finset α) (t : Finset (α × ℕ)) : s ×ˢ {1, 2, 3} = t
-- The {1, 2, 3} is a Finset

[Kyle Miller]

Just like other core operators, it pushes coercions inward among a tree of fbinop% expressions. Here's another example with that:

example (f : α × α → β) (s t : Finset α) : (s ×ˢ t : Set _).InjOn f
-- Set.InjOn f (↑s ×ˢ ↑t) with the Finsets as Sets

[Kyle Miller]

Pinging @Pol'tta / Miyahara Kō

[Kyle Miller]

Kyle Miller said:

adding these type ascriptions back in mathlib4#4200 is sort of undoing the work from just a year or so ago

I take this back -- I didn't look at all 56 files of changes carefully enough. Now I think every type ascription that was added are fine and justified, and this PR is a definite improvement. I'm not comfortable merging it myself though because I don't really understand what ramifications it has on the porting effort -- is there any reason not to?

This fbinop% (or something like it) would just be nice to have, and I don't think mathlib4#4200 should wait for it.