coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Familiarity with eauto implementation

From: Gregory Malecha <gmalecha AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Familiarity with eauto implementation
Date: Wed, 4 Dec 2019 04:45:00 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f42.google.com
Ironport-phdr: 9a23:lvh6Mh36YfB47j5xsmDT+DRfVm0co7zxezQtwd8ZseISI/ad9pjvdHbS+e9qxAeQG9mCsLQd1Lud6/2ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTSwbalvIBi0qQjdudUajIt/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTlkzkMOSIn/27Li8xwlKNbrwynpxxj2I7ffYWZOONjcq/BYd8WQGxMUcFMWSxcGYO8d5UAAPYdPehWqIn9okEBrRq4BQKxAO/ixTtFinrw0KYn0eouDBvG0RQvENwOvnrar8j7OrkOXu2u1qbE0S/OYulK1Tvh6oXFdA0qr/GWXbJ3dMrc0UghFxnbgVWfrozlJTOU3fkKvWeB6+pvS/6gi249pApspTWvycIshZPNho0L1l/E9T92zZ06Jd29UkF7YNqkHIFMuCGdMot7W8UvSHxmtiY9z70Jo5+7fC4SxZQoxh7fd/yHc5WT7R75VeaRJi90hH1keLKjhxay7FOvxvfgWcmz1VZHqDdOnNrUtn0VyRDf9syKRuF+80qhwzqDyR7f5vxeLU07i6bWLYMqzKQqmZoJq0vDGzf7mEXog6+ScUUp4u2o5P7mYrXiv5OdOZV0hhznPqQglcGzH/40MgcJX2ic9uS80KPs8VflT7VNi/06iqjZsJbEKsQHvqO1HRNZ34I55xu8DzqqysoUkWcaIF5fdx+LkZDlO1TUL/D5Cfe/jU6skDBux/3eMb3hB4/CLnzdn7j9fbZy8VVRyAU2zd9F5pJUDqsNL+70Wk/0rNDYFAM2MxSow+b7D9Vwzp8RWWWWAqOALKzStUKI6fk0LumXZI4VvS79JOI/6/7vi385g14dcrOz0ZsZcnDrVshhdm6eeDLHhsoLWTMBuRN7R+j3gnWDVyRSbjC8RfRvyCs8DdeJF4rMQZq8yJmI2CqwHpQeMm9DA1SBGnfhX4qBUvYILimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8ic7ONq38o8Kn73d0w3NX90BQ79Dh6FcOYijjfQGR9n2dOTDgzjvkm/B5Nj2yb2K09uMR2UNxe4/QTD1U/PJ/YivNgUpX8BliHcdCOR1KrBN6hBGNpF45j85o1e094Xu6aoFXbxSPzWu0akrWKANo/9aeOh3U=

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

[Coq-Club] Familiarity with eauto implementation, Gregory Malecha, 12/04/2019
- Re: [Coq-Club] Familiarity with eauto implementation, Théo Zimmermann, 12/04/2019
  - Re: [Coq-Club] Familiarity with eauto implementation, Gregory Malecha, 12/05/2019