The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

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?

Vadim

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060