如何在 Coq 中展开类实例?似乎只有当实例不包含证明或其他东西时才有可能。考虑一下:
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
;它在 unfold C2_nat
投诉步入 Error: Cannot coerce C2_nat to an evaluable reference.
.这是怎么回事?我如何到达
C2_nat
v2
的定义?
最佳答案
您结束了 C2_nat
的定义与 Qed
.以 Qed
结尾的定义是不透明的,不能展开。改写以下内容
Instance C2_nat: C2 nat:= {v2:=4}.
trivial.
Defined.
并且你的证明完成没有问题。
关于typeclass - Coq:展开类实例,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/24111816/