Deriving operations for structures

Stream: lean4

[Tomas Skrivan]

Are there deriving functions for deriving arithmetic operations for structures?

I would like to write

structure Vec2 (X : Type) where
  (x y : X)
  deriving Add, SMul ℝ

which would add instances Add X → Add (Vec2 X) and SMul ℝ X → SMul ℝ (Vec2 X)

A more complicated example:

structure Ball (R X : Type) where
  center : R
  radius : X
  deriving Add, SMul R

which would add instances Add R → Add X → Add (Ball R X) and Mul R → SMul R X → SMul (Ball R X).

Is there anything like this in mathlib/lean already? I couldn't find anything. Has anyone thought about this problem? I have done few attempts but I still do not have anything satisfactory.

[Kyle Miller]

Here's an approach using Mathlib:

structure Vec2 (X : Type) where
  (x y : X)

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

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

instance (X : Type) [Add X] : Add (Vec2 X) :=
  Add.ofEquiv (proxy_equiv% _)

With some more work, you could turn this into a derive handler (or at least a command, since SMul ℝ isn't supported by the deriving syntax). See for example the Fintype handler.

[Kyle Miller]

Or this unfinished PR for deriving LinearOrders: #3251

[Tomas Skrivan]

I saw the Fintype approach, I'm a bit worried about the generated code. I don't want to just prove theorems.

[Kyle Miller]

The least efficient part about the generated code is how it handles multiple constructors, but since structures have just one constructor, it might not be so bad.

[Kyle Miller]

It's worth evaluating it, and seeing what you can do to get it to inline everything in sight if necessary.

[Tomas Skrivan]

Yeah I might write some tactic that unfolds lots of the definitions involved.

[Kyle Miller]

For example, if you have a reduce% term elaborator, you could write

instance (X : Type) [Add X] : Add (Vec2 X) :=
  reduce% (Add.ofEquiv (proxy_equiv% _))

[Tomas Skrivan]

Sounds good, I will play around with this

[Tomas Skrivan]

So far so good, only one issue came up. Deriving instance for UniformSpace is a problem as it does not have instance for Sigma. Also I have some type classes that provide way simpler instance to Prod and I would prefer if proxy_equiv% would generate Prod if possible.

If I understand the code correctly I can alter defaultMkCtorProxyType to use Prod if possible. Not sure what are the downstream consequences of doing so.

[Kyle Miller]

I had to add a non-dependent Sigma instance for Add in the above code. Non-dependent sigma instances should have the same code as a Prod instance.

[Kyle Miller]

I think there's no problem adding Prod to the list of types that proxy_type% generates. It just increases the complexity a bit, and you have to be sure all the documentation that promises "if you implement instances for this list of types, then deriving handlers will work"

[Tomas Skrivan]

Kyle Miller said:

I had to add a non-dependent Sigma instance for Add in the above code. Non-dependent sigma instances should have the same code as a Prod instance.

Ah that is right, just using Sigma is probably ok. I have to play around with it a bit more.