Coq：展开类实例

问题描述

如何在Coq中展开类实例？似乎只有当实例不包含证明或其他东西时，才有可能。考虑一下：

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 被证明，但是我可以证明 thm2 ;它在展开C2_nat 步骤时抱怨，并带有错误：无法将C2_nat强制为可评估的引用。。

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..

这是怎么回事？如何获得 v2 的 C2_nat 定义？

What's going on? How do I get to C2_nat's definition of v2?

推荐答案

您以 Qed 结束了 C2_nat 的定义。以 Qed 结尾的定义是不透明的，无法展开。而是写以下内容

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.

这篇关于Coq：展开类实例的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！