The Coq mailing list

[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*)