coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is eauto behavior desirable?

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is eauto behavior desirable?
Date: Thu, 15 Sep 2016 17:15:13 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f50.google.com
Ironport-phdr: 9a23:j773SBP4D9exiTd3asEl6mtUPXoX/o7sNwtQ0KIMzox0KPn9rarrMEGX3/hxlliBBdydsKMdzbWL+Pm4ACRAuc/H6yFaNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbtr8FoOatcmrzef6o8SVOFQRwmXgKuoqdV329VyX7ZhOx9M6a+4Y8VjgmjNwYeNYxGdldxq4vi3XwYOOxqNl6DlaoPk79sRNAu3QdqU8SqFEXnx9azhmrJ6jiR6WRgyWo3AYT28+kxxSAgGD4gupcI32t37fv/Zh2CiXIIXNSqI5UCnqu6JiVAPhjQ8CPiIl+WSRjdZ/2vEI6Cm9rgByltaHKLqeM+BzK/vQ

typeclasses eauto with db does not use the typeclass_instances db.

On Thu, Sep 15, 2016 at 7:11 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 09/15/2016 01:02 PM, Matthieu Sozeau wrote:
> 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

Ah - yet another hidden difference between proof search tactics!

So, Michael should just do "typeclasses eauto with core" or whatever db,
unless he doesn't want typeclass instances in his search.

Is there a way to use typeclasses eauto without using the
typeclass_instances db?

-- Jonathan

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