coq - 可判定子集类型术语的简单语法
问题描述
我有一个类型BoundedNat n，代表小于的自然数n。我目前的实现如下：
Definition BoundedNat n := {x : nat | x < n}.
操作类型的元素BoundedNat n是相对重量级的。我经常需要包装（使用exist n ltac:(lia)）和解包（使用proj1_sig）元素。我怎样才能最好地利用底层类型的符号、相等、排序等？
解决方案
尽管您绝对可以汇总自己的有界自然数实现，但我强烈建议您重用现有的。我最喜欢的库是 ssreflect。它包含一个ordinal n对应于你的类型族，BoundedNat在fintype.v（doc here）中定义。ordinalfrom to有一个强制转换，nat因此您可以轻松地透明地重用大多数自然数上的运算符——例如，您可以i < j直接编写 when i j : ordinal n。
构建术语ordinal更复杂，因为它需要证明论证。没有找到此证明的最佳方法，因此继续进行的方法取决于应用程序。例如，向有界 nat 添加一个常量是很常见的，值得在 ssreflect 中进行专门的操作：
rshift : forall m n, ordinal n -> ordinal (m + n)
使用 ssreflect 的优点之一是它带有对子集类型的通用支持，例如ordinal. 例如，有一个insub : nat -> option (ordinal n)函数只有在其参数以 为界时才成功n。此函数不仅适用于natand ordinal，而且适用于由subtype接口连接的任何类型对：sT是 的子类型Tif 它是{x : T | P x}某种 boolean predicate的形式P。因此，您可以使用一致的界面操作子类型，而不是每次都滚动您自己的子类型。