The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello Pierre,

Yes, that seems to solve the problem I described.

But also seems that I described it non-fully. In my real case it is necessary to have access to g, when I define f (here it is IMPLF). We can define some more modules, but that will become too cumbersome.

The point is to model a system, which behaves according to our parameter-algorithm and some internal rules and then to implement this algorithm in other module with proof of correctness (and the theorem must look at function which models system).

Sincerely,
Kirill Taran

On Wed, Feb 12, 2014 at 4:49 AM, Pierre Courtieu <Pierre.Courtieu AT cnam.fr> wrote:

Hi, I would do the following. This is a bit cumbersome but this is the
price of putting definitions in a module type in the current state of
coq modules. If one could import things from a module type into a
module, we could factorize things. I think Elie Soubiran did his phd
on this subject, the idea was that there is no real difference between
a module type and a module in a dependently typed language.

I don't know if there are better solution.

Module Type Sig.
  Definition T : Type := nat.
  Parameter  f : T -> T.
  Definition g (t : T) : T := f (f t).
End Sig.

Module Impl <: Sig.

  Definition T : Type := nat.

  Definition f (t : T) : T := t * 2.

  Definition g (t : T) : T := f (f t).

End Impl.

You could make a functor building a sig from {T ; f } but you also end
up duplicating definitions between module and module type:

Module Type F.

  Definition T: Type := nat.
  Parameter  f : T -> T.

End F.

Module IMPLF<:F.

  Definition T: Type := nat.

  Definition f (t : T) : T := t * 2.

End IMPLF.

Module Type Sig(A:F).
  Import A.

  Definition g (t : T) : T := f (f t).
End Sig.

Module IMPLSig <: Sig(IMPLF).
  Import IMPLF.

  Definition g (t : T) : T := f (f t).

End IMPLSig.

Best regards,
Pierre

2014-02-11 22:26 GMT+01:00 Kirill Taran <kirill.t256 AT gmail.com>:

> Module Type Sig.
>   Definition T : Type := nat.
>   Parameter  f : T -> T.
>   Definition g (t : T) : T := f (f t).
> End Sig.
>
> Module Impl <: Sig.
>   Definition f (t : T) : T := t * 2.
> End Impl.