Can we have anonymous "instance" with assumptions?

Stream: CSLib

[Ching-Tsun Chou]

I have an instance of a class which needs an assumption:
https://github.com/ctchou/cslib/blob/5279f4467d8e89f01625809d131b8a5a56784034/Cslib/Computability/Automata/NA/Loop.lean#L182
Is it possible to use an anonymous instance here? I've tried it but it doesn't seem to work. First, instance inference fails. Then I added an explicit proof of the instance in a context where the assumption holds:

  have : na.finLoop.Total := by grind

Now instance inference works, but lake lint complains:

/- The impossibleInstance linter reports:
SOME INSTANCES HAVE ARGUMENTS THAT ARE IMPOSSIBLE TO INFER
These are arguments that are not instance-implicit and do not appear in
another instance-implicit argument or the return type. -/
-- Cslib.Computability.Automata.NA.Loop
/Users/ctchou/play/cslib-2/Cslib/Computability/Automata/NA/Loop.lean:181:1: error: @Cslib.Automata.NA.FinAcc.instTotalSumUnitFinLoopOfExistsMemSetStart argument 4 h : ∃
s0, s0 ∈ na.start

What is the best practice here?

[Kyle Miller]

Have you seen the docs#Fact class in Mathlib? This is a technique for injecting hypotheses into the typeclass system. It's intended for local instances (sometimes there's a case for a global instance, but these should be treated with suspicion).

A variant is to make a custom typeclass for just this hypothesis. This is often nicer since it doesn't require thinking about a global/general design.

In particular, it looks like your conditional instance is about whether na.start is nonempty. Any reason not to use the Nonempty class?

[Chris Henson]

Can you confirm that is the correct commit that triggers the linter? I tried checking out that commit and was not able to reproduce.

[Ching-Tsun Chou]

@Chris Henson The commit I gave does not have the lint error, which is triggered if you make the instance anonymous.
@Kyle Miller I'll look into what you wrote and get back to you.

[Ching-Tsun Chou]

I decided to use the Fact mechanism:
https://github.com/ctchou/cslib/blob/1a6d35afec5a09d0d526ac10f6ac97b8be28ecce/Cslib/Computability/Automata/NA/Loop.lean#L182
See also lines 196-199 of the same file. LTS.Total.mTr_ωTr on line 199 is where the Fact from line 196 is used.

[Chris Henson]

Just to unify with the conversation on GitHub, note this is in cslib#241 where I had left a comment.

[Ching-Tsun Chou]

Just an update to make this thread self-contained: @Kyle Miller and @Chris Henson pointed out that the Set.Nonempty assumption I need to make can be converted to an Nonempty assumption and hence can be handled by the instance inference mechanism itself. See cslib#241 for details.