The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Indeed, an instance is just syntactic sugar for a definition, an initial [refine] in the proof of that definition, and a hint resolve.

Michael, your tactic fails in the case where there are ambiguous instances.  There is a way around this: you can construct a typeclass that takes in a list and another class and is resolved by an instance of that class not in the list.  By applying this recursively, you can get the first n instances of any class.

On Mon, Sep 12, 2016, 7:36 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 09/12/2016 04:15 AM, Soegtrop, Michael wrote:
> Dear Jonathan, Daniel,
>
>> I don't think there is a way tactically to decide if a definition is an instance
> I thought about it once more: one issue with eauto is that it will also use local hypothesis. So these must be cleared before the test and this must be undone after the test. Below is a tactic which does this with a few test cases.

Another issue is that the typeclass_instances db can contain hints that
solve the goal with a non-instance in 1 step even if it isn't a
typeclass-typed goal.  If hole refinement is used instead: just "pose (_
: T) as Hex" - if it doesn't fail, then at least we know T is a Class,
but that doesn't mean that it was filled in with an instance, again due
to typeclass_instance hints.  The reason is that typeclasses are duck
types - any way you can fill in their requirements works.  The
"Instance" syntax is little (nothing?) more than a normal definition
combined with a resolve hint for the typeclass_instances db.

But, maybe this is good enough - in that the required unfolding would
work for such "faked" instances as well?   Because a faked instance is
just a good as a real one?

Or maybe unfolding all projections that simplify is good enough, even if
they're just projections on plain old records?

-- Jonathan