subsingleton tactic #12525

Stream: PR reviews

[Kyle Miller]

I made a tactic called subsingleton in #12525 that proves equalities using some sort of subsingleton argument. It's like intro; apply Subsingleton.elim, but it has a couple other features, like you can give it instances with subsingleton [inst]. This is an improvement to have := inst; subsingleton since inst might be universe polymorphic and it might have unsolved placeholders (so it saves you from giving type ascriptions).

Another thing is that subsingleton can be used places where types are morally subsingletons, like BEq instances that have LawfulBEq instances. This is useful when there are inescapable diamonds.

I've been fixing merge conflicts for this PR a couple times a week for the last month, and it would be nice to get eyes on it.

[Yaël Dillies]

Question without having looked at the PR: Can this be interfaced with nontriviality? Could it be used to discharge the subsingleton case created by nontriviality?

[Kyle Miller]

I haven't given that any thought. Does nontriviality prove equalities in the Subsingleton branch?

The main application I had in mind was congr! <;> subsingleton to discharge side goals now that congr! uses the FastSubsingleton typeclass.

[Yaël Dillies]

Yes, it does. I believe that currently all it uses in the subsingleton branch is some configured simp call

[Jireh Loreaux]

But of course, nontriviality does more than just equalities.