assumeInstancesCommute / assertInstancesCommute

Stream: metaprogramming / tactics

[Floris van Doorn]

Is there documentation about assumeInstancesCommute / assertInstancesCommute somewhere?
Why is this line needed, and not done by the assumeInstancesCommute on the next line? (it's adding the equation «$mα» =Q «$inst».toNonAssocSemiring.toAddCommMonoidWithOne.toAddMonoidWithOne)
Does assertInstancesCommute only add defeqs for type-class instances of the same type? (If so: what does the word "commute" signify?)

Reason for asking: @Pan Lin and I just ran into a similar situation where we had to add _ =Q _ line as well (we're making positivity more general, but that might require adding _ =Q _ lines in many places).

[Eric Wieser]

Floris van Doorn said:

Does assertInstancesCommute only add defeqs for type-class instances of the same type?

No, since one of its most common uses is to demonstrate that a synthesized LinearOrder is compatible with the PartialOrder passed to positivity extensions

[Eric Wieser]

My guess is that that line is needed because otherwise Qq only assumes that ma and ma' are equal, without finding the third instance

[Floris van Doorn]

The failure that Pan and I was precisely the case where we had 1 LinearOrder instance and 2 PartialOrder instances in a positivity extension, but assumeInstancesCommute didn't unify them all.
Maybe @Pan Lin can create a #mwe? (It's a bit tricky since it's on top of a modified version of positivity)

[Eric Wieser]

Here's a mwe:

import Mathlib

structure Foo {α : Type} (i : PartialOrder α) : Type

variable [i1 : PartialOrder α] [i2 : PartialOrder α] [i3 : LinearOrder α]
variable (x : Foo i1) (y : Foo i2) (z : Foo i3.toPartialOrder)

open Qq
#check by_elabq do
  assumeInstancesCommute
  return q($x = $y ∧ $y = $z ∧ $x = $z)

[Floris van Doorn]

Yes, that seems to reproduce exactly the issue we ran into. If you replace the variable lines by

variable [i1 : PartialOrder α] [i3 : LinearOrder α]
variable (x : Foo i1) (y : Foo i1) (z : Foo i3.toPartialOrder)

then it works correctly.