Make use of loopy instances for implications between Co(ntra)variantClasses

[alreadydone]

Currently in mathlib there are three versions of essentially the same statement with slightly different typeclass assumptions: Left.add_eq_add_iff_eq_and_eq Right.add_eq_add_iff_eq_and_eq eq_and_eq_of_le_of_le_of_add_le and the corresponding Mul versions (plus two more).

In the first and second (@tb65536, @negiizhao), the assumptions are PartialOrder with Covariant LE and Contravariant LE w.r.t. one of the arguments, and Covariant LT and Contravariant LE w.r.t. the other argument. In the third (@adomani), LinearOrder is assumed instead, and Contravariant LE w.r.t. the second argument is omitted.

The minimal assumptions in this case is actually PartialOrder with Covariant LT in both arguments. In fact, Contravariant LE implies Contravariant Eq (= Covariant Ne), and Covariant LE together with Covariant Ne suffice to imply Covariant LT. (Conversely, Covariant LT implies Covariant LE because Covariant Eq (= congrArg) is trivially true.)

I think people may not have sorted out all such possible implications before, and it would be beneficial to record all implications I've found (hopefully complete) here: they are all in mathlib except for the last two, but they are not made instances, probably due to the possibility of looping. There is a potential to take advantage of Lean 4's typeclasses system (which allows loopy instances) to substantially reduce duplications in this part of mathlib.

In LinearOrder: Covariant LE ↔ Contravariant LT Covariant LT ↔ Contravariant LE

In PartialOrder: Covariant LT → Covariant LE Contravariant LE → Contravariant LT Contravariant Eq ∧ Covariant LE → Covariant LT Contravariant Eq ∧ Contravariant LT ↔ Contravariant LE

---

Some other observations about the original three lemmas and the files they are in:

• There's actually no need to state the lemmas separately for Add and Mul. Some (Add)CommSemigroup assumption could be replaced by IsCommutative so there's no need to distinguish Mul and Add.

• Function.swap is used in all three lemmas, but elsewhere in the file(s) flip is used. I think flip is better, since it's @[inline] while swap isn't @[reducible], and Lean 4 should be able to deal with instances like [IsCommutative f] [Covariant (flip f) r] : Covariant f r without going into a loop.

• The bundled commutative ordered monoid typeclasses (Linear)Ordered(Cancel)CommMonoid/Group allows us to prove only co(ntra)variance w.r.t. one of the arguments, but with the commutation instance above we may not need the bundling and can use Co(ntra)variantClasses directly. (In fact the left/right-ordered noncommutative monoids aren't made into typeclasses yet, but also mathlib has nothing about them other than this co(ntra)variance stuff.) Here is a chart of relevant typeclasses:

Covariant LE	PosMulMono	OrderedCommMonoid	OrderedSemiring
Covariant LT	PosMulStrictMono		StrictOrderedSemiring
Contravariant LE	PosMulMonoRev	OrderedCancelCommMonoid
Contravariant LT	PosMulReflectLT
Contravariant Eq	IsLeftCancelMulZero (?) / IsDomain	IsCancelMul

• AddGroup.covariant_iff_contravariant could also be broken down into two instances in Lean 4.

I'm about to start unifying those three lemmas, adding instances and removing duplicates along the way, and I can't easily estimate how much stuff need to fixed downstream. As this is potentially a big project overall, and may induce big change in the library, I'm opening this issue as a request for comments. cc @YaelDillies

[adomani]

I like your suggestions! I remember that I tried to be careful about not introducing loops in the typeclass system and had to make some compromises.

I would be really happy to see how the new loop-avoidance allows more natural implications.

Also, I haven't looked carefully at your suggestions, but at a cursory glance, they all look like improvements.

Thanks!

[alreadydone]

I just realized Lean 4's typeclass inference isn't as smart as I thought:

instance IsSymmOp.flip' {α β} (op) [IsSymmOp α β (flip op)] : IsSymmOp α β op where
  symm_op := fun a b ↦ symm_op (op := _root_.flip op) b a

instance IsSymmOp.flip {α β} (op) [IsSymmOp α β op] : IsSymmOp α β (flip op) :=
  inferInstance
/- failed to synthesize
  IsSymmOp α β (_root_.flip op)
(deterministic) timeout at 'typeclass', 
maximum number of heartbeats (20000) has been reached 
(use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/

instance IsSymmOp.flip' {α β} (op) [IsSymmOp α β op] : IsSymmOp α β (flip op) where
  symm_op := fun a b ↦ symm_op b a

instance IsSymmOp.flip {α β} (op) [IsSymmOp α β (flip op)] : IsSymmOp α β op :=
  inferInstance
/- failed to synthesize instance
  IsSymmOp α β op -/

I could add both instances but I don't want the flip op -> op instance to cause timeouts when the instance is nowhere to be found. Maybe I was just too optimistic, because for this to work we need function eta during instance search, which is probably too costly. This looks like it will affect my plans about commutativity, but maybe this instance isn't actually important, we'll see.

[alreadydone]

6677 is a draft PR to address this issue; I've replaced bundled CommSemigroup/Monoid etc. by Mul + IsSymmOp (I'm puzzled by porting notes saying IsSymmOp is not available), and replaced mul and add by a general operation when possible.

covariantClass_le_of_lt is the only instance I added; covariant_lt_of_covariant_le_of_contravariant_eq and contravariant_le_of_contravariant_eq_and_lt are meant to replace existing instances if and when the definitions of Mul/AddCancel typeclasses are changed to use co(ntra)variance. I have not made the Group iffs instances.

In the file Monoid/Lemmas, although everything up to min_le_max_of_mul_le_mul can be generalized an arbitrary operation (since they don't involve One or Zero), and I could change the name to something like min_le_max_of_op_le_op and keep the original names (mul and add versions) as aliases, I choose not to do so, because

• to_additive works well enough so we only need to write the Mul version

• there are probably not many operations we are interested in other than Mul and Add

• some theorems' conclusions only involve (in)equalities and don't involve the operation, so you would need to specify the operation when applying such a theorem, which can be annoying.

As I went through the files I came across yet another variant mul_le_mul_iff_of_ge of eq_and_eq_of_le_of_le_of_mul_le which is simply its iff version, with a much simpler proof, so I just deleted the latter, and I'm about to change UniqueProds.lean to use the former.

Once I finish the file Ring/Lemmas, I'll open the PR for review, and leave future work to other people who are interested.

[alreadydone]

Here is the Hasse diagram of the implication preorder on all possible combinations of the following 5 co(ntra)variance properties on a partial order:

1. Covariant LE
2. Covariant LT (implies 1 so always appear with 1)
3. Contravariant LE (equivalent to 4+5, omitted in diagram)
4. Contravariant LT
5. Contravariant Eq (cancellation property)

In a (left or right) cancellative monoid, we only need to look at the top face of the cube. In a group, we have 1=2=4=5 so the diagram collapses down to two nodes.

An OrderedCancelCommMonoid satisfies both 1 and 3(=4+5), so it actually satisfies all five properties, which can already be inferred by the typeclass system.

In a linear order, 1=4 and 2=3=4+5, and we're reduced to four nodes: 1245 (Contra LE = all properties = Co LT), 14 (Contra LT = Co LE), 5 (Contra Eq), and ∅.

Appendix

To verify that this is the correct Hasse diagram, it suffices to show:

• 4+5 doesn't imply 1 (hence doesn't imply 2) i.e. Contra LE doesn't imply Co LE: consider the partial order on ℕ such that m ≤ n iff m = 0 or m = n.

• 1+4 doesn't imply 2 i.e. Co LE + Contra LT doesn't imply Co LT: consider Fin 2 with capped addition (1+1=1).

• 1+2+5 doesn't imply 4 i.e. Co LT + Contra Eq doesn't imply Contra LT: consider the usual order on ℕ, but make 0 incomparable to all other elements.

• 1+2+4 doesn't imply 5 i.e. Co LT + Contra LT doesn't imply Contra Eq: consider any non-cancellative monoid, with the discrete partial order (any two elements incomparable).

(Diagram created using draw.io)

[alreadydone]

It turns out adding a single instance covariantClass_le_of_lt (which loops with LeftCancelSemigroup.covariant_mul_lt_of_covariant_mul_le) leads to a timeout in synthesizing CovariantClass (Fin 1) (Fin 1) (swap (· + ·)) (· ≤ ·). Before adding the instance, Lean 4 simply makes two attempts:

[Meta.synthInstance] [0.594885s] ❌ CovariantClass (Fin (0 + 1)) (Fin (0 + 1)) (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▼
  [] [0.395171s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
  [] [0.199529s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶

but after adding the instance, it makes 8 attempts with some repetitions (same instances applied to same goals multiple times):

[Meta.synthInstance] [0.987670s] ❌ CovariantClass (Fin (0 + 1)) (Fin (0 + 1)) (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▼
  [] [0.175717s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
  [] [0.088875s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
  [] [0.187840s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
  [] [0.084045s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
  [] [0.083262s] ❌ apply OrderedCancelAddCommMonoid.to_contravariantClass_left to ContravariantClass (Fin (0 + 1))
        (Fin (0 + 1)) (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x < x_1 ▶
  [] [0.184647s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
  [] [0.080370s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
  [] [0.087082s] ❌ apply @OrderedCancelAddCommMonoid.to_contravariantClass_le_left to ContravariantClass (Fin (0 + 1))
        (Fin (0 + 1)) (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶

(1/3/6th rows and 2/4/7th rows are the same, see this gist for the full relevant part of the trace) It's good that Lean 4 determined the infeasibility of synthesizing the instance in finite time and doesn't enter an infinite loop, but the significantly increased search time still means that this issue's proposal is doomed with the current state of Lean 4 typeclass inference.

[alreadydone]

It just came to my mind that the Lean 4 use of co(ntra)variant classes is different from Lean 3 in that it uses eta-expanded operations/relations like (· * ·) which is actually fun x y => x * y as you can see in the docs. In Lean 3 it's simply has_mul.mul which would translate to Mul.mul in Lean 4. Would that cause any performance issue by any chance? Arguably it's better to use Mul.mul etc. if only for more readable docs ...

[adomani]

I do not know about performance implications, but trying to use Mul.mul instead of (· * ·) and ibenching it would be a way to find out. I suspect that something will break with the change, but it can probably also be fixed!

For some reason, I suspect that HMul.hMul might be preferred to Mul, but I do not know whether this is really true or not...

On a similar note, should it also be LE.le/LT.lt/...?

[digama0]

Note that there is a PR open for this: https://github.com/leanprover/lean4/pull/2267 , it has some issues to work out though.

[adomani]

I went ahead and did a brute-force search and replace for the regexes: #6777. Let's see how it goes! EDIT: It passed building and it is linting!

[alreadydone]

Hmmm I think I finally found the right way to add commutation instances (previous failed attempt)! It appears that the @[inline] attribute on flip misled me: it is weaker than @[reducible] and flip doesn't get unfolded during instance search. The following instance works:

import Mathlib.Init.Algebra.Classes

variable {α : Type u} {β : Type v} (op : α → α → β)

instance IsSymmOp.flip 
    [IsSymmOp α β (fun x y => op y x)] : IsSymmOp α β op where
  symm_op := fun a b ↦ symm_op (op := fun x y => op y x) b a

example [IsSymmOp α β op] : IsSymmOp α β (fun x y => op y x) :=
  inferInstance /- surprising success! -/ 
/- This means it still works on unexpanded operations introduced by #6777 -/

example [IsSymmOp α β (fun x y => op y x)] : IsSymmOp α β (op · ·) := inferInstance /- success -/
example : IsSymmOp α β (fun x y => op y x) := inferInstance /- fails fast, no infinite loop! -/
example : IsSymmOp α β op := inferInstance /- fails fast -/
example : IsSymmOp α β (op · ·) := inferInstance /- fails fast -/

We could also introduce

abbrev flip2 {α β φ} (f : α → β → φ) (b a) := f a b -- or @[reducible] def

and use flip2 op in place of fun x y => op y x.

[YaelDillies]

As I went through the files I came across yet another variant mul_le_mul_iff_of_ge of eq_and_eq_of_le_of_le_of_mul_le which is simply its iff version, with a much simpler proof, so I just deleted the latter, and I'm about to change UniqueProds.lean to use the former.

Please do. I added it in hope of replacing eq_and_eq_of_le_of_le_of_mul_le but didn't actually do it.

[alreadydone]

It's done in #6677! In the PR description you'll see

• Generalize mul_eq_mul_iff_eq_and_eq and remove the less general Left/Right.mul_eq_mul_iff_eq_and_eq.
• Move mul_le_mul_iff_of_ge.

[alreadydone]

A correction: I just found that Function.swap is the one that is reducible (same in Lean 3) while flip is only inline but not reducible. This is partly due to my confusion / bad memory and partly due to mathlib4 docs not showing reducible attributes. I filed https://github.com/leanprover/doc-gen4/issues/144.

[alreadydone]

Given that swap is reducible, I don't quite understand why the following instance leads to timeouts (here I defined swap2 identically as swap but as an abbrev and it still doesn't work):

import Mathlib.Init.Algebra.Classes

universe u v u₃
variable {α : Type u} {β : Type v} (op : α → α → β)
abbrev swap2 {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : ∀ y x, φ x y := fun y x => f x y

instance IsSymmOp.flip 
    [IsSymmOp α β (swap2 op)] : IsSymmOp α β op where
  symm_op := fun a b ↦ symm_op (op := fun x y => op y x) b a

example : IsSymmOp α β (fun x y => op y x) := inferInstance
/-
failed to synthesize
  IsSymmOp α β fun x y ↦ op y x
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
-/

Is it that loop detection algorithm only checks duplications up to syntactic equality, even though unification during instance search looks through reducible defs?