coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [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: RE: [Coq-Club] Is eauto behavior desirable?
Date: Fri, 16 Sep 2016 08:10:47 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.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 mga01.intel.com
Ironport-phdr: 9a23:RsYA+BLDcyvH+r7t6tmcpTZWNBhigK39O0sv0rFitYgUKvvxwZ3uMQTl6Ol3ixeRBMOAuqsC1LSd6vqwESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9ScbuiJH93OervpbXfg9ghTynYLo0Ig/85VHasdBTio9/II4wzAHIqz1GYbIF63lvIAfZpBHx6duq+4YnuwFRsPIo+soKGfH/fq84RLFcSi8hPm8p/srznRjFUQaLoHAbVzNFwVJzHwHZ4USiDd/KuSzgu78l1Q==

Dear Jonathan,

> It's not just bad for performance. There are occasions where one has
> multiple subgoals with evar interdependencies such that one cannot accept
> just any arbitrary solution to one of the subgoals, as that solution might
> prevent solutions in the other(s).

Indeed, I have cases where some tactic creates a special hint hypothesis
which enables other tactics, so that I make sure that the second tactic
doesn't run before the first one. It would be easier if eauto would stick to
the priorities given.

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

Re: [Coq-Club] Is eauto behavior desirable?, (continued)
- 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
      - RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/16/2016