Additive properties?

Stream: Is there code for X?

[Robert Maxton]

What's the nicest way (or the way with the most existing API) to express "for some p : α → Prop, p (a + b) = p a ∧ p b" in instance search? So far, it seems like the best I've got is to define an instance for MonoidWithZero Prop (with * = ∧) and then require p : α →+ Additive Prop, but that's not terribly convenient and also doesn't really compose well, because e.g. if p is also multiplicative then I'd need p : α →*₀ Prop and it can't be both.

I could just use a Fact instance, but that has even less API support...

[Robert Maxton]

The intent here is that I have a bunch of bundled types that just expand out into Subtypes, and rather than defining a bunch of repetitive instances on each of them separately I'd like to define e.g.

instance [AddZeroClass α] (p : α →+ Additive Prop) : Add (Subtype p) := sorry

[Robert Maxton]

(In the long run/general case, this seems like a good choice for a deriving handler, and indeed I kind of plan to do that as well, but probably later.)

[Edward van de Meent]

although it is nice to abstract this behaviour, do note that adding MonoidWithZero Prop will make stuff like a = b * c = d valid syntax, which i think we don't want...

[Edward van de Meent]

also, please take a look at docs#AddSubmonoid, as the following works:

import Mathlib
variable {M : Type*} [AddMonoid M] (p : AddSubmonoid M) (x y : p)

#check x + y

[Andrew Yang]

Do you have any concrete applications in mind? It seems to me that there are no non-constant functions on additive groups that satisfy this property ?

[Edward van de Meent]

indeed on groups, a property p : M -> Prop with P (a + b) <-> P a /\ P b will be constant, since for all a and x, if p x, then also p ((x-a) + a), meaning that p (x-a) /\ p a, and we can conclude p a

[Edward van de Meent]

i do think that on monoids these properties can get more complex

[Jz Pan]

What about rewrite α → Prop as Set α? Currently they are definitionally equal, although the docstring said that "this is an implementation detail which should not be relied on".

[Robert Maxton]

Monoids were my original intended use case... though now that I think about it, I think I actually want docs#SubadditiveHomClass, which under the usual Prop ordering by implication is sufficient for what I want. (Which is to be able to easily define a bunch of bundled MatricesOfShape (triangular, diagonal, etc) types as aliases of various Subtypes, as otherwise for $n$ types and $m$ compatible operations each I end up needing to write like $3nm$ instances -- HFoo Submat Mat Mat, HFoo Mat Submat Mat, and Foo Submat.

[Robert Maxton]

It's a shame AddSubgroup etc doesn't seem to have nice autoParam tactics registered, because most of the proof obligations are closable by simp...