The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/01/2016 07:38 PM, Jonathan Leivent wrote:
> On 09/01/2016 07:19 PM, Vadim Zaliva wrote:
> > Sometimes I wish I can avoid automatic typeclass resolution and make it
> > generate sub-goals for all unresolved type class instances. Then I can
> > proceed and prove them manually, instead of using Hints, etc. Something
> > like 'unshelve':
> >
> > The following example:
> >
> > Class A (n:nat) : Prop.
> > Definition f (n:nat) `{A n} := n.
> > Definition g (n:nat) := n.
> > Lemma Foo:  forall x, f (g x) = x.
> >
> > In absence of:
> >
> > Instance A_g:  forall x, A (g x).
> >
> > gives me:
> >
> > Error:
> > Unable to satisfy the following constraints:
> > In environment:
> > x : nat
> >
> > ?H : "A (g x)"
> >
> > And I could not proceed with the proof. Why couldn't it just generate a
> > sub-goal for A (g x) ?
> >
> > Is there is a way to achieve this behavior in current version?
>
> Is this sufficient?:
>
> Class A (n:nat) : Prop.
> Definition f (n:nat)`{A n} := n.
> Definition g (n:nat) := n.
>
> Lemma Foo:  exists w, forall x, @f (g x) (w x) = x.
> unshelve eexists.

This might be better:

Lemma Foo:  forall x, exists w, @f (g x) w = x.
intro x.
unshelve eexists.

I think using an evar - either one created by exists or by the evar 
tactic (not refine) - are the only ways to create a subgoal of a class 
type that Coq doesn't immediately try to resolve.  To use refine to do 
this, I think you have to create the hole with some other type that you 
can reduce to the desired class.

-- Jonathan