The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

>> Also, I've found that as a practical matter, it's more difficult to use 
>> "if and
>> only if" results than the equivalent pair of split results, because "apply 
>> ->"
>> and "apply <-" aren't as good at unification as the stock "apply" (in
>> particular they don't accept "with" specifiers).  Is this something that 
>> should
>> be mentioned in the guidelines, to split up "if and only if" results?
>
> I wonder if this is best fixed by improving apply -> and apply <-
> rather than working around them in the library.

I agree with Tom: cluttering the name-space with partial lemmas (from
left to right, and from right to left) seems to be a not-that-good
design choice. E.g., in MSets, (where lemmas are stated as
equivalences) there seem to have been improvements regarding that,
w.r.t. FSets (where lemmas where stated as l2r and r2l versions).

I have little experience of problems with apply <- , apply ->, But i
think this is because I use rewrite a lot to apply such equivalences.

With best regards,
Thomas