从另一个文件引用类型变量时出错

Question

我正在研究coq中群论的形式化。我有两个文件:

• 组。v -包含组
的定义和定理
• groups_Z。v -包含Z群的定理和定义。

groups.v:

Require Import Coq.Setoids.Setoid.
Require Import Coq.Lists.List.
Require Import PeanoNat.
Class Semigroup G : Type :=
{
mult : G -> G -> G;
assoc : forall x y z:G,
mult x (mult y z) = mult (mult x y) z
}.
Class Monoid G `{Hsemi: Semigroup G} : Type :=
{
e : G;
left_id : forall x:G, mult e x = x;
}.
Class Group G `{Hmono: Monoid G} : Type :=
{
inv : G -> G;
left_inv : forall x:G, mult (inv x) x = e;
}.
Declare Scope group_scope.
Infix "*" := mult (at level 40, left associativity) : group_scope.
Open Scope group_scope.
Section Group_theorems.
Parameter G: Type.
Context `{Hgr: Group G}.
(* More theorems follow *)
Fixpoint pow (a: G) (n: nat) {struct n} : G :=
match n with
| 0 => e
| S n' => a * (pow a n')
end.
Notation "a ** b" := (pow a b) (at level 35, right associativity).
End Group_theorems.
Close Scope group_scope.

groups_Z.v:

Add LoadPath ".".
Require Import groups.
Require Import ZArith.
Open Scope group_scope.
Section Z_Groups.
Parameter G: Type.
Context `{Hgr: Group G}.
Definition pow_z (a: groups.G) (z: Z) : G :=
match z with
| Z0 => e
| Zpos x => pow a (Pos.to_nat x)
| Zneg x => inv (pow a (Pos.to_nat x))
end.
Notation "a ** b" := (pow_z a b) (at level 35, right associativity).
End Z_groups.
Close Scope group_scope.

尝试定义pow_z失败，消息:

术语&;pow a (post .to_nat x)&;有类型"组"。当它是

如果我们使用不同的签名:Definition pow_z (a: G) (z: Z) : G

代替Definition pow_z (a: groups.G) (z: Z) : G。

则给出另一个错误:

术语";a&;"有"G"虽然它应该有类型"groups.G".

如何解决这个问题?

Answer 1

在Coq中，命令Parameter G : Type声明了一个全局常量，这类似于公理化抽象类型G : Type的存在。从理论的角度来看，这应该是ok的，因为这个公理是微不足道的实现，但我认为你的意思是Variable G : Type表示一个局部变量，而不是。

Coq的错误消息从那里开始，因为您声明了两个名为G的全局常量，每个模块一个。一旦声明了第二个常量，第一个常量就由Coq的groups.G指定(这是使该常量与其他常量消除歧义的最短名称)。现在pow操作并返回groups.G，而您要求pow_z返回G(在此位置的groups_Z.v文件中意味着groups_Z.G，与groups.G不同)。

NB:群论在Coq中已经开发了好几次，如果你想做一些其他的事情，而不是尝试这个系统，我建议你在现有的库上工作。例如，数学组件库有一个有限群库。

Answer 2

我在两个文件和pow_z定义中将Parameter G: Type.更改为Variable G: Type:

Definition pow_z (a: G) (z: Z) : G :=
match z with
| Z0 => e
| Zpos x => pow G a (Pos.to_nat x)
| Zneg x => inv (pow G a (Pos.to_nat x))
end.