2

如何在 Coq 中定义同构类？

假设我有一个记录 ToyRec：

Record ToyRec {Labels : Set} := {
X:Set;
r:X->Labels
}.

以及 ToyRec 类型的两个对象之间的同构定义，说明如果存在保留映射元素标签的双射 f:T1.(X)->T2.(X)，则两个对象 T1 和 T2 是同构的。

Definition Isomorphic{Labels:Set} (T1 T2 : @ToyRec Labels) : Prop :=
exists f:T1.(X)->T2.(X), (forall x1 x2:T1.(X), f x1 <> f x2) /\ 
                         (forall x2:T2.(X), exists x1:T1.(X), f x1 = f x2) /\
                         (forall x1:T1.(X) T1.(r) x1 = T2.(r) (f x1)).

现在我想定义一个函数，它接受一个对象 T1 并返回一个包含所有与 T1 同构的对象的集合。

g(T1) = {T2 | Isomorphic T1 T2}

在 coq 中怎么做这样的事情？我知道我可能在这里推理过于理论化，但是同构类的正确类型理论概念是什么？或者更基本的是，如何定义满足给定属性的所有元素的集合（或类型）？

4

1 回答 1

3

这真的取决于你想用它做什么。在 Coq 中，有一个理解类型，它是 type 中所有满足 property{x : T | P x}的元素x的类型。但是，它是一种type，这意味着它用于对其他术语进行分类，而不是传统意义上可以计算的数据结构。因此，您可以使用它，例如，编写一个仅适用于满足的元素的函数（在这种情况下，函数的类型将是，它的结果类型在哪里），但您不能使用它来，比如说，写一个函数来计算有多少满足的元素。TPTP{x : T | P x} -> YYTP

如果你想用这个集合进行计算，事情会变得有点复杂。让我们假设P是一个可判定的属性，这样事情就变得更容易了。如果T是有限类型，那么您可以使用具有理解运算符的集合数据结构（例如，查看Ssreflect库）。但是，这会在无限时中断T，这是您的ToyRec类型的情况。正如 Vinz 所说，没有通用的方法可以建设性地将这个集合构建为数据结构。

如果你准确地解释了你想用这种类型做什么，也许会更容易得到一个完整的答案。

于 2015-01-08T22:50:31.083 回答