The Coq mailing list

[Daniil Frumin <difrumin AT gmail.com>]

Hm maybe you are using an old version of the library. Try following links:

http://coq.inria.fr/pylons/contribs/files/GroupTheory/v8.4/GroupTheory.tar.gz
http://coq.inria.fr/pylons/contribs/view/FreeGroups/v8.4
http://coq.inria.fr/pylons/contribs/view/Algebra/v8.4
http://coq.inria.fr/pylons/contribs/view/LinAlg/v8.4


On Wed, Jan 15, 2014 at 12:38 AM, Ömer Sinan Ağacan
<omeragacan AT gmail.com>
 wrote:
> Hmm, apparently I can't compile GroupTheory library. My Coq version is:
>
> The Coq Proof Assistant, version 8.4pl2 (June 2013)
> compiled on Jun 30 2013 12:15:13 with OCaml 4.00.1
>
> and error message is:
>
> File "./g1.v", line 257, characters 0-21:
> Error:
> Found no subterm matching "star a (exp (neg (S n1)) a)" in the current goal.
> make: *** [g1.vo] Error 1
>
> any ideas about that?
>
> Thanks,
>
> ---
> Ömer Sinan Ağacan
> http://osa1.net
>
>
> 2014/1/14 Ömer Sinan Ağacan 
> <omeragacan AT gmail.com>:
>> Wow, thanks all for your answers. This amount of code should keep me
>> busy for a while. I hope I can understand the Coq used in these
>> implementations.
>>
>> ---
>> Ömer Sinan Ağacan
>> http://osa1.net
>>
>>
>> 2014/1/14 Vladimir Voevodsky 
>> <vladimir AT ias.edu>:
>>>
>>> On Jan 14, 2014, at 3:18 PM, Daniil Frumin wrote:
>>>
>>>> Hi,
>>>>
>>>> There are many examples of proof of the specific theorems/properties
>>>> on the internet: everything from blogposts to Coq contributions that
>>>> Harley has linked.
>>>>
>>>> However, there are also bigger projects, like Math Classes [1], which
>>>> aim is to develop interfaces (based on Coq's typeclasses) for many
>>>> algebraic gadgets.
>>>>
>>>> Recently, Vladimir Voevodsky has published his paper [2] on his work
>>>> in the formalization of mathematics. I haven't read it yet, but I
>>>> guess it deals with Univalence, HoTT and other things I am clueless
>>>> about.
>>>>
>>>> I myself tried to formalize basic category theory [3] and I've got to
>>>> say it is going slower than I want and it is harder than I initially
>>>> anticipated.
>>>>
>>>> [1] http://math-classes.org
>>>> [2] http://arxiv.org/abs/1401.0053
>>>> [2] http://repos.covariant.me/browse?r=cat;a=tree
>>>
>>>
>>> There is a conceptually correct formalization of the basics of basic 
>>> category theory here:
>>>
>>> https://github.com/benediktahrens/rezk_completion
>>>
>>> with the accompanying paper here:
>>>
>>> http://arxiv.org/abs/1303.0584
>>>
>>>
>>> Vladimir.
>>>
>>>



-- 
Sincerely yours,
-- Daniil