Coq 记录类型

Question

我是Coq的新手。当我尝试定义两个带有相同名称类型字段的记录类型时，会出现错误。例如：

Record squag := {
    U : Type;
    op : U -> U -> U where "x * y" := (op x y);
    idempotent_op : forall x : U, (x * x) = (x);
    commutative_op : forall x y : U, (x * y) = (y * x);
    antiAbsorbent_op : forall x y: U, (x * (x * y)) = (y)
}.
Record dummy := { 
    U : Type; 
    zero : U
}.

我遇到的错误是：

错误：U 已存在。

感谢任何帮助。

- Yasmine Shaorda

Answer 1

在Coq命名空间中，您不能重复使用记录名称。但是，您可以在不同的文件或模块中声明两个记录：

Module Squag.
Record squag := {
    U : Type;
    op : U -> U -> U where "x * y" := (op x y);
    idempotent_op : forall x : U, (x * x) = (x);
    commutative_op : forall x y : U, (x * y) = (y * x);
    antiAbsorbent_op : forall x y: U, (x * (x * y)) = (y)
}.
End Squag.

Module Dummy.
Record dummy := { 
    U : Type; 
    zero : U
}.
End Dummy.

然后，您可以将这两个字段分别称为Squag.U和Dummy.U。

- Arthur Azevedo De Amorim

---

如果我定义的是一些代数理论（如幺半群、群等）的库，有没有比每个理论都有一个单独的模块更好的处理方式？ - Yasmine Shaorda

您可能想查看“打包数学结构”（Packaging Mathematical Structures）论文（它是有关math-comp的），以及“math-classes”库（其中有一篇描述其架构的论文）。 - Anton Trunov

为类似结构声明不同的名称与证明和使用这些结构的公共引理相比，是一个小问题 - 例如，如果我证明了一些关于群的东西，我能用它来处理阿贝尔群吗？Anton提到的库解决了这个问题，你应该去看看。 - Arthur Azevedo De Amorim