grinding subsingletons

Stream: general

[Robin Carlier]

variable (C : Type) [Subsingleton C]

attribute [grind] Subsingleton

theorem foo (a b : C) : a = b := by
  grind -- fails

What would be the right pattern to get grind to work here? I’ve tried all variants of the [grind] attribute on Subsingleton.elim and various related subsingleton lemmas, but none seem to be working.

Note that grind reports

[issue] failed to create E-match local theorem for
        ∀ (a b : C), a = b

Is this worth escalating to a lean4 issue or is this user issue?

[Jovan Gerbscheid]

This works:

variable (C : Type) [Subsingleton C]

attribute [ext, grind ext] Subsingleton.elim

theorem foo (a b : C) : a = b := by
  grind -- succeeds

[Jovan Gerbscheid]

It seems @[grind ext] is not documented in the manual!?

[Robin Carlier]

Thanks!
It would be cool if grind ext was documented in the reference manual (to which subsystem of grind is it talking to?)

[Robin Carlier]

@Kim Morrison does adding ext to Subsingleton.elim and making grind ext seem like reasonable annotations to you? This looks like annotations that Core should make rather than Mathlib.

[Kyle Miller]

Subsingleton isn't cheap to always try (failures can take some time).

Mathlib has a FastSubsingleton class used by congr! and friends for that reason.

[Floris van Doorn]

I expect that could have serious performance issues. IIRC simp did a subsingleton check on every subterm, but that is also not the default anymore for performance reasons(?)

[Robin Carlier]

So better to make it [local grind ext] only where relevant?

[Robin Carlier]

Note that this came up when trying to use grind in CategoryTheory for things related to discrete categories or thin quivers. aesop_cat has no trouble using subsingletons instances but grind needs some help with those.

[Kim Morrison]

Yes, I think we add it as an aesop rule in the CategoryTheory ruleset.