The Coq mailing list

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

Ok. Now it works fine. Thanks a lot!

bests regards

Richard

---

From: "Li-yao Xia" <lysxia AT gmail.com>
To: "Richard Dapoigny" <richard.dapoigny AT univ-smb.fr>
Cc: "coq-club" <coq-club AT inria.fr>
Sent: Thursday, May 22, 2025 10:01:09 AM
Subject: Re: [Coq-Club] Problem with scope of lemmas

Hi Richard,

Try removing the `Univ` parameter in the definition of the `open_space` field. `open_space Univ : ...` should be `open_space : ...`.

Cheers,
Li-yao

On 2025-05-21 1:39 PM, richard wrote:

f735b306-0b45-4997-8f0d-b7ae936c1f8e AT univ-smb.fr">

Dear Coq users,

I have first a module with a lot of lemmas and definitions:

Module  Mereo_signature (M1 : UsualDecidableTypeFull).
Import M1.

Definition ....

Lemma ...

Definition Universe : N := ...

End Mereo_signature.

Then, in a second module:

Module Topo_signature (M1 : UsualDecidableTypeFull).
Include Mereo_signature (M1).

...

Theorem int_space : (interior Universe) ≡ Universe.
Proof.

...

Class Kuratowski_Open (X :Type)(Univ :X)(equiv_open : X -> X -> Prop)(Inter : X -> X -> X) := {
  Open                             : X -> Prop ;
  Interior                           : X -> X;
  open_space Univ          : equiv_open (Interior Univ) Univ;
}.

Instance proof_topo : Kuratowski_Open N Universe singular_eq n_conjunction := {
  Open Q                                := exists a : N, η Q (klass a);
  Interior Q                              := interior Q;
  open_space Universe           := int_space;
}.

End Topo_signature.

I have the following error:

In Environment Universe: N The term "int_space" has type "interior Topo_signature.Universe = Topo_signature.Universe" while it is expected to have type "interior Universe = Universe".

If anyone has an idea to solve that difficulty?

Thanks in advance,

Richard