The Coq mailing list

[Eduardo Ochs <eduardoochs AT gmail.com>]

Hello list,

this is probably a basic question (I'm a newbie) but anyway, here it
goes... If abcdefg is a 7-uple - with a complex dependent type - is
there a way to extract all its components at once? Something like this
would be ideal,

  Definition (a, b, c, d, e, f, g) := abcdefg.

but this is not accepted...

Let me explain how I arrived at this problem. I am trying to use Coq
to formalize a certain notation that I have been using for years for
doing constructions and proofs in Category Theory, and I tried to do
this:

  (* ------ snip, snip ------ *)

  Definition type_of (T : Type) (t : T) := T.
  Implicit Arguments type_of [T].

  Section Categories.
    Variable C_0     : Type.
    Variable Hom_C   : C_0 -> C_0 -> Set.
    Variable id_C    : forall (A : C_0), Hom_C A A.
    Variable o_C     : forall (A B C : C_0) (g : Hom_C B C) (f : Hom_C A B),
                              Hom_C A C.
                       Implicit Arguments o_C [A B C].
    Variable idL_C   : forall (A B : C_0) (f : Hom_C A B),
                              (o_C (id_C _) f = f).
                       Implicit Arguments idL_C [A B].
    Variable idR_C   : forall (A B : C_0) (f : Hom_C A B),
                              (o_C f (id_C _) = f).
                       Implicit Arguments idR_C [A B].
    Variable assoc_C : forall (A B C D : C_0)
                              (f : Hom_C A B) (g : Hom_C B C) (h : Hom_C C D),
                              (o_C h (o_C g f) = o_C (o_C h g) f).
                       Implicit Arguments assoc_C [A B C D].

    Definition C       := (C_0, Hom_C, id_C, o_C, idL_C, idR_C, assoc_C).
    Definition C_minus := (C_0, Hom_C, id_C, o_C).

    Definition Category      := type_of C.
    Definition Protocategory := type_of C_minus.

    Variable   D : Category.
    Definition (D_0, Hom_D, id_D, o_D, idL_D, idR_D, assoc_D) := D.  (* <- *)
    Definition D_minus := (C_0, Hom_C, id_C, o_C).

    (* etc... *)
  end Categories.

  (* ------ snip, snip ------ *)

It would be fantastic if the "(* <- *)" line above would be accepted,
but it isn't... Any hints, suggestions, pointers, workarounds (using
records, maybe)?...

Thanks in advance,
  Eduardo Ochs
  
eduardoochs AT gmail.com
  http://angg.twu.net/