The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Thanks, Theo!

On Wed, Dec 4, 2019 at 5:22 AM Théo Zimmermann <theo.zimmi AT gmail.com> wrote:

Hi Gregory,

There is a well-known (or maybe not so well-known) trick that allows
using eauto in "forward mode" (apply a lemma and then stop), which is
to use it in combination with shelve and unshelve. I mention this
briefly in this document:
https://hal.archives-ouvertes.fr/hal-01671994/document.

During the 2018 Coq Implementors Workshop, we worked with Michael and
Armaël at improving the support for this kind of forward reasoning
mode, in particular with the (still unfinished) PR
https://github.com/coq/coq/pull/7661 (both Armaël and I are defending
our PhD theses soon, so that might explain the lingering state).

None of this information is given to discourage you working on your
project plugin though. I didn't take the time to look at your code
just yet, but I'd advise that you avoid "eauto.mli" and rather look at
what is available in "class_tactics.mli", in particular the
"autoapply" function, as there are plans to remove the (old)
implementation of "eauto" in favor of the one of "typeclasses eauto"
(while keeping compatibility as much as possible, cf.
https://github.com/coq/coq/pull/721).

Sorry for not taking more time to answer more properly.

Théo

Le mer. 4 déc. 2019 à 10:45, Gregory Malecha <gmalecha AT gmail.com> a écrit :
>
> Hello --
>
> I'm working on a plugin that uses hint databases (and discrimination trees) to apply any of a collection of lemmas (or external tactics). I don't believe this functionality exists, but please correct me if I am wrong. Essentially
>
> Hint Resolve lem1 lem2 : hint_db.
> Hint Extern 0 (f _ _) => tac : hint_db.
> apply_any hint_db
>
> should act like (order is not important)
>
> eapply lem1 + eapply lem2 + tac + fail "no lemma applies"
>
> I've come up with a simple skeleton of this: https://github.com/gmalecha/coq-apply-any
> The function that I'm not sure how to implement is: https://github.com/gmalecha/coq-apply-any/blob/master/src/apply_any.ml#L1
> I was expecting that a function like this would be exported from eauto.mli, but my readings over that code seem like that might not be the case. Can someone with more familiarity with that code suggest where to look?
>
> Thanks.
>
> --
> gregory malecha
> gmalecha.github.io

--

gregory malecha

gmalecha.github.io