Merge pull request #23 from pi8027/ci

Update CI and doc, and add Cyril as an author
pi8027 · Mar 20, 2024 · 2b9fd27 · 2b9fd27
2 parents 08cc859 + cf33b05
commit 2b9fd27
Show file tree

Hide file tree

Showing 4 changed files with 134 additions and 85 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -53,9 +53,11 @@ jobs:
           - 'mathcomp/mathcomp:2.2.0-coq-8.16'
           - 'mathcomp/mathcomp:2.2.0-coq-8.17'
           - 'mathcomp/mathcomp:2.2.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.17'
           - 'mathcomp/mathcomp-dev:coq-8.18'
+          - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:

diff --git a/README.md b/README.md
@@ -6,51 +6,64 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/pi8027/stablesort/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/pi8027/stablesort/actions?query=workflow:"Docker%20CI"
-
-
-
-
-This library provides two kinds of optimized mergesort functions written in
-Coq.
-The first kind is non-tail-recursive mergesort functions. In the call-by-need
-evaluation, they allow us to compute the first k smallest elements of a list
-of length n in the optimal O(n + k log k) time complexity of the partial and
-incremental sorting problems. However, the non-tail-recursive merge function
-linearly consumes the call stack and triggers a stack overflow in the
-call-by-value evaluation.
-The second kind is tail-recursive mergesort functions and thus solves the
-above issue in the call-by-value evaluation. However, it does not allow us to
-compute the output incrementally in the optimal O(n + k log k) time regardless
-of the evaluation strategy.
-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.
-
-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
+[docker-action-shield]: https://github.com/pi8027/stablesort/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/pi8027/stablesort/actions/workflows/docker-action.yml
+
+
+
+
+This library provides a generic and modular way to prove the correctness,
+including stability, of several mergesort functions. The correctness lemmas in
+this library are overloaded using a canonical structure
+(`StableSort.function`). This structure characterizes stable mergesort
+functions, say `sort`, by its abstract version `asort` parameterized over the
+type of sorted lists and its operators such as merge, the relational
+parametricity of `asort`, and two equational properties that `asort`
+instantiated with merge and concatenation are `sort` and the identity
+function, respectively, which intuitively mean that replacing merge with
+concatenation turns `sort` into the identity function.
+From this characterization, we derive an induction principle over
+traces—binary trees reflecting the underlying divide-and-conquer structure of
+mergesort—to reason about the relation between the input and output of
+`sort`, and the naturality of `sort`. These two properties are sufficient to
+deduce several correctness results of mergesort, including stability. Thus,
+one may prove the stability of a new sorting function by defining its abstract
+version, proving the relational parametricity of the latter using the
+parametricity translation (the Paramcoq plugin), and manually providing the
 equational properties.
 
+As an application of the above proof methodology, this library provides two
+kinds of optimized mergesorts.
+The first kind is non-tail-recursive mergesort. In call-by-need evaluation,
+they allow us to compute the first k smallest elements of a list of length n
+in the optimal O(n + k log k) time complexity of the partial and incremental
+sorting problems. However, the non-tail-recursive merge function linearly
+consumes the call stack and triggers a stack overflow in call-by-value
+evaluation.
+The second kind is tail-recursive mergesorts and thus solves the above issue
+in call-by-value evaluation. However, it does not allow us to compute the
+output incrementally regardless of the evaluation strategy.
+Therefore, there is a performance trade-off between non-tail-recursive and
+tail-recursive mergesorts, and the best mergesort function for lists depends
+on the situation, in particular, the evaluation strategy and whether it should
+be incremental or not.
+In addition, each of the above two kinds of mergesort functions has a smooth
+(also called natural) variant of mergesort, which takes advantage of sorted
+slices in the input.
+
 ## Meta
 
 - Author(s):
   - Kazuhiko Sakaguchi (initial)
+  - Cyril Cohen
 - License: [CeCILL-B Free Software License Agreement](CeCILL-B)
 - 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 namespace: `stablesort`
-- Related publication(s): none
+- Related publication(s):
+  - [A bargain for mergesorts (functional pearl) — How to prove your mergesort correct and stable, almost for free](https://arxiv.org/abs/2403.08173) doi:[10.48550/arXiv.2403.08173](https://doi.org/10.48550/arXiv.2403.08173)
 
 ## Building and installation instructions
 

diff --git a/coq-stablesort.opam b/coq-stablesort.opam
@@ -12,33 +12,44 @@ license: "CECILL-B"
 
 synopsis: "Stable sort algorithms and their stability proofs in Coq"
 description: """
-This library provides two kinds of optimized mergesort functions written in
-Coq.
-The first kind is non-tail-recursive mergesort functions. In the call-by-need
-evaluation, they allow us to compute the first k smallest elements of a list
-of length n in the optimal O(n + k log k) time complexity of the partial and
-incremental sorting problems. However, the non-tail-recursive merge function
-linearly consumes the call stack and triggers a stack overflow in the
-call-by-value evaluation.
-The second kind is tail-recursive mergesort functions and thus solves the
-above issue in the call-by-value evaluation. However, it does not allow us to
-compute the output incrementally in the optimal O(n + k log k) time regardless
-of the evaluation strategy.
-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.
+This library provides a generic and modular way to prove the correctness,
+including stability, of several mergesort functions. The correctness lemmas in
+this library are overloaded using a canonical structure
+(`StableSort.function`). This structure characterizes stable mergesort
+functions, say `sort`, by its abstract version `asort` parameterized over the
+type of sorted lists and its operators such as merge, the relational
+parametricity of `asort`, and two equational properties that `asort`
+instantiated with merge and concatenation are `sort` and the identity
+function, respectively, which intuitively mean that replacing merge with
+concatenation turns `sort` into the identity function.
+From this characterization, we derive an induction principle over
+traces—binary trees reflecting the underlying divide-and-conquer structure of
+mergesort—to reason about the relation between the input and output of
+`sort`, and the naturality of `sort`. These two properties are sufficient to
+deduce several correctness results of mergesort, including stability. Thus,
+one may prove the stability of a new sorting function by defining its abstract
+version, proving the relational parametricity of the latter using the
+parametricity translation (the Paramcoq plugin), and manually providing the
+equational properties.
 
-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."""
+As an application of the above proof methodology, this library provides two
+kinds of optimized mergesorts.
+The first kind is non-tail-recursive mergesort. In call-by-need evaluation,
+they allow us to compute the first k smallest elements of a list of length n
+in the optimal O(n + k log k) time complexity of the partial and incremental
+sorting problems. However, the non-tail-recursive merge function linearly
+consumes the call stack and triggers a stack overflow in call-by-value
+evaluation.
+The second kind is tail-recursive mergesorts and thus solves the above issue
+in call-by-value evaluation. However, it does not allow us to compute the
+output incrementally regardless of the evaluation strategy.
+Therefore, there is a performance trade-off between non-tail-recursive and
+tail-recursive mergesorts, and the best mergesort function for lists depends
+on the situation, in particular, the evaluation strategy and whether it should
+be incremental or not.
+In addition, each of the above two kinds of mergesort functions has a smooth
+(also called natural) variant of mergesort, which takes advantage of sorted
+slices in the input."""
 
 build: [make "-j%{jobs}%"]
 install: [make "install"]
@@ -53,4 +64,5 @@ tags: [
 ]
 authors: [
   "Kazuhiko Sakaguchi"
+  "Cyril Cohen"
 ]
diff --git a/meta.yml b/meta.yml
@@ -9,37 +9,55 @@ synopsis: >-
   Stable sort algorithms and their stability proofs in Coq
 
 description: |-
-  This library provides two kinds of optimized mergesort functions written in
-  Coq.
-  The first kind is non-tail-recursive mergesort functions. In the call-by-need
-  evaluation, they allow us to compute the first k smallest elements of a list
-  of length n in the optimal O(n + k log k) time complexity of the partial and
-  incremental sorting problems. However, the non-tail-recursive merge function
-  linearly consumes the call stack and triggers a stack overflow in the
-  call-by-value evaluation.
-  The second kind is tail-recursive mergesort functions and thus solves the
-  above issue in the call-by-value evaluation. However, it does not allow us to
-  compute the output incrementally in the optimal O(n + k log k) time regardless
-  of the evaluation strategy.
-  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.
-
-  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
+  This library provides a generic and modular way to prove the correctness,
+  including stability, of several mergesort functions. The correctness lemmas in
+  this library are overloaded using a canonical structure
+  (`StableSort.function`). This structure characterizes stable mergesort
+  functions, say `sort`, by its abstract version `asort` parameterized over the
+  type of sorted lists and its operators such as merge, the relational
+  parametricity of `asort`, and two equational properties that `asort`
+  instantiated with merge and concatenation are `sort` and the identity
+  function, respectively, which intuitively mean that replacing merge with
+  concatenation turns `sort` into the identity function.
+  From this characterization, we derive an induction principle over
+  traces—binary trees reflecting the underlying divide-and-conquer structure of
+  mergesort—to reason about the relation between the input and output of
+  `sort`, and the naturality of `sort`. These two properties are sufficient to
+  deduce several correctness results of mergesort, including stability. Thus,
+  one may prove the stability of a new sorting function by defining its abstract
+  version, proving the relational parametricity of the latter using the
+  parametricity translation (the Paramcoq plugin), and manually providing the
   equational properties.
 
+  As an application of the above proof methodology, this library provides two
+  kinds of optimized mergesorts.
+  The first kind is non-tail-recursive mergesort. In call-by-need evaluation,
+  they allow us to compute the first k smallest elements of a list of length n
+  in the optimal O(n + k log k) time complexity of the partial and incremental
+  sorting problems. However, the non-tail-recursive merge function linearly
+  consumes the call stack and triggers a stack overflow in call-by-value
+  evaluation.
+  The second kind is tail-recursive mergesorts and thus solves the above issue
+  in call-by-value evaluation. However, it does not allow us to compute the
+  output incrementally regardless of the evaluation strategy.
+  Therefore, there is a performance trade-off between non-tail-recursive and
+  tail-recursive mergesorts, and the best mergesort function for lists depends
+  on the situation, in particular, the evaluation strategy and whether it should
+  be incremental or not.
+  In addition, each of the above two kinds of mergesort functions has a smooth
+  (also called natural) variant of mergesort, which takes advantage of sorted
+  slices in the input.
+
+publications:
+- pub_url: https://arxiv.org/abs/2403.08173
+  pub_title: A bargain for mergesorts (functional pearl) — How to prove your mergesort correct and stable, almost for free
+  pub_doi: 10.48550/arXiv.2403.08173
+
 authors:
 - name: Kazuhiko Sakaguchi
   initial: true
+- name: Cyril Cohen
+  initial: false
 
 opam-file-maintainer: [email protected]
 
@@ -127,12 +145,16 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-dev'
   repo: 'mathcomp/mathcomp'
 - version: 'coq-8.17'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.18'
   repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.19'
+  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'