From e69e119aae04e19b40942b673f82266853ed80f9 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Mon, 28 Feb 2022 14:37:00 +0900 Subject: [PATCH] Remove some compatibility hacks --- .github/workflows/docker-action.yml | 5 --- README.md | 4 +- coq-stablesort.opam | 4 +- meta.yml | 18 ++------- theories/mathcomp_ext.v | 62 ----------------------------- theories/stablesort.v | 6 --- 6 files changed, 8 insertions(+), 91 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 4d2622a..6aafc76 100644 --- a/.github/workflows/docker-action.yml +++ b/.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' diff --git a/README.md b/README.md index bec2a11..656145a 100644 --- a/README.md +++ b/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 diff --git a/coq-stablesort.opam b/coq-stablesort.opam index 91b6816..36cc758 100644 --- a/coq-stablesort.opam +++ b/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"} ] diff --git a/meta.yml b/meta.yml index e4dec8d..6d8c2e2 100644 --- a/meta.yml +++ b/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"}' diff --git a/theories/mathcomp_ext.v b/theories/mathcomp_ext.v index 863d294..9eb8af6 100644 --- a/theories/mathcomp_ext.v +++ b/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. diff --git a/theories/stablesort.v b/theories/stablesort.v index 30a49de..9242610 100644 --- a/theories/stablesort.v +++ b/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 *) (******************************************************************************)