Get rid of traces

.github/workflows/docker-action.yml

@@ -17,13 +17,9 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.13.0-coq-8.11'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.12'
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.11'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.12'
           - 'mathcomp/mathcomp:1.14.0-coq-8.13'
           - 'mathcomp/mathcomp:1.14.0-coq-8.14'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
@@ -37,16 +33,21 @@ jobs:
           - 'mathcomp/mathcomp:1.16.0-coq-8.16'
           - 'mathcomp/mathcomp:1.16.0-coq-8.17'
           - 'mathcomp/mathcomp:1.16.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.16.0-coq-dev'
           - 'mathcomp/mathcomp:1.17.0-coq-8.15'
           - 'mathcomp/mathcomp:1.17.0-coq-8.16'
           - 'mathcomp/mathcomp:1.17.0-coq-8.17'
           - 'mathcomp/mathcomp:1.17.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.17.0-coq-dev'
+          - 'mathcomp/mathcomp:1.18.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.18.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
+          - 'mathcomp/mathcomp:1.18.0-coq-dev'
           - 'mathcomp/mathcomp:2.0.0-coq-8.16'
           - 'mathcomp/mathcomp:2.0.0-coq-8.17'
           - 'mathcomp/mathcomp:2.0.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.0.0-coq-dev'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.1.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.16'
           - 'mathcomp/mathcomp-dev:coq-8.17'
           - 'mathcomp/mathcomp-dev:coq-8.18'

Make

@@ -1,7 +1,6 @@
 theories/mathcomp_ext.v
 theories/param.v
 theories/stablesort.v
-theories/top_down.v
 
 -R theories stablesort
 

README.md

@@ -28,21 +28,24 @@ The point is that the best mergesort function for lists depends on the
 situation, in particular, the evaluation strategy and whether it should be
 incremental or not.
 
-To prove the correctness (including stability) of these mergesort functions,
-this library also provides a generic way to prove these properties. The
-correctness lemmas provided in this library are overloaded using a canonical
-structure (`StableSort.function`). Stable sort functions are characterized in
-this interface by the parametricity axiom and binary trees representing the
-divide-and-conquer structure of sort. Thus, one may prove the stability of a
-new sorting function by using the parametricity translation (Paramcoq) and
-by providing a lemma corresponding to the binary tree construction.
+This library also provides a generic way to prove the correctness (including
+stability) of these mergesort functions. The correctness lemmas in this
+library are overloaded using a canonical structure (`StableSort.function`).
+This structure characterizes stable sort functions, say `sort`, by an abstract
+version of the sort function `asort` parameterized over the type of sorted
+lists and its operators such as merge, the parametricity of `asort`, two
+equational properties that `asort` instantiated with merge and concatenation
+are `sort` and the identity function, respectively. Thus, one may prove the
+stability of a new sorting function by defining its abstract version, using
+the parametricity translation (Paramcoq), and manually providing the
+equational properties.
 
 ## Meta
 
 - Author(s):
   - Kazuhiko Sakaguchi (initial)
 - License: [CeCILL-B Free Software License Agreement](CeCILL-B)
-- Compatible Coq versions: 8.11 or later
+- Compatible Coq versions: 8.13 or later
 - Additional dependencies:
   - [MathComp](https://math-comp.github.io) 1.13.0 or later
   - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later

coq-stablesort.opam

@@ -28,19 +28,22 @@ The point is that the best mergesort function for lists depends on the
 situation, in particular, the evaluation strategy and whether it should be
 incremental or not.
 
-To prove the correctness (including stability) of these mergesort functions,
-this library also provides a generic way to prove these properties. The
-correctness lemmas provided in this library are overloaded using a canonical
-structure (`StableSort.function`). Stable sort functions are characterized in
-this interface by the parametricity axiom and binary trees representing the
-divide-and-conquer structure of sort. Thus, one may prove the stability of a
-new sorting function by using the parametricity translation (Paramcoq) and
-by providing a lemma corresponding to the binary tree construction."""
+This library also provides a generic way to prove the correctness (including
+stability) of these mergesort functions. The correctness lemmas in this
+library are overloaded using a canonical structure (`StableSort.function`).
+This structure characterizes stable sort functions, say `sort`, by an abstract
+version of the sort function `asort` parameterized over the type of sorted
+lists and its operators such as merge, the parametricity of `asort`, two
+equational properties that `asort` instantiated with merge and concatenation
+are `sort` and the identity function, respectively. Thus, one may prove the
+stability of a new sorting function by defining its abstract version, using
+the parametricity translation (Paramcoq), and manually providing the
+equational properties."""
 
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.11"}
+  "coq" {>= "8.13"}
   "coq-mathcomp-ssreflect" {>= "1.13.0"}
   "coq-paramcoq" {>= "1.1.3"}
 ]

meta.yml

@@ -25,14 +25,17 @@ description: |-
   situation, in particular, the evaluation strategy and whether it should be
   incremental or not.
 
-  To prove the correctness (including stability) of these mergesort functions,
-  this library also provides a generic way to prove these properties. The
-  correctness lemmas provided in this library are overloaded using a canonical
-  structure (`StableSort.function`). Stable sort functions are characterized in
-  this interface by the parametricity axiom and binary trees representing the
-  divide-and-conquer structure of sort. Thus, one may prove the stability of a
-  new sorting function by using the parametricity translation (Paramcoq) and
-  by providing a lemma corresponding to the binary tree construction.
+  This library also provides a generic way to prove the correctness (including
+  stability) of these mergesort functions. The correctness lemmas in this
+  library are overloaded using a canonical structure (`StableSort.function`).
+  This structure characterizes stable sort functions, say `sort`, by an abstract
+  version of the sort function `asort` parameterized over the type of sorted
+  lists and its operators such as merge, the parametricity of `asort`, two
+  equational properties that `asort` instantiated with merge and concatenation
+  are `sort` and the identity function, respectively. Thus, one may prove the
+  stability of a new sorting function by defining its abstract version, using
+  the parametricity translation (Paramcoq), and manually providing the
+  equational properties.
 
 authors:
 - name: Kazuhiko Sakaguchi
@@ -46,26 +49,18 @@ license:
   file: CeCILL-B
 
 supported_coq_versions:
-  text: 8.11 or later
-  opam: '{>= "8.11"}'
+  text: 8.13 or later
+  opam: '{>= "8.13"}'
 
 tested_coq_nix_versions:
 
 tested_coq_opam_versions:
-- version: '1.13.0-coq-8.11'
-  repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.12'
-  repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.11'
-  repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.12'
-  repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.14'
@@ -92,8 +87,6 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.16.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-dev'
-  repo: 'mathcomp/mathcomp'
 - version: '1.17.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
 - version: '1.17.0-coq-8.16'
@@ -102,15 +95,27 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.17.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-dev'
+- version: '1.18.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '1.18.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '1.18.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '1.18.0-coq-dev'
   repo: 'mathcomp/mathcomp'
 - version: '2.0.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 - version: '2.0.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
 - version: '2.0.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-dev'
+- version: '2.1.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-dev'
   repo: 'mathcomp/mathcomp'
 - version: 'coq-8.16'
   repo: 'mathcomp/mathcomp-dev'

theories/param.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From Param Require Export Param.
 
 Set Implicit Arguments.
@@ -17,13 +17,16 @@ Parametricity eq.
 Parametricity or.
 Parametricity Acc.
 Parametricity bool.
+Parametricity option.
 Parametricity prod.
 Parametricity nat.
 Parametricity list.
 Parametricity pred.
 Parametricity rel.
 Parametricity BinNums.positive.
 Parametricity BinNums.N.
+Parametricity merge.
+Parametricity rev.
 
 Lemma bool_R_refl b1 b2 : b1 = b2 -> bool_R b1 b2.
 Proof. by case: b1 => <-; constructor. Qed.