Port Coq code to use done tactic instead of easy and benchmark

[palmskog]

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.

[ndcroos]

Hello, I'd like to work on this issue. Could you assign to to me please?

[palmskog]

@ndcroos in all but the most active projects, we don't really do GitHub assignments for issues. Typically, an OK from the maintainers (@spitters or @Lysxia) is enough. For example, it's probably not convenient to let the project depend directly on MathComp or Coq-Std++, so the done tactic would have to be copied over.

[ndcroos]

I will wait for an OK by the maintainers before doing anything.

There is also fast_done in Coq-Std++. https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/tactics.v?ref_type=heads#L45

(** [done] can get slow as it calls "trivial". [fast_done] can solve way less
goals, but it will also always finish quickly.  We do 'reflexivity' last because
for goals of the form ?x = y, if we have x = y in the context, we will typically
want to use the assumption and not reflexivity *)
Ltac fast_done :=
  solve
    [ eassumption
    | symmetry; eassumption
    | apply not_symmetry; eassumption
    | reflexivity ].
Tactic Notation "fast_by" tactic(tac) :=
  tac; fast_done.

The idea is to use fast_done where possible, and done where fast_done fails.

[spitters]

@ndcroos thanks. Please go ahead and do the environment as Karl suggests. it would be great if fast done could be used. from my phone

On Sat, Jul 27, 2024, 18:36 ndcroos @.***> wrote:

There is also fast_done in Coq-Std++

https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/tactics.v?ref_type=heads#L45

(* [done] can get slow as it calls "trivial". [fast_done] can solve way less goals, but it will also always finish quickly. We do 'reflexivity' last because for goals of the form ?x = y, if we have x = y in the context, we will typically want to use the assumption and not reflexivity ) Ltac fast_done := solve [ eassumption | symmetry; eassumption | apply not_symmetry; eassumption | reflexivity ]. Tactic Notation "fast_by" tactic(tac) := tac; fast_done.

The idea is to use fast_done where possible, and done where fast_done fails.

— Reply to this email directly, view it on GitHub https://github.com/coq-community/math-classes/issues/128#issuecomment-2254195046, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTWXZR3TBXBY6ECV6GTZOPD73AVCNFSM6AAAAABKSOQQ6CVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENJUGE4TKMBUGY . You are receiving this because you were mentioned.Message ID: @.***>