The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Matthieu,

 

maybe I should switch to typeclass eauto. The only downside is that the search depth can only be specified in a vernacular command, not in a tactic. Well I am not sure how much of an issue this really is. I think I have only very few cases, where the trace gets larger when increasing the search depth, and there are likely ways to fix it.

 

I am not sure that it would be so difficult to fix eauto. I think one could use pretty much the same algorithm, but do it priority level by priority level.

 

Best regards,

 

Michael

 

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Matthieu Sozeau
Sent: Thursday, September 15, 2016 7:03 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is eauto behavior desirable?

 

Hi Michael,

Indeed, that's a difference between eauto which executes all tactics then lexicographically order them according to priority and number of subgoals created, and typeclasses eauto which trusts the priorities to execute the tactics in the order so specified. It's not such an easy fix of eauto sadly and probably an incompatible change in some cases...
Best,
-- Matthieu

On Thu, 15 Sep 2016 at 16:58, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 09/15/2016 10:42 AM, Soegtrop, Michael wrote:
> Dear Jonathan,
>
>> It wasn't until recently in 8.5 that eauto took the hint costs into consideration at
>> all - it was previously trying hints in most-recent-first order regardless of cost.
>> Yet few noticed.
> I know, I reported the bug.
>
> I guess also taking into account that this change didn't break a lot of developments, this means that few people are using eauto for non-trivial stuff. So I wonder if one could change this behavior as well. I think it is really bad for performance.
>
>

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).  This was the case I
was getting into when I noticed that eauto wasn't respecting hint costs,
as I was trying to carefully arrange hints so that those that solved
subgoals without instantiating "side" evars (hence not interfering with
other subgoals) were given lower costs and so tried first.

I think that although many people are using (e)auto, few are probably
doing so in a way such that the order of hints makes a noticeable
difference.

-- Jonathan

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