Math Classes currently uses the easy tactic from Coq's standard library as a finisher tactic to close a goal. However, easy is known to be slow, most directly because it uses inversion. For example, it can be slow when there are inductives with many constructors in the proof context.
An alternative to easy is the done tactic from Coq-Std++, which does not use inversion, and incorporates best practices from the MathComp done tactic. Math Classes could likely benefit from being ported to use done instead of easy, which would be a good project for a first-time contributor. There should be benchmarks with and without done to measure the improvements.
The port should not necessarily make Math Classes depend on Coq-Std++, but could bundle the done tactic.
Math Classes currently uses the
easytactic from Coq's standard library as a finisher tactic to close a goal. However,easyis known to be slow, most directly because it usesinversion. For example, it can be slow when there are inductives with many constructors in the proof context.An alternative to
easyis thedonetactic from Coq-Std++, which does not useinversion, and incorporates best practices from the MathCompdonetactic. Math Classes could likely benefit from being ported to usedoneinstead ofeasy, which would be a good project for a first-time contributor. There should be benchmarks with and withoutdoneto measure the improvements.The port should not necessarily make Math Classes depend on Coq-Std++, but could bundle the
donetactic.