coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is eauto behavior desirable?
Date: Thu, 15 Sep 2016 13:11:22 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f182.google.com
Ironport-phdr: 9a23:V9us0hTOYk07h/Yq2zJ0vrXcWNpsv+yvbD5Q0YIujvd0So/mwa67YxGN2/xhgRfzUJnB7Loc0qyN4vmmBjFLuM7Y+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/hKiO/MjYZBwNjz6ga5tzKg+3pEPfrJo4m4xnf4Q2zBLVonJOM8BbxH1lI07byxT74Maz8Zpu/gxfvvsg84hLVqCsLPdwdqBREDlzazN938bsrxSWFQY=

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