CODEWITHSUNDEEP
coq
user4035
user4035

Reputation: 23729

Error when referencing type variable from another file

I am working upon formalization of groups theory in coq. I have 2 files:

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.

The attempt to define pow_z fails with message:

The term "pow a (Pos.to_nat x)" has type "groups.G" while it is expected to have type "G".

If we use the different signature: Definition pow_z (a: G) (z: Z) : G

instead of Definition pow_z (a: groups.G) (z: Z) : G.

then it gives another error:

The term "a" has type "G" while it is expected to have type "groups.G".

How to fix this?

Upvotes: 0

Views: 57

Answers (2)

user4035
user4035

Reputation: 23729

I changed Parameter G: Type. to Variable G: Type in both files and pow_z definition to this:

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.

Upvotes: 0

Cyril
Cyril

Reputation: 367

In Coq, the command Parameter G : Type declares a global constant, which is akin to axiomatizing the existence of an abstract Type G : Type. From a theoretical point of view, this should be ok as this axiom is trivially realizable, but I think you meant Variable G : Type to denote a local variable instead.

The errors messages of Coq follow from there because you declare two global constants named G, one in each module. As soon as the second one is declared, the first one is designated by groups.G by Coq (it's the shortest name that disambiguates this constant from others). Now pow operates on and returns a groups.G, while you require pow_z returns a G (which in file groups_Z.v at this location means groups_Z.G, and is different from groups.G).

NB: Group theory has been developed several times in Coq, and if you want to do anything else than experimenting with the system, I would advise you work on top of existing libraries. For example the mathematical components library has a finite group library.

Upvotes: 1

Related Questions