`Control.refine`在Ltac2中做什么？

Question

我正在学习Ltac2和阅读coq 8.13.2的正式文件。

我不知道Control.refine在引文内部的评估中扮演了什么角色，因为对这个函数似乎没有太多的解释。

例如，在constr引号中的策略表达式中使用变量应该由：constr:(... $x ...)完成，其中$x是ltac2:(Control.refine (fun () => x))的语法糖。

简单地说，为什么ltac2:(x)不起作用？(实际上，在插入由Error: Cannot infer an existential variable of type ...表示的x的位置时，coq没有给出一个错误)。

所以我的问题是：

1. Control.refine一般是做什么的？
2. 有时这样做似乎是一种成语：constr:( ... ltac2:(Control.refine (fun () => ...) ...)，在什么情况下应该(或不应该)使用这种反引号成语？

谢谢。

Answer 1

ltac2:(...)内引号期望的是unit类型的Ltac2术语，而不是constr类型的术语.实际上，由于这个原因，您的示例应该触发一个警告。

由于引号的内容具有unit类型，这意味着它只能通过副作用起作用。警告告诉您，引用返回的值将被丢弃。特别是，它不能用来填补这个洞。

相反，引号的语义是在目标Γ ⊢ A中评估其内容，其中Γ是当前的假设列表，A是推断的空洞类型。预计这样做将解决目标，得到的部分证明将被用作该孔的Coq项填充。这正是Control.refine : (unit -> constr) -> unit的réle。它以一个(出于技术原因，被拒绝的)术语作为一个论点，并使用它来解决所关注的目标。

在你的例子中所发生的是，你提供了一个被忽略的术语，目标没有被触及，引文正确地抱怨它没有解决。

至于你的第二点，我实在说不清。这取决于你想做什么。但是总的来说，如果你坚持使用反引号$x，我会认为这更容易读懂。但是，并不总是能够做到这一点，例如，如果正在构建的术语依赖于constr:(...)引号中引入的上下文。