Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
复制标题
递归函数的定义和推理：Coq Proof Assistant 的实用工具
DOI：
10.1007/11737414_9
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Vlad Rusu
中科院分区：
文献类型：
--
作者：
G. Barthe;Julien Forest;David Pichardie;Vlad Rusu
我们提出了一个实用的工具，用于定义和证明递归函数的性质的Coq证明助手。该工具从伪代码生成预期函数的图形作为归纳关系。然后它证明了这个关系实际上代表了一个函数，这个函数就是我们试图定义的函数。然后，我们生成归纳和反演原理，以及用于证明函数其他性质的不动点方程。我们的工具建立在最先进的技术，用于定义递归函数，也可以用来生成可执行的功能，从他们的图形的归纳描述。我们通过两个案例研究说明了我们的工具的好处。
We present a practical tool for defining and proving properties of recursive functions in the Coq proof assistant. The tool generates from pseudo-code the graph of the intended function as an inductive relation. Then it proves that the relation actually represents a function, which is by construction the function that we are trying to define. Then, we generate induction and inversion principles, and a fixpoint equation for proving other properties of the function. Our tool builds upon state-of-the-art techniques for defining recursive functions, and can also be used to generate executable functions from inductive descriptions of their graph. We illustrate the benefits of our tool on two case studies.