Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Florent,

Florent Hivert 
<>
 writes:

> One great benefit of boolean reflection when trying to prove combinatorics 
> is
> that, Coq is able to automatically decide the truth of many particular cases
> which are omnipresent in there. My experience is that it is quite helpful
> here. However when playing with finset, I can't manage to compute
> anything... Here is an example. There is only one partition of the empty 
> set,
> the empty set itself.
>
> Lemma blu : [set p | partition p [set: 'I_0]] == [set set0].
> Proof.
>   compute.
>
> Ten minutes later I stopped Coq which has exhausted the 32GB of memory of my
> computer. Is this expected ? Is there a workaround ?

Indeed this question has come before on the list, see for example
[1]. On a related note, it is really a pity that the Inria mailserver
forbids google indexing, this effectively makes searching the archives
almost impossible, greatly diminishing the utility of this discussion
forum.

Regarding your question, my personal guess (given that I was not
involved with the development of the libraries) is some parts of
ssreflect are not intended for computation, but for constructive
mathematics, where is usually enough to be computable "in theory".

Indeed, a {set T} is a {ffun T -> bool}, which indeed makes the set
effective very suitable for computation due to efficiency concerns. Note
that this is however a very nice representation to do mathematics, for
instance the intersection of two sets is:

setI A B ≡ λ e → A e && B e

etc...

The same story applies to matrices, etc... I believe that such issues
are well documented in papers and posts by ssreflect authors, but maybe
it would make sense to summarize them in a central place such as a FAQ
section in the wiki.

I'm afraid I am not an expert on the domain of making ssrcompute, all
that I know is that there has been some work by Cohen, Dénès, and
Mörtberg [2], which if I recall correctly is based on providing special
purpose data representations for computation.

For instance, regarding finset, I just recently witnessed an experiment
where two algorithms were written, one using finset and the other using
Coq MSets, then proved equivalent, which was immediate. Then, proofs
were done in ssreflect, which turned out to be a great advantage.

IMVHO, even if hacky, this approach didn't work out too bad. I could
send you some drafty code off-list if you are interested.

Best regards,
Emilio


[1] https://sympa.inria.fr/sympa/arc/ssreflect/2014-11/msg00007.html
[2] http://www.maximedenes.fr/download/refinements.pdf