Defining Minkowski sums (and generally, designing API)

Stream: new members

[Philippe Duchon]

This is probably more a question on defining the "right" API for a new definition than it is about a specific definition.

#synth Add (Set ℝ) does not find anything, so I assume Mathlib does not know about the general Minkowski sum of two sets. So, I tried writing a definition in Lean - and in the process, maybe learn a bit more on defining things "right".

My first definition went like this:

import Mathlib
def Msum {M: Type} [Add M] (s1: Set M) (s2: Set M) : Set M := fun (x: M) ↦ ∃ (u: s1) (v: s2), x = u + v

But here, I am using the "sets are predicates" definition, so I should probably use the existing API for the image of a set by a mapping. So, my second definition was:

import Mathlib
def Msum2 {M: Type} [Add M] (s1: Set M) (s2: Set M) : Set M := (fun (c: M × M) ↦ c.1 + c.2) ''  s1 ×ˢ s2

(Is there a way to use the image without uncurrying the function?)

From there, I proceeded to prove associativity, and define instances of semigroup or monoid structures on Set M from the corresponding assumptions on M. But my proofs seem very clumsy - probably, partly due to lack of familiarity on my part, but also because I did not define a proper API around my definitions.

So - how does one decide what the "right" API would be for a new notion?

Also, defining an additive monoid structure on Set M requires defining a scalar multiplication by naturals, meaning 3 • ({2, 3}: Set ℕ) would denote the set {6,7,8,9} and not the set {6,9} of images under the "times three" mapping which would be a natural choice in other contexts. Again, I'm not sure what the best thing to do would be (or even if there is a right one).

I've been reading resources such as Mathematics in Lean, which explains (not always in full detail) why some things are set up the way they are, but it does not tell me how to decide how things should be set up.

[Sébastien Gouëzel]

Mathlib does know about the Minkowski sum, but it's not available without opening a scope.

import Mathlib
open Pointwise
#synth Add (Set ℝ)

[Sébastien Gouëzel]

It's docs#Set.add
You can look around in this file to see how this is implemented, and how the API is designed.

[Sébastien Gouëzel]

To find out whether something is already defined in Mathlib, there are several ways. The thing you did (checking #synth) is a good one, but here it failed because it's hidden behind a scope. Other ways are:

• grepping to see if "Minkowski sum" is mentioned somewhere (it's not)
• Ask loogle (https://loogle.lean-lang.org) about (_ : Set _) + (_ : Set _) (it works)
• Ask leansearch (https://leansearch.net/) about the Minkowski sum (it gives some good answers)

[Philippe Duchon]

Thanks! I also tried looking for Minkowski in the general documentation, but failed to try loogle because I'm not familiar enough with the patterns to search for.

And as I suspected, there is a lot of API in the existing files.

[Andrew Yang]

Arguably docs#Set.add should mention "Minkowski sum".