The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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.

-- Jonathan