Decidability instances with long hypotheses

Stream: mathlib4

[Alex Meiburg]

What is the purpose of instances like
docs#instDecidableMonotoneOnOfForallForallMemSetForallForallForallLe ?

I assume that it matters for something, but it's not clear to me what or how. Of course I could just delete it and rebuild and see what breaks, but I figured someone here could probably explain better. (Would any such explanation belong in a docstring, too, maybe?)

[Eric Wieser]

It lets Decidable synthesis unfold the defition of MonotoneOn

[Alex Meiburg]

Oh, right, I see, ok. Wait, so should essentially every (reasonably computable) Prop have a similar "unfolding instance"? I mean, probably not, but I'm curious what the guidelines would be.

e.g. docs#IsLinearMap could easily have a similar instance, which would work fine as long as R/M/M₂ are all finite

[Alex Meiburg]

(Maybe a more silly + obscure one would be Module.Baer )

[Eric Wieser]

I think probably the rule is add the instance only if you can come up with an example where it would apply

[Eric Wieser]

Maybe we should have a library note for these

[Alex Meiburg]

"would apply" as in "the unfolded definition could be decidable", or "would apply" as in "someone would need it"?

Like Module.Baer is decidable given a Fintype R and Fintype Q, but I don't expect anyone using that in a decide tactic any time soon. But IsLinearMap I could definitely see (if someone is giving some explicit description of a linear map over some small funny finite structure)

[Alex Meiburg]

I'm interested because I have a little pool of decidability + fintype instances I've actually got laying around on a branch somewhere, but sometimes I'm not sure when they're wanted/welcome and in what form

[Eric Wieser]

"someone would need it", but that could be you. Maybe a good proxy is "you can provide a test file that shows it's useful, even if just for a demo"