The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hi ,
Here is another problem with notations:


Module Type SIGNot.
Inductive InfTwoNat:nat-> Prop:=
ohConstructorTooLong: forall (n:nat), InfTwoNat n.
Notation "<<< n " :=(ohConstructorTooLong n  ) (at level 40):new_scope.
End SIGNot.

Module sigImpl <:SIGNot.
Inductive InfTwoNat:nat ->Prop:=
ohConstructorTooLong: forall (n:nat), InfTwoNat n.

End sigImpl.

Module Type FUN.
Declare Module sigsig :SIGNot.
End FUN.
Module Ext (picsou:SIGNot)<:FUN.
Module sigsig:=picsou.
End Ext.


Module foufou(fun1:FUN)(fun2:FUN with Module sigsig:=fun1.sigsig).
Open Scope new_scope.
Import fun1.sigsig.
Check (fun1.sigsig.ohConstructorTooLong O).

(* Coq < <<< 0
    : InfTwoNat 0 
the notation works  :-) *)


Check (fun2.sigsig.ohConstructorTooLong O).
(* fun2.sigsig.ohConstructorTooLong 0
    : fun2.sigsig.InfTwoNat 0 
it doesn't work  :-( *)

As we see both fun1.sigsig and fun2.sigsig are of type SIGNot where the 
notation is defined...
I think this problem results from the equivalence between modules which is 
not supported by the current version of Coq...in fact we have 
fun1.sigsig=fun2.sigsig ...
Can this problem be solved ?!






Pierre Casteran wrote:

> Jacek Chrzaszcz wrote:
>
> > On Mon, Jan 12, 2004 at 01:03:15PM +0100, Houda Anoun wrote:
>
> > Seriously, in situations like this one:
> > Module M:T:=A
> > one has to decide which elements come from T and which from A.
> > Now they simply all come from T.
>
>
>
> There is a slight problem. This work only if we work with opaque
> signature constraint , and not if I use '<:'
>
> Module Type S1.
> Inductive P : Set :=
> c : P.
> Notation "'XXX'" := c (at level 40) : my_scope.
> End S1.
>
> Module M1 <: S1.
> Inductive P : Set :=
> c : P .
> End M1.
>
>
> Import M1.
>
> (* Open Scope my_scope.
> Error: Scope my_scope is not declared *)
>
>
> If I use a constraint with ':', the notation is available :
>
> Module M2 : S1.
> Inductive P : Set :=
> c : P .
> End M2.
>
> Import M2.
>
> Open Scope my_scope.
>
> Check c.
>
> (*
> XXX : P
> *)
>
> By the way, I have often to deal with inductive type definitions.
> Is it OK to put the inductive definition in the signature (since
> it is a declaration of the constructors and the _ind, _rec, ...
> theorems), and duplicate the inductive definition in the signature
> and in the module and/or functor ?.
>
> Pierre
>
> P.S.
> Jacek, Igor (Walukiewicz) told me about your thesis. Congratulations !