remove Heap, PermutEq, and PermutSetoid from Sorting

[andres-erbsen]

• Added changelog.
• Added / updated documentation.
• Opened overlay pull requests.

[andres-erbsen]

@fblanqui what's your opinion on PermutSetoid? These files are marked as deprecated in stdlib, but CoLoR uses them, and somewhat seriously it seems. Do you think they are worth recommending to new users (by keeping them in stdlib)? My own experience is quite limited, but I wonder whether relation composition of Forall2 SetoidEq and Permutation would be friendlier to work with than PermutSetoid.

[fblanqui]

Hi. I don't have any opinion on that yet. I didn't write the CoLoR files that use PermutSetoid. What I understand is that PermutSetoid.permutation defines permutation of two lists of elements of A modulo an equivalence relation on A, by using Multiset.meq. But this is also more directly defined in SetoidPermutation. But this probably requires to adapt a few proofs.

16:26 ~/src/color (master) gc PermutSetoid|cat
./Util/Relation/SCCTopoOrdering.v:13:From Coq Require Import Permutation Multiset Heap PermutSetoid.
./Util/List/ListPermutation.v:14:From Coq Require Export Permutation PermutSetoid Multiset.
./Util/Multiset/MultisetList.v:13:From Coq Require Import Permutation PermutSetoid Lia Multiset.
./DP/ASCCUnion.v:12:From Coq Require Import Permutation Multiset Setoid PermutSetoid.

[andres-erbsen]

Ah, I was somehow not noticing SetoidPermutation when I reached out. Given that it already exists in stdlib, for more than a decade, my sense is that for stdlib the best plan would be to go ahead with the removal of PermutSetoid.

Now, what would be good for CoLoR in this scenario? Would you want to take over PermutSetoid, or remove the reliance on it?

[fblanqui]

I don't know, and I don't have much time to dedicate to this at the moment. The simplest is probably to copy and paste PermutSetoid in CoLoR I guess.