RFC: HUnion and HInter

Stream: lean4

[Rudy Peterson]

I would like to add typeclasses for heterogeneous union and intersection, generalizing Union and Inter the way HAdd does for Add.

Specifically, I would like to add the following to src/Init/Core.lean:

/--
The notation typeclass for heterogeneous union.
This enables the notation `a ⋃ b : γ` where `a : α`, `b : β`.
-/
class HUnion (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a ⋃ b` computes the union of `a` and `b`.
  The meaning of this notation is type-dependent. -/
  hUnion : α → β → γ

/--
The notation typeclass for heterogeneous intersection.
This enables the notation `a ∩ b : γ` where `a : α`, `b : β`.
-/
class HInter (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a ∩ b` computes the intersection of `a` and `b`.
  The meaning of this notation is type-dependent. -/
  hInter : α → β → γ

/-- `a ∪ b` is the union of`a` and `b`. -/
infixl:65 " ∪ " => HUnion.hUnion

/-- `a ∩ b` is the intersection of`a` and `b`. -/
infixl:70 " ∩ " => HInter.hInter

I am working on a pull request for mathlib4 with closure operations for automata, including union and intersection. It would be nicer if I could use a mathematical notation instead of an English name to make the code closer to pen-and-paper formalism.

Would this interfere with the current notations for Union and Inter...

Thanks!

[Patrick Massot]

Does such heterogeneous union and intersection exist anywhere on paper?

[Rudy Peterson]

Hmmm, good question.

In the automata literature I have seen sometimes math notation is not used to give the union of M1 and M2. It seems that often it is declared as "let M be the union of automata M1 and M2 such that L(M) = L(M1) ∪ L(M2)".

In one document where they use M1 + M2 for the "sum" automaton, and M1 × M2 for the "cartesian product" automaton, which they use to define the union and intersection respectively. This more closely reflects how I construct the operations.

Maybe + and × would be better for my purposes: it's a strange disconnect between defining automata on paper in set theory where there are no strict types and one can just do operations between different sets and in Lean where any distinctions are enforced...

[Patrick Massot]

It may be a case where the distinction is more important than for the average mathematical topic. We had lots of discussions about this in the context of matroids.

[Patrick Massot]

@Kyle Miller may want to take a look here.

[Peter Nelson]

Here is a link to a topic that Patrick is presumably referring to where I asked something like this - it was sdiff rather than union, for 'remove a thing' type operations in combinatorics.

#mathlib4 > Making SDiff heterogeneous? @ 💬

[Peter Nelson]

In the end, I just used a custom unicode backslash.

[Kyle Miller]

There's a technical hurdle with heterogenous operators. Homogeneous operators are able to use the expected type, which they propagate to their arguments, aiding elaboration.

Heterogeneous operators on the other hand don't have a mechanism to do that propagation on their own. This can mean lots of type ascriptions.

One partial solutions is default instances that apply the homogenous instance when all else fails.

For arithmetic operations, the rest of the solution is the binop% elaborator, which does the propagation using a metaprogram.

If core moves to use heterogenous unions and intersections, then it would need to change Union and Inter, which would affect Set in mathlib. It's possible that binop% would work with Set` arguments, but I worry about set operations and arithmetic operations interacting in surprising ways.