Ssreflect Users Discussion List

[Andrej Bauer <>]

Enrico,

I think it is best if we joing efforts. I can add whatever is needed
back into the standard library. There is equality (see
HoTT/theories/Paths.v), and Coq knows how to rewrite with respect to
it, but the codomain of equality is not Prop. I think this is doable.

With kind regards,

Andrej

On Wed, Oct 10, 2012 at 11:45 AM, Enrico Tassi <> wrote:
> On Wed, Oct 10, 2012 at 10:42:15AM -0400, Andrej Bauer wrote:
>> https://github.com/HoTT/HoTT and other repositories in the HoTT account.
>>
>> Bas tells me there is an ssr plugin. I think that's what I am really
>> asking for. Where can I read more about it?
>
> This is the last official release (1.4).
>
>   
> https://www.msr-inria.inria.fr/Projects/math-components/index_html#download
>
> It includes a few .ml sources in src/ and the libraries in theories/.
> The .ml files are used to build ssreflect.cmxs, a plugin that Coq is
> able to load. We have versions of these .ml files that compile on Coq
> trunk.
>
> Most tactics require some definitions/lemmas that are in
> ssreflect.v (that also takes care of loading the cmxs file).
> A regular user would "Require Import ssreflect" to load at once the
> plugin and its minimal environment of lemmas/defs.
> The rest of theories/ can be discarded.
>
> Unfortunately a quick check reveals that even these minimal definitions
> rely on some concepts of the standard library of Coq, for example
> ssreflect.v Requires Bool, uses the <-> notation and the standard equality.
>
> So even the minimal "ssreflect plugin" requires some careful inspection
> and cleanup to be used in your HoTT Coq branch where, if I got it right,
> the directory theories/ has been wiped out. But I guess you have the
> same problem with standard Coq tactics, since many of them rely on the
> content of the standard library...
>
> Tomorrow I will try to build HoTT/Coq + HoTT/HoTT and see if it is
> feasible to make the plugin work in this setting (or at least estimate
> the effort).
> A pointer to valid substitutes for bool, logical connectives and
> equality (one that can be eliminated, on Set I guess) would be
> appreciated.
>
> If you can't wait here a link to our regression/test system, that
> collects the files used in the last successful build. But you will have to
> cleanup ssreflect.v all by yourself, and ssreflect.ml4 surely contains
> references to standard lemmas too, like the elimination principle for
> equality, needed to implement rewrite.
>
>   
> http://ssr.msr-inria.inria.fr/hudson/job/ssr_trunk/lastSuccessfulBuild/artifact/ssr/ssreflect/ssreflect1.3_trunk/
>
> Cheers
> --
> Enrico Tassi