Default values not synthesizing

Stream: new members

[Eric Paul]

I made some definition for ordered groups that are not in mathlib and I am now trying to connect them with things already defined. I assume that things are a bit strange since the less rich structure LeftLinearOrderedGroup is not obviously extended by LinearOrderedCommGroup.

import Mathlib

variable {α : Type*}

class LeftOrderedGroup (α : Type*) extends Group α, PartialOrder α where
  mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b

class LeftLinearOrderedGroup (α : Type*) extends LeftOrderedGroup α, LinearOrder α

instance [LinearOrderedCommGroup α] : LeftLinearOrderedGroup α where
  mul_le_mul_left _ _ a b := mul_le_mul_left' a b
  le_total := LinearOrderedCommGroup.le_total
  decidableLE := LinearOrderedCommGroup.decidableLE

Given that I'm getting errors of the form "could not synthesize default value", I assume that this is not the right way to do things.

It's also not clear to me why this instance isn't working but these other ones are.

import Mathlib

variable {α : Type*}

class LeftOrderedGroup (α : Type*) extends Group α, PartialOrder α where
  mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b

class LeftLinearOrderedGroup (α : Type*) extends LeftOrderedGroup α, LinearOrder α

instance [OrderedCommGroup α] : LeftOrderedGroup α where
  mul_le_mul_left _ _ a b := mul_le_mul_left' a b

instance [LinearOrderedCommGroup α] : LeftOrderedGroup α := inferInstance

instance [LinearOrderedCommGroup α] : LeftLinearOrderedGroup α := sorry

[Daniel Weber]

The usual way to do this in Mathlib would be using docs#MulLeftMono, that is [Group α] [PartialOrder α] [MulLeftMono α] for LeftOrderedGroup, and [Group α] [LinearOrder α] [MulLeftMono α] for LeftLinearOrderedGroup

[Daniel Weber]

You can use spread notation to fill all fields that LinearOrderedCommGroup assigns:

import Mathlib

variable {α : Type*}

class LeftOrderedGroup (α : Type*) extends Group α, PartialOrder α where
  mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b

class LeftLinearOrderedGroup (α : Type*) extends LeftOrderedGroup α, LinearOrder α

instance [LinearOrderedCommGroup α] : LeftLinearOrderedGroup α where
  __ := inferInstanceAs (LinearOrderedCommGroup α)
  mul_le_mul_left _ _ a b := mul_le_mul_left' a b

[Eric Paul]

Oh awesome thank you! I didn't know about the spread notation. I still don't think I understand why it was necessary in this case but not in others.

For the definitions, I was copying how they are done in mathlib where OrderedCommGroup is defined. Basically, copying how mathlib does it, I add the mul_le_mul_left and then add instances for MulLeftMono. Do you think mathlib should switch to the spelling you used as well?