Remove some compatibility hacks

.github/workflows/docker-action.yml

@@ -17,11 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.12.0-coq-8.10'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.11'
           - 'mathcomp/mathcomp:1.13.0-coq-8.12'
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'

README.md

@@ -42,9 +42,9 @@ by providing a lemma corresponding to the binary tree construction.
 - Author(s):
   - Kazuhiko Sakaguchi (initial)
 - License: [CeCILL-B Free Software License Agreement](CeCILL-B)
-- Compatible Coq versions: 8.10 or later
+- Compatible Coq versions: 8.11 or later
 - Additional dependencies:
-  - [MathComp](https://math-comp.github.io) 1.12.0 or later
+  - [MathComp](https://math-comp.github.io) 1.13.0 or later
   - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
 - Coq namespace: `stablesort`
 - Related publication(s): none

coq-stablesort.opam

@@ -40,8 +40,8 @@ by providing a lemma corresponding to the binary tree construction."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.10"}
-  "coq-mathcomp-ssreflect" {>= "1.12.0"}
+  "coq" {>= "8.11"}
+  "coq-mathcomp-ssreflect" {>= "1.13.0"}
   "coq-paramcoq" {>= "1.1.3"}
 ]
 

meta.yml

@@ -46,22 +46,12 @@ license:
   file: CeCILL-B
 
 supported_coq_versions:
-  text: 8.10 or later
-  opam: '{>= "8.10"}'
+  text: 8.11 or later
+  opam: '{>= "8.11"}'
 
 tested_coq_nix_versions:
 
 tested_coq_opam_versions:
-- version: '1.12.0-coq-8.10'
-  repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.11'
-  repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.12'
-  repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.11'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.12'
@@ -100,9 +90,9 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.12.0"}'
+    version: '{>= "1.13.0"}'
   description: |-
-    [MathComp](https://math-comp.github.io) 1.12.0 or later
+    [MathComp](https://math-comp.github.io) 1.13.0 or later
 - opam:
     name: coq-paramcoq
     version: '{>= "1.1.3"}'

theories/mathcomp_ext.v

@@ -4,68 +4,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Definition pairwise {T : Type} (r : rel T) :=
-  fix pairwise (xs : seq T) : bool :=
-    if xs is x :: xs then all (r x) xs && pairwise xs else true.
-
-Lemma pairwise_cat {T : Type} (r : rel T) (xs ys : seq T) :
-  pairwise r (xs ++ ys) = [&& allrel r xs ys, pairwise r xs & pairwise r ys].
-Proof. by elim: xs => //= x xs ->; rewrite all_cat -!andbA; bool_congr. Qed.
-
-Lemma pairwise_map {T T' : Type} (f : T' -> T) (r : rel T) xs :
-  pairwise r (map f xs) = pairwise (relpre f r) xs.
-Proof. by elim: xs => //= x xs ->; rewrite all_map. Qed.
-
-Lemma mergeA (T : Type) (leT : rel T) :
-  total leT -> transitive leT -> associative (merge leT).
-Proof.
-move=> leT_total leT_tr.
-elim=> // x xs IHxs; elim=> // y ys IHys; elim=> [|z zs IHzs] /=.
-  by case: ifP.
-case: ifP; case: ifP => /= lexy leyz.
-- by rewrite lexy (leT_tr _ _ _ lexy leyz) -IHxs /= leyz.
-- by rewrite lexy leyz -IHys.
-- case: ifP => lexz; first by rewrite -IHxs //= leyz.
-  by rewrite -!/(merge _ (_ :: _)) IHzs /= lexy.
-- suff->: leT x z = false by rewrite leyz // -!/(merge _ (_ :: _)) IHzs /= lexy.
-by apply/contraFF/leT_tr: leyz; have := leT_total x y; rewrite lexy.
-Qed.
-
-Lemma all_merge (T : Type) (P : {pred T}) (leT : rel T) (s1 s2 : seq T) :
-  all P (merge leT s1 s2) = all P s1 && all P s2.
-Proof.
-elim: s1 s2 => //= x s1 IHs1; elim=> [|y s2 IHs2]; rewrite ?andbT //=.
-by case: ifP => _; rewrite /= ?IHs1 ?IHs2 //=; bool_congr.
-Qed.
-
-Lemma allrel_merge (T : Type) (leT : rel T) s1 s2 :
-  allrel leT s1 s2 -> merge leT s1 s2 = s1 ++ s2.
-Proof.
-elim: s1 s2 => [|x s1 IHs1] [|y s2]; rewrite ?cats0 //=.
-by rewrite allrel_consl /= -andbA => /and3P [-> _ /IHs1->].
-Qed.
-
-Lemma eq_sorted (T : Type) (e e' : rel T) : e =2 e' -> sorted e =1 sorted e'.
-Proof. by move=> ee' [] //; apply: eq_path. Qed.
-
-Lemma sorted_pairwise (T : Type) (leT : rel T) :
-  transitive leT -> forall s : seq T, sorted leT s = pairwise leT s.
-Proof.
-by move=> leT_tr; elim => //= x s <-; rewrite path_sortedE.
-Qed.
-
-Lemma pairwise_sorted (T : Type) (leT : rel T) (s : seq T) :
-  pairwise leT s -> sorted leT s.
-Proof. by elim: s => //= x s IHs /andP[/path_min_sorted -> /IHs]. Qed.
-
-Lemma path_relI (T : Type) (leT leT' : rel T) (x : T) (s : seq T) :
-  path [rel x y | leT x y && leT' x y] x s = path leT x s && path leT' x s.
-Proof. by elim: s x => //= y s IHs x; rewrite andbACA IHs. Qed.
-
-Lemma sorted_relI (T : Type) (leT leT' : rel T) (s : seq T) :
-  sorted [rel x y | leT x y && leT' x y] s = sorted leT s && sorted leT' s.
-Proof. by case: s; last apply: path_relI. Qed.
-
 Lemma nilp_rev (T : Type) (s : seq T) : nilp (rev s) = nilp s.
 Proof. by move: s (rev s) (size_rev s) => [|? ?] []. Qed.
 

theories/stablesort.v

@@ -6,12 +6,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-(* COMPATIBILITY HACK: [mathcomp_ext] has to be imported *before* MathComp    *)
-(* libraries since [pairwise] has to be imported from MathComp if available.  *)
-(* However, [eq_sorted] has to be imported from [mathcomp_ext] to override a  *)
-(* deprecation alias in MathComp; hence, we declare the following notation.   *)
-Local Notation eq_sorted := mathcomp_ext.eq_sorted (only parsing).
-
 (******************************************************************************)
 (* The abstract interface for stable (merge)sort algorithms                   *)
 (******************************************************************************)