record - 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
}.

我得到的错误是:

Error: U already exists.

任何帮助表示赞赏。

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 .