Performance issues with Function.Injective.$typeclass

Stream: mathlib4

[Ruben Van de Velde]

Eric Wieser said:

(docs#Function.injective.addCommGroup etc)

I thought we needed to avoid those for reasons I don't understand

[Eric Wieser]

For now I think it's better to use them and take a performance hit rather than do a whole lot more work at each call site; I think there's a best-of-both-worlds solution that unfold those functions at elaboration time

[Matthew Ballard]

The issue is that for all Function.Injective/Surjective typeclass constructors expose too much data to unification. Because you have a copy of each operation on the source and the target as parameters to the function, Lean has to check the data at each call site.

You can

1. Rip these out at the call site and do things by hand #10617.
2. Make constructors that don't expose the data by taking the appropriate parent classes as parameters. Eg. take [CommMonoid B] and [Monoid A] for f : A \to B injective if you want a CommMonoid A. #11029

They each result in the same performance gain (~1.5%) overall with the benefit concentrated in areas that heavily use subobjects.

The disadvantage of 1 is that maintainability goes out the window. The disadvantage of 2 is that preferred parents are a choice and you might want another choice so might need multiple versions of these depending on inheritance.

I got distracted by the question of what the preferred parent should actually be for instead of polishing this...

[Eric Wieser]

The best-of-both-worlds solution is a metaprogram that does 1, taking the status quo as input

[Eric Wieser]

Here's a prototype of that metaprogram:

import Mathlib.GroupTheory.Subgroup.Basic

open Lean Meta

elab "optimize_inst%" arg:term : term <= expectedType => do
  let .some className ← Lean.Meta.isClass? expectedType |
    throwError "Can only be used for classes"
  let ctor := Lean.getStructureCtor (← getEnv) className
  Lean.logInfo m!"{ctor.numParams} {ctor.numFields}"
  let provided ← Lean.Elab.Term.elabTerm arg (some expectedType)
  -- create universe variables
  let levels ← Meta.mkFreshLevelMVarsFor (.ctorInfo ctor)
  let mut e := Expr.const ctor.name levels
  -- get argument types
  let (mvars, binders, _body_) ← forallMetaTelescope (←inferType e)
  e := mkAppN e mvars
  guard (← isDefEq (←inferType e) expectedType)
  e ← instantiateMVars e
  -- substitute parent classes with direct instances, if possible
  for arg in mvars.extract ctor.numParams (ctor.numParams + ctor.numFields),
      bi in binders.extract ctor.numParams (ctor.numParams + ctor.numFields) do
    if let .instImplicit := bi then
      if let .some new_arg ← trySynthInstance (←inferType arg) then
        arg.mvarId!.assign new_arg
        Lean.logInfo m!"{arg} ← {new_arg}"
        e ← instantiateMVars e
  -- must be defeq to what the user passed
  if !(← isDefEq provided e) then
    Lean.logError "Not defeq"
  pure e

variable {G} [CommGroup G] (H : Subgroup G)

-- pretend we are running before these exist
attribute [-instance] Subgroup.toCommGroup SubgroupClass.toCommGroup

instance (priority := 75) foo : CommGroup H :=
  optimize_inst%
    Subtype.coe_injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
      (fun _ _ => rfl) fun _ _ => rfl

/--
info: def foo.{u_1} : {G : Type u_1} → [inst : CommGroup G] → (H : @Subgroup G (@CommGroup.toGroup G inst)) → CommGroup ↥H :=
fun {G} [inst : CommGroup G] H ↦ @CommGroup.mk (↥H) (@Subgroup.toGroup G (@CommGroup.toGroup G inst) H) ⋯
-/
#guard_msgs in
set_option pp.explicit true in
#print foo

[Matthew Ballard]

Great! I think that is a good start. Let me play dumb. What is the advantage of the current design?

[Matthew Ballard]

Matthew Ballard said:

Great! I think that is a good start. Let me play dumb. What is the advantage of the current design?

This kinda got lost. I think it would be a good guide for any final optimize_inst%

[Matthew Ballard]

The main way I've seen it used is that people build the data classes and then just go for the jugular and define say a Field using Function.Injective.field

[Yaël Dillies]

It didn't get lost but it was feeling a bit shunning to say "There's none" :grinning:

[Matthew Ballard]

I think Eric's idea is useful well beyond this case. But it should apply to all structures and back propagate to make the parents

[Eric Wieser]

What are you referring to by "current design"; the pattern of using Function.Injective.foo?

[Matthew Ballard]

The statement also

[Eric Wieser]

The statement of what?

[Eric Wieser]

The idea of the pattern is

• You have to construct most of the data fields yourself anyway; they typically amount to showing closure of your property. If you don't construct all of them, you get bad defeqs (things like coe_sub are not then dsimp lemmas)
• You don't want to do any proofs about the algebraic structure; the statement is just "well obviously it inherits the structure, all the operators are the same".

[Eric Wieser]

The other consideration is:

• The order of type class parents is an implementation detail that you the mathematician never want to have to even know exists

[Eric Wieser]

I've PR'd the above at #11521

[Notification Bot]

28 messages were moved here from #mathlib4 > Instance diamond in Equiv.TransferInstance by Eric Wieser.

[Eric Wieser]

(for small values of 28)

[Junyan Xu]

I'm adding the whole hierarchy of algebraic instances for DirectLimit in #19772, and I think it might benefit from your PR, which probably also solves the other issue that sometimes some data field available in ancestor instances are not picked up in descendent instances, resulting in those fields being filled by npowRec etc. causing a diamond. It took me some effort to locate a diamond that reports the Semiring and Field instances are not the same, which turned out to be due to the Semiring instance not picking up npow from Monoid. Before your PR is merged, is there a way to ensure that data fields don't get automatically get filled by automation? I recall this question being asked on Zulip sometime ago, but I don't remember the keywords to find the discussion.