coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Is eauto behavior desirable?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Is eauto behavior desirable?
Date: Thu, 15 Sep 2016 13:51:54 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga02.intel.com
Ironport-phdr: 9a23:AOInTx9zwZhwmP9uRHKM819IXTAuvvDOBiVQ1KB92+McTK2v8tzYMVDF4r011RmSDNydtK8P1bee8/i5HzdRudDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvjotuMPk4W2XL9Oeo0d0Tu612J94E/ushLEu4J0BzHo39FKax95FhDAhatpSv6/dq655V58i5d6LoL/s9EVrjmLexjFeQLRGduD2dgrsbsrFzISRaFznoaSGQf1BRSSUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3pZxsRRD0kiAfc3Yc8WrXg8F0xuoPpROqpxVyx8jPZ4yaKOB5Zovce88XQSxKWcMHBH8JOZ+1c4ZaV7lJBu1ftYSo/1Y=

Dear Coq Users,

as far as I can tell (it is not documented) eauto will execute any hint first, which solves the goal, regardless of priority in the database. This has the undesirable effect that eauto first checks all hints if they would solve the goal, even expensive ones. I tend to give priorities to extern hints such that expensive tactics are tried last, but this has no effect, if all tactics are tried before any tactic is executed.

I wonder how other uses see this. Do you think it is a great feature of eauto or not?

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
  - RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/15/2016
    - Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
      - Re: [Coq-Club] Is eauto behavior desirable?, Matthieu Sozeau, 09/15/2016
        
        Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
        
        Re: [Coq-Club] Is eauto behavior desirable?, Matthieu Sozeau, 09/15/2016
        
        Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
        Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/19/2016
        RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/20/2016
        
        RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/16/2016