Ssreflect Users Discussion List

[Georges Gonthier <>]

  Hi Florent,
Let me add some "insider's insight" to Emilio's generically correct response.
   The reason many mathematical  definitions in mathcomp are opaque is that 
the heuristics implemented by the Coq type checker for comparing inferred and 
expected types tends to handle even moderately nested transparent definitions 
very poorly. Specifically, Coq uses a combination of lazy constant expansion 
and call-by-need  head (weak) reduction. In abstract instances that do not 
compute to a simple value, this tends to expand types into 
exponentially-large call trees, especially when trying to show that terms are 
not equal (e.g., when trying a reflexivity proof). Making definitions opaque 
mitigates this problem and makes the library usable, at the cost of having to 
switch algorithms to do a proof by computation.
   As was pointed out, the vernacular Opaque directive is mostly ignored by 
the type checker. The safest way to render a definition opaque is via module 
signature ascription, but this is rather inconvenient (for instance, it can't 
be done inside a Section), and so is done only for certain "key" definitions, 
such as bigop, subset, or card.
   In most cases the library just uses the locked_with function to hide the 
definition behind a match on an opaque "key". This ensures the definition if 
never unfolded by the type checker heuristics, but unfortunately this is not 
sufficient to block the compute strategy - eager definition expansion with 
strong call-by-value. Hence the compute in your proof attempts to create a 
huge term.
  I hope this helps,
Georges

-----Original Message-----
From: 

 
[mailto:]
 On Behalf Of Emilio Jesús Gallego Arias
Sent: 12 February 2016 00:00
To: Florent Hivert 
<>
Cc: 

Subject: Re: [ssreflect] Coq computing with sets...

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://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fsympa.inria.fr%2fsympa%2farc%2fssreflect%2f2014-11%2fmsg00007.html&data=01%7c01%7cgonthier%40064d.mgd.microsoft.com%7cfaf5aeea389e4821f33b08d3333f9e39%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=4jPTlIzo3NqP%2fZ3BzEw3vq7HlY3iRWnxoXhppt6PANc%3d
[2] 
https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww.maximedenes.fr%2fdownload%2frefinements.pdf&data=01%7c01%7cgonthier%40064d.mgd.microsoft.com%7cfaf5aeea389e4821f33b08d3333f9e39%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=70HD8YgmLQfcvdL4rL3HMzTyrDiD1gfErvMVfQsTmcQ%3d