A Semi-reflexive Tactic for (Sub-)Equational Reasoning
A Semi-reflexive Tactic for (Sub-)Equational Reasoning
复制标题
（亚）等式推理的半反身策略
DOI：
10.1007/11617990_7
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
C. Coen
中科院分区：
文献类型：
--
作者：
C. Coen
我们提出了一个简单的单调函数理论，这是实施策略的基础，该策略是通过“传播” Xry形式的约束条件重写的，其中关系r可以比等价关系更弱。只有在每个参数中是单调的N- ARY功能的句法组成的目标。 NUPRL早期类似发展的新颖性和改进。
该策略的一些有趣的应用是：关于等价类的类型理论的推理（通过在定义明确的目标中进行重写）；在给定单调的情况下，用较小的（较大）替换一个术语来传播不平等。
We propose a simple theory of monotone functions that is the basis for the implementation of a tactic that generalises one step conditional rewriting by “propagating” constraints of the form xRy where the relation R can be weaker than an equivalence relation. The constraints can be propagated only in goals whose conclusion is a syntactic composition of n-ary functions that are monotone in each argument. The tactic has been implemented in the Coq system as a semi-reflexive tactic, which represents a novelty and an improvement over an earlier similar development for NuPRL.
A few interesting applications of the tactic are: reasoning in type theory about equivalence classes (by performing rewriting in well-defined goals); reasoning about reductions and properties preserved by reductions; reasoning about partial functions over equivalence classes (by performing rewriting in PERs); propagating inequalities by replacing a term with a smaller (greater) one in a given monotone context.