How do I unfold class instances in Coq? It seems to be possible only when the instance doesn't include a proof, or something. 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.
thm1
is proved, but I can't prove thm2
; it complains at the unfold C2_nat
step with Error: Cannot coerce C2_nat to an evaluable reference.
.
What's going on? How do I get to C2_nat
's definition of v2
?
You ended the definition of C2_nat
with Qed
. Definitions ending with Qed
are opaque and cannot be unfolded. Write the following instead
Instance C2_nat: C2 nat:= {v2:=4}.
trivial.
Defined.
and your proof finishes without problems.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With