The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

That is normal, as the kind of the implementation of a type (inductive, coinductive, or forall) is unknown to the module type. I must admit, that it would be nice to add support for inductives in the "with" definitions. An easy workaround is to define your inductive outside of the module, and then bind your type in the module with the one you defined.

Module Foo : Bar
with Inductive Baz := Constructor.
…

does not work, but

Inductive Baz_ := Constructor.
Module Foo : Bar
with Definition Baz := Baz_
…

is the usual way people work around this limitation.

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

Thanks, I didn't know about this feature.

But I failed to use it with inductive types, because there is can be only
Definition or Module as <decl> in Module ... with <decl>.
(I am getting error if I try to use Inductive instead of decl,
reference manual talks about this, too.)

Sincerely,
Kirill Taran

On Wed, Feb 26, 2014 at 9:09 AM, AUGER Cédric <sedrikov AT gmail.com> wrote:

Le Wed, 26 Feb 2014 05:39:11 +0400,
Kirill Taran <kirill.t256 AT gmail.com> a écrit :

> Hello.
>
> Is it possible to declare types inside module such way that I can
> pattern match on them outside of the module?
> (When I define module satisfying signature I must declare types with
> Definition or wrap Inductive/Record with it;
> that makes type content invisible to module users; I suspect that this
> behaviour is implemented intentionally.)
>
> Sincerely,
> Kirill Taran

I am not sure that is what you wish, but as far as I can remember
(sorry, I almost never use modules in Coq as I find them often less
convenient than records/type classes), there is a "with" syntax defined
in the reference documentation.

Without the "with", modules implementing a module type are made opaque,
so that all inductive types defined inside of it cannot be
pattern-matched, but with "with" you can require the type to be
transparent. Below is an example (without inductives). See the
reference manual for better explanations.

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

Module Type Cat.
  Parameter Obj : Type.
  Parameter Hom : Obj -> Obj -> Type.
  Parameter Id : forall x, Hom x x.
  Parameter Comp : forall z y, Hom y z -> forall x, Hom x y -> Hom x z.
  Hypothesis LId : forall x y (f : Hom y x), Comp x x (Id x) y f = f.
  Hypothesis RId : forall x y (f : Hom y x), Comp x y f y (Id y) = f.
  Hypothesis Assoc
  : forall t z (f : Hom z t) y (g : Hom y z) x (h : Hom x y),
    Comp t z f x (Comp z y g x h) = Comp t y (Comp t z f y g) x h.
End Cat.

Module Opp (C : Cat) : Cat
with Definition Obj := C.Obj
with Definition Hom := fun x y => C.Hom y x
with Definition Id := C.Id
with Definition Comp := fun z y f x g => C.Comp x y g z f.
  Definition Obj := C.Obj.
  Definition Hom := fun x y => C.Hom y x.
  Definition Id := C.Id.
  Definition Comp := fun z y f x g => C.Comp x y g z f.
  Lemma LId : forall x y (f : Hom y x), Comp x x (Id x) y f = f.
  Proof. intros; apply C.RId. Defined.(*for teaching purpose, use Qed in practice*)
  Lemma RId : forall x y (f : Hom y x), Comp x y f y (Id y) = f.
  Proof. intros; apply C.LId. Defined.(*for teaching purpose, use Qed in practice*)
  Lemma Assoc : forall t z (f : Hom z t) y (g : Hom y z) x (h : Hom x y),
    Comp t z f x (Comp z y g x h) = Comp t y (Comp t z f y g) x h.
  Proof. intros; symmetry; apply C.Assoc. Defined.(*for teaching purpose, use Qed in practice*)
End Opp.

Fixpoint le (m n : nat) : Type :=
  match m with
  | O => unit
  | S m => match n with
           | O => Empty_set
           | S n => le m n
           end
  end.

Fixpoint le_id (m : nat) : le m m :=
  match m with
  | O => tt
  | S m => le_id m
  end.

Fixpoint le_comp (m : nat) : forall n, le m n -> forall o, le n o -> le m o :=
  match m as m return forall n, le m n -> forall o, le n o -> le m o with
  | O => fun _ _ o _ => tt
  | S m => fun n => match n with
                    | O => fun x => match x with end
                    | S n => fun H o => match o with
                                        | O => fun x => match x with end
                                        | S o => fun K => le_comp m n H o K end end end.

Module Le. (*no ":Cat" type annotation, so what follows is transparent*)
  Definition Obj := nat.
  Definition Hom := le.
  Definition Id := le_id.
  Definition Comp z y f x g := le_comp x y g z f.
  Lemma LId : forall x y (f : Hom y x), Comp x x (Id x) y f = f.
  Proof.
    intros x y f; revert x f; induction y; simpl; auto.
    + intros _ []; split.
    + intros []; simpl; auto.
      intros [].
  Defined. (*for teaching purpose, use Qed in practice*)
  Lemma RId : forall x y (f : Hom y x), Comp x y f y (Id y) = f.
  Proof.
    intros x y f; revert x f; induction y; simpl; auto.
    + intros _ []; split.
    + intros []; simpl; auto.
      intros [].
  Defined. (*for teaching purpose, use Qed in practice*)
  Lemma Assoc
  : forall t z (f : Hom z t) y (g : Hom y z) x (h : Hom x y),
    Comp t z f x (Comp z y g x h) = Comp t y (Comp t z f y g) x h.
  Proof.
    intros t z f y g x h; revert y h z g t f; induction x; simpl; auto.
    intros [].
    + intros [].
    + intros y h []; simpl.
      - intros [].
      - intros z g []; simpl; auto.
        intros [].
  Defined. (*for teaching purpose, use Qed in practice*)
End Le.

Module Ge := Opp Le.
(*as Opp uses "with", Ge.Obj, Ge.Hom, Ge.Id and Ge.Comp
  are transparent.
  Ge.LId is not transparent as it is not "with" defined when Opp was
  defined.
*)

Eval compute in (Ge.Hom 3 0). (*reduced to "unit" as expected*)
Eval compute in (Le.LId). (*big ugly transparent term*)
Eval compute in (Ge.LId). (*small nice opaque term*)

--
.../Sedrikov\...