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

如何解决从另一个文件引用类型变量时出错

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

• groups.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 (Pos.to_nat x)”的类型为“groups.G”，而它是 预计类型为“G”。

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

而不是Definition pow_z (a: groups.G) (z: Z) : G。

然后它给出另一个错误：

术语“a”具有类型“G”，而预期具有类型 “groups.G”。

如何解决这个问题？

解决方法

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

Coq 的错误消息紧随其后，因为您声明了两个名为 G 的全局常量，每个模块中一个。一旦声明了第二个，第一个就被 Coq 用 groups.G 指定（这是将这个常量与其他常量区分开来的最短名称）。现在 pow 操作并返回一个 groups.G，而您要求 pow_z 返回一个 G（在此位置的文件 groups_Z.v 中表示 groups_Z.G,与 groups.G 不同）。

注意：群论在 Coq 中已经发展了好几次，如果你想做任何事情而不是对系统进行试验，我建议你在现有库的基础上工作。例如，数学组件库有一个 finite group library。

,

我将两个文件中的 Parameter G: Type. 更改为 Variable G: Type，并将 pow_z 定义更改为：

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.