Ssreflect Users Discussion List

[Enrico Tassi <>]

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