Ssreflect Users Discussion List

[Bas Spitters <>]

Dear Ben,

We have a formalization of basic category at:
http://www.xs4all.nl/~weegen/eelis/research/math-classes/

Our approach uses type classes, but it seems that you can do something
similar using canonical structures. We also have a basic library of
universal algebra. In order to extend reflection to category theory
you would need generalized algebraic theories (i.e. add dependent
types).

At the end of our paper you will find an explanation of how to use
quoting with type classes. We borrowed the idea from Matita, but
Georges found it independently and has been using it in ssr for some
time now. I believe it is explained in the new ssr tutorial:
http://www.msr-inria.inria.fr/Projects/math-components/tutorial.pdf

Finally, Kozen has a Gentzen style proof system for basic category theory.
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.85.7497
I have not looked at the details, but this may serve as the syntactic
layer for a reflective tool in Coq.

Bas

On Fri, Sep 17, 2010 at 1:08 PM, ben <> wrote:
> Hello,
>
> i am formalizing category theory in Coq, and i was wondering whether
> reflection could help with the automation of some proofs.
>
> From Yves' book i know how reflection works in theory. Nevertheless it
> would be nice to see some real life example of a proof in some algebraic
> theory done by reflection, in order to get a better feeling for what
> kind of problems are suitable for being treated with this technique.
>
> Could you point me to an example, a theorem (of, say group theory ?)
> where reflection was particularly helpful ?
>
> Thanks a lot in advance,
> ben
>
>