Coq: Deploying Class Instances

Question

How to deploy class instances in Coq? This seems possible only when the instance does not contain evidence or anything else. Consider this:

Class C1 (t:Type) := {v1:t}.
Class C2 (t:Type) := {v2:t;c2:v2=v2}.

Instance C1_nat: C1 nat:= {v1:=4}.

Instance C2_nat: C2 nat:= {v2:=4}.
trivial.
Qed.

Theorem thm1 : v1=4.
unfold v1.
unfold C1_nat.
trivial.
Qed.

Theorem thm2 : v2=4.
unfold v2.
unfold C2_nat.
trivial.
Qed.

thm1proven, but I cannot prove thm2; he complains about unfold C2_natusing Error: Cannot coerce C2_nat to an evaluable reference..

What's happening? How to get to the C2_natdefinition v2?

Answer 1

You have finished defining C2_natwith Qed. Definitions ending in Qedare opaque and cannot be expanded. Write instead

Instance C2_nat: C2 nat:= {v2:=4}.
  trivial.
Defined.

and your proof ends without a problem.