RFC: swap the order of the arguments to Membership.mem

[mattrobball]

Proposal

The current definition of Membership is

class Membership (α : outParam (Type u)) (γ : Type v) where
  mem : α → γ → Prop

We propose to change it to

class Membership (α : outParam (Type u)) (γ : Type v) where
  mem : γ → α → Prop

Why?

As pointed out by @digama0, when elaborated, instances on subtypes need an insertion of a .lam for the coercion. With the current ordering, this lambda does not satisfy etaExpandStrict?.isSome at reducible transparency since the initial application is not to the bound variable of the lambda in the body.

As a result, the discrimination tree keys for any such instance will be weaker than necessary and will match too much. For

import Mathlib

open Lean Meta Elab DiscrTree

instance bar (G : Type*) [Group G] [Fintype G] : Fintype (⊤ : Subgroup G) := sorry

run_meta do 
  withReducible do
  let info ← getConstInfo `bar
  let x := info.type
  let (_, _, type) ← forallMetaTelescopeReducing x
  let keys ← mkPath type tcDtConfig 
  logInfo m!"{keys}"

variable {G : Type*} [Group G] [Fintype G] 

set_option trace.Meta.synthInstance true in
#synth Fintype (⊤ : Subgroup G)

The instances below all match.

[instances] #[@SetLike.instFintype, @FinEnum.instFintype, @Set.fintypeInsert', @IsSimpleOrder.instFintypeOfDecidableEq, @Unique.fintype, @CategoryTheory.FinCategory.fintypeObj, @NonemptyFiniteLinearOrder.toFintype, @Subtype.fintype, @Fintype.subtypeEq, @Finset.fintypeCoeSort, @List.Subtype.fintype, @Multiset.Subtype.fintype, @Finset.Subtype.fintype, @FinsetCoe.fintype, @Set.fintypeUniv, @Set.fintypeUnion, @Set.fintypeSep, @Set.fintypeInter, @Set.fintypeInterOfLeft, @Set.fintypeInterOfRight, @Set.fintypeDiff, @Set.fintypeDiffLeft, @Set.fintypeiUnion, @Set.fintypesUnion, @Set.fintypeBiUnion', @Set.fintypeBind', @Set.fintypeEmpty, @Set.fintypeSingleton, @Set.fintypePure, @Set.fintypeInsert, @Set.fintypeImage, @Set.fintypeRange, @Set.fintypeMap, @Set.fintypeImage2, @Set.fintypeSeq, @Set.fintypeSeq', @Set.fintypeMemFinset, @Submonoid.fintypePowers, @AddSubmonoid.fintypeMultiples, @RingHom.fintypeRangeS, @RingHom.fintypeRange, @Set.fintypeIcc, @Set.fintypeIco, @Set.fintypeIoc, @Set.fintypeIoo, @Set.fintypeIci, @Set.fintypeIoi, @Set.fintypeIic, @Set.fintypeIio, @Set.fintypeUIcc, @LinearMap.fintypeRange, @NonUnitalRingHom.fintypeRange, @NonUnitalAlgHom.fintypeRange, @AlgHom.fintypeRange, @Subgroup.instFintypeSubtypeMemOfDecidablePred, @AddSubgroup.instFintypeSubtypeMemOfDecidablePred, @Subgroup.fintypeBot, @AddSubgroup.fintypeBot, @MonoidHom.fintypeMrange, @AddMonoidHom.fintypeMrange, @MonoidHom.fintypeRange, @AddMonoidHom.fintypeRange, @conjugatesOf.fintype, @ConjClasses.instFintypeElemCarrier, @Polynomial.rootSetFintype, @IsNoetherian.instFintypeElemOfVectorSpaceIndex, @FiniteDimensional.instFintypeElemOfVectorSpaceIndex, @RingHom.fintypeFieldRange, @SimpleGraph.neighborSetFintype, @SimpleGraph.Subgraph.finiteAt, @SimpleGraph.Subgraph.instFintypeElemNeighborSetOfVertsOfDecidablePredMemSet, @instFintypeElemImageToSetOfDecidableEqOfSingletonSet, bar, inst✝]

because the keys are [Fintype, Subtype, *, ◾]

After swapping the order, we only match

#[@SetLike.instFintype, @FinEnum.instFintype, @IsSimpleOrder.instFintypeOfDecidableEq, @Unique.fintype, @CategoryTheory.FinCategory.fintypeObj, @NonemptyFiniteLinearOrder.toFintype, @Subtype.fintype, @Subgroup.instFintypeSubtypeMemOfDecidablePred, bar, inst✝]

because the keys for the goal are [Fintype, Subtype, *, Membership.mem, *, Subgroup, *, *, *, Top.top, Subgroup, *, *, *] and the keys all instances in Fintype instances on subtypes are more robust.

Additionally, the reordering is more pleasant for the identification of sets with predicates.

Community Feedback

This was discussed here after multiple cases of slow instance synthesis for subobjects, including explicit workarounds to avoid the coercion.

It speeds up building of mathlib by ~2% and linting by ~5%. See leanprover-community/mathlib4#15457 for a sorryed branch of mathlib with this implemented.

Impact

The positive impact was discussed above. The negative impact is that mathlib seems to rely a bit too much on the weak keys at some places to synthesize instances. Indeed, the example fails without bar on the new branch. A decent amount of cleanup will be required.

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[mattrobball]

Note: ~2% of the keys in Mathlib are of the form #[.const _ _, .const `Subtype _, .star, .other].

[mattrobball]

And ~3% of the keys are of the form #[.const _ _, .const `Subtype _, .star, .other] ++ mkArray .star n for some n : Nat.

[TwoFX]

Hi @mattrobball, as far as I understand the 2% build speedup is on the sorryed branch. Do you know how much of the speedup is due to the better keys as opposed to having to check fewer proofs?

[mattrobball]

Given that there is such a large decrease in typeclass synthesis, I would be surprised if it is substantially due to the sorry's but I can revert the toolchain and run a benchmark for comparison if that would be helpful

[TwoFX]

@mattrobball Yes, that would be very helpful, thank you.

[mattrobball]

Comparison from v4.10.0 to modified toolchain (which is branched off v.4.10.0).

[kim-em]

@mattrobball, do you have an estimate of how much work is required to fix Mathlib?

[mattrobball]

Maybe in the neighborhood of unbundling FunLike would be my guess. To get a sense of the failures, there is one test here in core, which I think you made, about IntermediateField timeouts which is upside-down with this change.

[TwoFX]

Hi @mattrobball, thank you for investigating this issue. The numbers and the reasoning are solid and we would like to see this change happen, so we are accepting the RFC.

Getting a corresponding PR merged would be conditional on having a mathlib adaptation PR ready. Adapting mathlib seems to be quite a lot of work, and the FRO does not have enough capacity at the moment to perform the adaptation in a timely manner. We would be very happy about a community-led effort to adapt mathlib and would help where we can. To phrase it in terms of our new priority labels, we would treat a PR for this RFC with priority P-medium.

[mattrobball]

@TwoFX, very understandable. I will have to start teaching again next week so also cannot commit to any timeline for a working version of mathlib. I'll bring this up on Zulip to see if others might be willing to assist.

PS: you might want to adjust the priority label to avoid confusion.

[TwoFX]

This was completed in #5020.