Monoid for a structure

Stream: new members

[Evgeny Kurnevsky]

Hi. Is there an easy way to define Mul/Semigroup/Monoid hierarchy for a structure with 2 fields? I can pretty easily define MyStruct ≃ Nat × Nat which probably can be used somehow?

[Evgeny Kurnevsky]

Prod requires some proofs: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Algebra/Group/Prod.lean so defining it by hand would also require me to write those proofs..

[Tomas Skrivan]

I'm aware of one approach.

Use mathlibs proxy_equiv% which for a creates an equivalence between the structure with a type build out of Sigma, Sum and Unit.

Then define function <strcture>.ofEquvi which transfers the algebraic structure along and equivalence. For example

def AddCommGroup.ofEquiv {X Y : Type*} [AddCommGroup X] (f : X ≃ Y) : AddCommGroup Y where
   ...

Then you can provide the instance for your structure S like

instance : AddComGroup S := AddCommGroup.ofEquiv (proxy_equiv% S)

Short mwe for addition

import Mathlib

instance {X Y : Type*} [Add X] [Add Y] : Add ((_ : X) × Y) where
  add | ⟨x1, y1⟩, ⟨x2, y2⟩ => ⟨x1 + x2, y1 + y2⟩

def Add.ofEquiv {X Y : Type*} [Add X] (f : X ≃ Y) : Add Y where
  add a b := f (f.symm a + f.symm b)

structure Vec3 where
  (x y z : Nat)

instance : Add Vec3 := Add.ofEquiv (proxy_equiv% Vec3)

#eval Vec3.mk 1 2 3 + Vec3.mk 10 100 1000

[Tomas Skrivan]

Here I have a file setting it up to get NormedSpace but all the proofs use sorry right now.

[Tomas Skrivan]

I would really like to write something like

structure Vec3 (R : Type*) where
  (x y z : R)
deriving  [AddCommGroup R] -> NormedAddCommGroup,
          {S : Ring} [AddCommGroup R] [Module S R] -> Module S

[Tomas Skrivan]

I'm curious if anyone thought about automatically generating these instances a bit more. I'm have been thinking about it for quite some time and still don't know what would be the best approach.

For the above structure Vec3 R the deriving [AddCommGroup R] -> AddCommGroup would ideally trigger a sequence of instances:

instance [Add R] : Add (Vec3 R) := ...
instance [AddSemigroup R] : AddSemigroup (Vec3 R) := ...
instance [AddCommMagma R] : AddCommMagma (Vec3 R) := ...
...
instance [AddCommGroup R] : AddCommGroup (Vec3 R) := ...

I can of course hardcode this particular sequence of instances but ideally it would be automatically generated.

I think there are effectively two questions:

1. Figure out the sequence of typeclasses for which to derive an instance.
2. For each typeclass figure out the necessary constraints on the structure parameters

Partial answers:

1. This is probably easy as you can just walk the class hierarchy. For example, AddCommGroup extends AddGroup AddCommMonoid. So you try to derive instances for those first. I'm not sure how to prevent diamonds though as a naive application of the approach above would mean calling AddGroup.ofEquiv and AddCommMonoid.ofEquiv which would create two instances of Add on Vec3 and that is bad.

2. The task is to figure out the "minimal/sufficient/obvious" conditions under which you can provide an instance AddCommGroup (Vec3 R). It would be great to be able to run some kind of analysis on failed typeclass synthesis and figure out the minimal set of instances to make the synthesis to succeed. Such analysis would be also great for improving typeclass synthesis error messages.

[Kyle Miller]

Relatedly, something I got a bit stuck on with #3251 (deriving LinearOrders) was what API should be automatically generated to support the derived LinearOrder. It seems that most derived typeclasses don't need any supporting theory, but for this you do want to know how the order is related to the actual inductive type. Similarly, for these algebraic structures, you want to know how the operations are related to the inductive type.