Merge pull request #29 from pi8027/count_sort_args

Change the order of arguments of `count_sort` to align with MathComp

.github/workflows/docker-action.yml

@@ -56,13 +56,17 @@ jobs:
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-8.20'
           - 'mathcomp/mathcomp:2.2.0-coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.18'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.3.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-8.20'
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp-dev:rocq-prover-9.0'
+          - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-stablesort.opam'

coq-stablesort.opam

@@ -2,7 +2,7 @@
 # Follow the instructions on https://github.com/coq-community/templates to regenerate.
 
 opam-version: "2.0"
-maintainer: "kazuhiko.sakaguchi@inria.fr"
+maintainer: "kazuhiko.sakaguchi@ens-lyon.fr"
 version: "dev"
 
 homepage: "https://github.com/pi8027/stablesort"

meta.yml

@@ -59,7 +59,7 @@ authors:
 - name: Cyril Cohen
   initial: false
 
-opam-file-maintainer: kazuhiko.sakaguchi@inria.fr
+opam-file-maintainer: kazuhiko.sakaguchi@ens-lyon.fr
 
 license:
   fullname: CeCILL-B Free Software License Agreement
@@ -151,13 +151,21 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-dev'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.18'
-  repo: 'mathcomp/mathcomp-dev'
+- version: '2.3.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-8.20'
+  repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
 - version: 'coq-8.19'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.20'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-dev'
+- version: 'rocq-prover-9.0'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'rocq-prover-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:

theories/stablesort.v

@@ -1067,7 +1067,7 @@ Qed.
 
 End SortSeq.
 
-Lemma count_sort (T : Type) (p : pred T) (leT : rel T) (s : seq T) :
+Lemma count_sort (T : Type) (leT : rel T) (p : pred T) (s : seq T) :
   count p (sort _ leT s) = count p s.
 Proof.
 by elim/sort_ind: (sort _ leT s) => // xs xs' IHxs ys ys' IHys;
@@ -1076,7 +1076,7 @@ Qed.
 
 Lemma size_sort (T : Type) (leT : rel T) (s : seq T) :
   size (sort _ leT s) = size s.
-Proof. exact: (count_sort predT). Qed.
+Proof. exact: (count_sort _ predT). Qed.
 
 Lemma sort_nil (T : Type) (leT : rel T) : sort _ leT [::] = [::].
 Proof. by case: (sort _) (size_sort leT [::]). Qed.
@@ -1418,7 +1418,7 @@ Arguments sort_pairwise_stable    sort {T leT leT'} leT_total {s} _.
 Arguments sort_pairwise_stable_in sort {T P leT leT'} leT_total {s} _ _.
 Arguments sort_stable             sort {T leT leT'} leT_total leT'_tr {s} _.
 Arguments sort_stable_in          sort {T P leT leT'} leT_total leT'_tr {s} _ _.
-Arguments count_sort              sort {T} p leT s.
+Arguments count_sort              sort {T} leT p s.
 Arguments size_sort               sort {T} leT s.
 Arguments sort_nil                sort {T} leT.
 Arguments all_sort                sort {T} p leT s.