Proof Trick: Small Inversions
Proof Trick: Small Inversions
复制标题
证明技巧：小反转
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
J. Monin
中科院分区：
文献类型：
--
作者：
J. Monin
我们展示了如何用小的证明项来反转归纳假设，使用对角谓词的依赖消除。该技术不需要任何辅助类型，如True，False，eq。在某种意义上，它也可以用来区分Coq中归纳类型的排序Prop的构造函数。
We show how an inductive hypothesis can be inverted with small proof terms, using just dependent elimination with a diagonal predicate. The technique works without any auxiliary type such as True, False, eq. It can also be used to discriminate, in some sense, the constructors of an inductive type of sort Prop in Coq.