coq - 在 Coq 中部分计算目标的策略

Question

我有目标

quad X Y

，但我不记得“四边形”的定义，也不想开始搜索它的定义。

有没有一种策略可以让我用它的定义快速替换 quad？

 Record quad (X Y:Type):= { x:X; y:Y}.

或者我必须记住并使用

refine (@Build_quad _ _).

?

Answer 1

您稍微弄错了，Build_quad不是 的定义quad，而是它的构造函数。它创建类型的术语quad。正如@ejgallego 所说，您应该constructor在这种情况下使用该策略。

您的目标希望您提供一个类型quad X Y的术语，而从头开始构建这样一个术语的唯一方法是使用Build_quad类型的构造函数forall X Y: Type, X -> Y -> quad X Y。