specificity of grind patterns

Stream: mathlib4

[Lawrence Wu (llllvvuu)]

How should I be thinking about whether a grind pattern is specific enough?

I am working with finsets right now but I see

[grind.ematch] activated `Multiset.notMem_zero`, [@Membership.mem #1 _ _ (@OfNat.ofNat _ `[0] _) #0]
[grind.ematch] activated `Set.mem_insert_iff`, [@Membership.mem #3 _ _ (@insert _ _ _ #1 #0) #2]
[grind.ematch] activated `Set.subset_insert`, [@insert #2 _ _ #1 #0]
[grind.ematch] activated `Multiset.mem_add`, [@Membership.mem #3 _ _ (@HAdd.hAdd _ _ _ _ #1 #0) #2]

looks like those do not have Multiset or Set anywhere in the pattern. Is that OK? And how does grind determine to put Set / Multiset in the pattern vs not?

[Lawrence Wu (llllvvuu)]

So those only cost my theorem 9 heartbeats, but in contrast I put a grind annotation I thought was reasonable (docs#Finsupp.mem_support_iff, which yielded the innocuous-looking-to-me grind pattern [@Membership.mem #4 (Finset _) _ (@support _ #3 #2 #1) #0]) and it blew up some theorems, like docs#MonoidAlgebra.support_single_mul_eq_image from 1340 to 3874 heartbeats, with the main changes in the trace.grind.debug output being things like

    #54 := Lean.Grind.IntModule.OfNatModule.Q #7 #55
    #55 := AddCommMonoid.toGrindNatModule #7 #56
    #56 := @NonUnitalNonAssocSemiring.toAddCommMonoid #7 #11
    #57 := @Lean.Grind.AddCommMonoid.toZero #54 #58
    #58 := @Lean.Grind.NatModule.toAddCommMonoid #54 #59
    #59 := @Lean.Grind.IntModule.toNatModule #54 #60
    #60 := @Lean.Grind.IntModule.OfNatModule.ofNatModule #7 #55

Is there a way I can get better at predicting these things?

[Lawrence Wu (llllvvuu)]

Interestingly, the generated patterns are different for Set and Finsets:

#print Set.mem_insert_iff
-- @Membership.mem α (Set α) Set.instMembership (insert a s) x
#print Finset.mem_insert
-- @Membership.mem α (Finset α) Finset.instMembership (insert b s) a
attribute [grind? =] Set.mem_insert_iff
-- Set.mem_insert_iff: [@Membership.mem #3 _ _ (@insert _ _ _ #1 #0) #2]
attribute [grind? =] Finset.mem_insert
-- Finset.mem_insert: [@Membership.mem #4 (Finset _) _ (@insert _ (Finset _) _ #0 #2) #1]

What are the rules for which implicit parameters get into the grind pattern? I couldn't find that in the reference manual

[Jovan Gerbscheid]

Oh, could it be that grind is unfolding Set α, into α → Prop?

[Wrenna Robson]

Good argument for packaging that into a struct...

[Jovan Gerbscheid]

That refactor is going to be a nightmare though

[Jovan Gerbscheid]

I suppose for similar reasons it is having trouble with

def Multiset (α : Type u) : Type u := Quotient (List.isSetoid α)