The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-smb.fr>]

I have found a similar problem : https://coq-club.inria.narkive.com/aQkFMfjF/functor-modules-and-multiple-inheritance

However it has been proposed 13 years ago, so I expect that perhaps now there is a better way to solve it?

---

From: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
To: "coq-club" <coq-club AT inria.fr>
Sent: Sunday, December 22, 2024 5:00:09 PM
Subject: Re: [Coq-Club] Problem with definitions scope in imported module

Can you post a code snippet  that I can run locally on my machine? 

Best, 

Mukesh 

On Sun, 22 Dec 2024 at 15:13, richard <richard.dapoigny AT univ-smb.fr> wrote:

Thanks Mukesh for your prompt answer. 

However, it does not work since in that case, variables in F3 become unknown.

Le 22/12/2024 à 14:03, mukesh tiwari a écrit :

Hi Richard, 

In F2.v you have a definition  *Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).*  and then the same in F3.v  *Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).*. I suspect when you redefining Mereology in F3 and subsequently importing F2.v, somehow it is causing some confusion.  Trying removing the definition *Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).* from F3.v and see if it works (I am not an expert in modules so I cannot say for sure it is the case). 

Best, 

Mukesh 

On Sun, 22 Dec 2024 at 12:15, richard <richard.dapoigny AT univ-smb.fr> wrote:

Dear coq members,

I have the following problem with importing definitions with multiples
coq modules:

I have a file F1.v :
=====================================================================

Module  DST_signature (M1 : UsualDecidableTypeFull).
Import M1.
...
End DST_signature.
=====================================================================

then a file F2.v (there is a file F1.vo) :

=====================================================================
Require Import F1.

Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).

(** Module Abstract *Structure **)

Module geometry_signature (M1 : UsualDecidableTypeFull).

Module basis_mereo := Mereology M1.
Import basis_mereo.
...
End geometry_signature.
=====================================================================

and finally a file F3.v (there is a file F2.vo and a file F1.vo) :

=====================================================================

Require Import F1.
Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).

(** Module Abstract *Structure **)

Module AbstractStructure (M1 : UsualDecidableTypeFull).

Module basis_inst := Mereology M1.
Import basis_inst.
...
End  AbstractStructure.

Require Import F2.

Module Tarski_geom (M1 : UsualDecidableTypeFull).

Module basis_mereo := Mereology M1.
Import basis_mereo.
Module adt := AbstractStructure M1.
Import adt.
Module geom := geometry_signature M1.
Import geom.
...
Lemma test : forall A, η A balls -> η A (el Gspace). -> fail
...
End Tarski_geom.
=====================================================================

While there is no problem for all variables defined in F1 there seems to
be a problem with variables  defined in F2 since the error is :

The term "Gspace" has type "basis_mereo.N" while it is expected to have
type "N". (Gspace is defined in F2)

If someone has an idea to solve the problem?

Thanks in advance,

Richard