A tactic language for the system Coq
A tactic language for the system Coq
复制标题
DOI：
10.1007/3-540-44404-1_7
复制
发表时间：
2000-01-01
期刊：
影响因子：
--
通讯作者：
Delahaye, D
中科院分区：
文献类型：
--
作者：
Delahaye, D
我们提出了一个新的战术语言的系统Coq，这是为了丰富目前的战术组合（战术）。这种语言是基于一个功能的核心与递归和匹配运算符的Coq条款，但也证明上下文。它可以直接用于证明脚本或顶层定义（战术定义）。我们表明，这种语言的实现涉及到相当大的变化，证明脚本的解释，基本上是由于匹配运算符。我们给出了一些例子，解决小证明部分本地和其他一些处理非平凡的问题。最后，我们讨论了这种元语言的地位，相对于Coq语言和Coq的实现语言。
We propose a new tactic language for the system Coq, which is intended to enrich the current tactic combinators (tacticals). This language is based on a functional core with recursors and matching operators for Coq terms but also for proof contexts. It can be used directly in proof scripts or in toplevel definitions (tactic definitions). We show that the implementation of this language involves considerable changes in the interpretation of proof scripts, essentially due to the matching operators. We give some examples which solve small proof parts locally and some others which deal with non-trivial problems. Finally, we discuss the status of this meta-language with respect to the Coq language and the implementation language of Coq.