智能修改Coq环境

Ltac用于automating proofs and modifying proof environment，outputting strings和defining complex notations。它也可以用于Coq环境的“智能”修改吗？这里有两个失败的尝试：智能修改Coq环境

Variable Phy: Set. 

Fail Let pp (x:Type) := ltac: (match type of x with 
     | Set => constr: (Reset Phy) 
     | _ => idtac end). 
(*Cannot infer an internal placeholder of type "Type" in environment: x : Type*) 

Fail Ltac pp x := match type of x with 
     | Set => constr: (Reset Phy) 
     | _ => idtac end. 
(*The reference Reset was not found in the current environment.*)

另外，如果这不是Ltac的工作，也许有另一种方式？

来源

2017-03-17 jaam

我无法理解片段试图完成什么;你能详细说明一下吗？ –

如果条件得到满足，他们试图释放变量'Phy' – jaam

简短的回答：第

即使你会达到这样做，使用一些黑客，会停止在未来勒柯克版本工作。

原因是因为ltac命令的解释发生在比文档解释更低的层次上。这个选择可能是有争议的，但它是这样的。战术运行在一个不变的环境中，只能访问证据。因此，你可以从ltac做的最多的是修改当前的证明。

您的错误发生是因为Reset确实在ltac无法访问的较高级别进行解析。

对于环境和文档自身的编程操作，您需要依赖ML代码，或者您可以尝试编写一些接口工具（如SerAPI）来实现您想要的功能。

来源

2017-03-17 20:31:57 ejgallego

“战术运行在一个不变的环境中，只能访问证明”这不完全正确，因为目前有一种黑客可以在内部添加定义但它很可能会消失，因为它很难进行并行证明处理。 – ejgallego

为了保持完整性，您可以添加一个参考文件 – jaam

只需在定义内部定义a：= 3'。这将从证据中改变环境。这本身就是通过遍布所有Coq源的数千行代码来实现的。 – ejgallego

智能修改Coq环境

回答

相关问题