Packaging conditions as type class possible? Other solutions

Stream: mathlib4

[Stephan Maier]

Hi, I find that lists of variables can get rather long. Imagine trying PL-topology without going straight into R^n. Is there a way to simplify such variable lists? Here is an easy and limited example from purely algebraic "PL-topology":

/-- These are the typs that are needed -/
class AlgebraicPLSpace (𝕜 : Type u) (V : Type v) (P : Type w) where
  is_StrictOrderedCommRing : StrictOrderedCommRing 𝕜
  is_AddCommGroup : AddCommGroup V
  is_Module: Module 𝕜 V
  is_NoZeroSMulDivisors : NoZeroSMulDivisors 𝕜 V
  is_AddTorsor : AddTorsor V P

/-- OK, this here does noit compile. Trying tu use Coe's of various kinds does not help: -/
example [AlgebraicPLSpace 𝕜 V P] (x y : P) := affineSegment 𝕜 x y

/-- This would be the way out. But I need to repeat this too often! -/
variable (𝕜 : Type u) [OrderedCommRing 𝕜]
variable (V : Type v) [AddCommGroup V] [Module 𝕜 V] [NoZeroSMulDivisors 𝕜 V]
variable (P : Type w) [AddTorsor V P]

/-- Or would I write a mcro that expands as follows: -/
-- variables [AlgebraicPLSpace 𝕜 V P] ---- expandes to ----> the variable list above?

Any thoughts. And sorry, if this has been asked before.
Cheers, Stephan

[Calle Sönne]

I have not been able to test this, since I don't know exactly what to import to make this compile. But have you tried adding:

instance [h : AlgebraicPLSpace 𝕜 V P] : StrictOrderedCommRing 𝕜 := h.is_StrictOrderedCommRing
instance [h : AlgebraicPLSpace 𝕜 V P] : AddCommGroup V := h.is_AddCommGroup
(and so on)

before example [AlgebraicPLSpace 𝕜 V P] (x y : P) := affineSegment 𝕜 x y? This should make it so that lean can deduce StrictOrderedCommRing from a given instance of AlgebraicPLSpace.

[Anne Baanen]

I'm afraid it is not technically possible to follow Calle's approach or Stephan's first approach: the problem here is that to find an instance of e.g. StrictOrderedCommRing 𝕜 from an instance of AlgebraicPLSpace 𝕜 _ _, the problem is in figuring out what the V and P are supposed to be that fill in the _s. In principle that could be any type. So the algorithm doesn't like these instances.

[Anne Baanen]

There have been various proposals for a macro that would expand [AlgebraicPLSpace 𝕜 V P] into a full list of instances, but they have been less popular for various reasons. Mostly to do with how to deal with variables that have already been declared. That is, questions like: assume we have a line above variable [Field 𝕜], should [AlgebraicPLSpace 𝕜 V P] be smart enough to expand into [OrderedField 𝕜] instead of [OrderedCommRing 𝕜]?

[Anne Baanen]

For now, the closest we have is variable? [AlgebraicPLSpace 𝕜 V P] which return the full variable declaration as a suggestion. At least that should save you some typing, even if reading the full declaration is still extremely long.

[Calle Sönne]

Oh I see, sorry about that!

[Stephan Maier]

Anne Baanen said:

I'm afraid it is not technically possible to follow Calle's approach or Stephan's first approach: the problem here is that to find an instance of e.g. StrictOrderedCommRing 𝕜 from an instance of AlgebraicPLSpace 𝕜 _ _, the problem is in figuring out what the V and P are supposed to be that fill in the _s. In principle that could be any type. So the algorithm doesn't like these instances.

Thanks a lot. I suspected as much. I did try what Calle proposed. Never mind. I appreciate that interferences are a chelenge when generating code. So I rest my case. Thanks for the hint with variable?.