Making SDiff heterogeneous?

Stream: mathlib4

[Peter Nelson]

I would like to make SDiff heterogeneous so it can denote more general 'removals' than set difference in cases where \ is standard notation, such as removing sets of edges from a graph. I don't have enough experience for such things - is this a major change/bad idea?

[Eric Wieser]

The danger of using notation is that it gives the false impression that any of the existing lemmas about sdiff could be used here

[Eric Wieser]

In this case can't you define sdiff to remove one graph from another?

[Eric Wieser]

That is, G \ SimpleGraph.mkFromEdgeSet s or similar?

[Yury G. Kudryashov]

There are at least two reasonable "diff" operations on graphs: remove edges and remove vertices.

[Peter Nelson]

Yes, and you can also remove either sets of edges/vertices or single edges/vertices - I think that's a good argument for heterogeneity. (I actually have deletions of elements /sets of matroids in mind; I just wanted to pick a more familiar example).

[Peter Nelson]

It's a little annoying to not be able to use standard mathematical notation for those things, just because that symbol happens to be defined for sets.

[Yury G. Kudryashov]

You can always introduce notation like \ₑ

[Peter Nelson]

What is different between this and the heterogeneity of +, /, etc that was introduced in lean4? I was happy to see this, before I saw that SDiff wasn't included.

[Yury G. Kudryashov]

We don't use HAdd in mathlib (yet).

[Yury G. Kudryashov]

SDiff is defined in mathlib

[Yury G. Kudryashov]

An interesting question is whether we can use heterogeneous multiplication for both left and right actions.

[Yury G. Kudryashov]

Is there a situation when A acts on B on the left and B acts on A on the right?

[Yury G. Kudryashov]

(so that we can't decide what's the correct meaning of (a : A) * (b : B))?

[Eric Wieser]

Yury G. Kudryashov said:

There are at least two reasonable "diff" operations on graphs: remove edges and remove vertices.

Only "remove edges" is well-typed as sdiff for docs#SimpleGraph

[Eric Wieser]

Yury G. Kudryashov said:

Is there a situation when A acts on B on the left and B acts on A on the right?

There are many such situations; but the relevant question is probably "in what situations are the two not defeq", and I have none in mind yet

[Kyle Miller]

Yury G. Kudryashov said:

An interesting question is whether we can use heterogeneous multiplication for both left and right actions.

I think we learned the answer to this is "no", and for reasons other than the left/right ambiguity. x ^ y is a right action, and we've had lots of trouble with its binop% casting rules throughout the port. I have some code that makes the casting be for a right action (the assumption is it will likely have types X -> Y -> X, with Y having no relationship to X), and I was hoping to eventually get it into Lean so that we can remove our macro_rules overrides.

[Kyle Miller]

I think \ does make sense as another kind of right action (though I'm not saying anything about it being confusing to use this notation). I wonder if there's a good symbol for an inverse to it? It shouldn't be union/sup since that should be symmetric

[Yury G. Kudryashov]

So, while Lean 4 has docs#HAdd, we are not going to use it anywhere because of parsing rules for a + b? Should we drop docs#HSMul then?

[Kyle Miller]

The issue with HPow in particular is that we don't want y in x ^ y to be coerced just because x has another type and y can be coerced to it. The binop% algorithm looks at the types of everything in an algebraic expression and tries to find a single type everything coerces to.

[Kyle Miller]

I think it's fine having heterogenous operator instances when there aren't coercions between the operands. (Nat just happens to be able to coerce to every ring, which makes x ^ n be the unexpected thing.)

[Eric Wieser]

I think I thought about HSMul a bit while writing my scalar actions paper, and concluded that HSMul X X Y would open up a massive number of typeclass diamonds.

[Peter Nelson]

So would having G \ e := G \ ({e} : Set E) be problematic for an edge e : E in a graph G?

[Jireh Loreaux]

Peter, I think it's safest to just make modified \ notation as Yury suggested above. If we determine it's possible to merge the two notations, it's always possible to do later.

[Yury G. Kudryashov]

E.g., we merged different ×ˢ notations recently.

[Eric Wieser]

Peter Nelson said:

So would having G \ e := G \ ({e} : Set E) be problematic for an edge e : E in a graph G?

I still think you'd do better to promote {e} to a graph so that you can use docs#SimpleGraph.completeBooleanAlgebra

import Mathlib.Combinatorics.SimpleGraph.Basic

example {V : Type u} (G : SimpleGraph V) (e : Sym2 V) : SimpleGraph V :=
  G \ SimpleGraph.fromEdgeSet {e}

[Kyle Miller]

Peter Nelson said:

So would having G \ e := G \ ({e} : Set E) be problematic for an edge e : E in a graph G?

It seems like it would work? It'd take engineering effort to redo SDiff and maybe it'd take changes to Lean if there are issues. I wouldn't try doing vertex deletions too with this notation.

[Peter Nelson]

Yup, I'm already using modified notation; there is basically no other way. It just makes things look less pretty than I'd like.

And that was my original question really - what are the engineering issues? And it looks like the answer is that there really are some.

[Peter Nelson]

Eric Wieser said:

Peter Nelson said:

So would having G \ e := G \ ({e} : Set E) be problematic for an edge e : E in a graph G?

I still think you'd do better to promote {e} to a graph so that you can use docs#SimpleGraph.completeBooleanAlgebra

The graph thing was really a toy example - I'm working in a situation where you can't do something like that.

[Kyle Miller]

You need to be able to reliably figure out the type of the SDiff expression and propagate types to its operands

[Kyle Miller]

For example, without additional support, S \ {x, y} won't elaborate, since it will say it can't infer an Insert instance for the {x, y} notation

[Jireh Loreaux]

Kyle, isn't that not a problem anymore because of default_instances? Or is that what you mean by "additional support"?

[Kyle Miller]

There are a couple pieces to the additional support. Default instances are one, but the binop% and unop% elaborators are another.

[Kyle Miller]

Yury G. Kudryashov said:

E.g., we merged different ×ˢ notations recently.

Yeah, getting this to (finally) work reliably took a custom elaborator: https://github.com/leanprover-community/mathlib4/blob/41a80d7f6a9db42342210225d6fc50f34781b9b3/Mathlib/Tactic/FBinop.lean

[Kyle Miller]

@Jireh Loreaux I forgot to mention what a point of binop% and unop% are: they figure out where you need to insert coercions so that the default instances can be applied

[Kyle Miller]

@Peter Nelson There's a chance that it might all Just Work if someone made SDiff be heterogenous, made a homogenous version, used this to give the heterogenous one a default instance, and installed a binop% macro rule for SDiff, and then cross a couple fingers and compile mathlib

[Peter Nelson]

That sounds great - I don't think I understand enough of the under-the-hood stuff to be that someone, though!

[Jireh Loreaux]

Peter, just have a look at the existing HMul and Mul, then ask Kyle where to find a good %binop example. This should be mostly mimicry.

[Kyle Miller]

I'm a mimic too, and I've just picked up on it by trying to read a lot of core code. My understanding is that the following pieces are what you need for a heterogenous arithmetic-like operator that prefers to be homogenous. For multiplication:

• https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L1157
• https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L1273
• https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L1372
• https://github.com/leanprover/lean4/blob/master/src/Init/Notation.lean#L276
• https://github.com/leanprover/lean4/blob/master/src/Init/Notation.lean#L295