From dbb98e952893bf64e8cc08616380d46036968127 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 2 Apr 2020 01:03:33 +0200 Subject: [PATCH] compatibility with mathcomp-dev and lost with mathcomp < 1.9.0 (#64) - compatibility with mathcomp-dev and lost with mathcomp < 1.9.0 + updating opam dependencies + adding travis jobs --- .travis.yml | 12 ++++++++---- finmap.v | 20 ++++++++++---------- multiset.v | 6 +++--- opam | 4 ++-- shell.nix | 9 +++++---- 5 files changed, 28 insertions(+), 23 deletions(-) diff --git a/.travis.yml b/.travis.yml index a7233d1..6aac7df 100644 --- a/.travis.yml +++ b/.travis.yml @@ -14,17 +14,21 @@ env: - NJOBS="2" - CONTRIB_NAME="finmap" matrix: - - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.7" - - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.8" - - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.9" - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.7" - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.8" - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.9" - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.10" + - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.11" + - DOCKERIMAGE="mathcomp/mathcomp:1.10.0-coq-8.7" + - DOCKERIMAGE="mathcomp/mathcomp:1.10.0-coq-8.8" + - DOCKERIMAGE="mathcomp/mathcomp:1.10.0-coq-8.9" + - DOCKERIMAGE="mathcomp/mathcomp:1.10.0-coq-8.10" + - DOCKERIMAGE="mathcomp/mathcomp:1.10.0-coq-8.11" - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.7" - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.8" - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.9" -# - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.10" + - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.10" + - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.11" install: | # Prepare the COQ container diff --git a/finmap.v b/finmap.v index 05872bb..f897bd1 100644 --- a/finmap.v +++ b/finmap.v @@ -410,18 +410,18 @@ Variable (K : choiceType). Implicit Types (k : K) (ks : seq K). Definition f (s : seq K) := choose (perm_eq (undup s)) (undup s). Fact perm s : perm_eq (f s) (undup s). -Proof. by rewrite perm_eq_sym chooseP. Qed. +Proof. by rewrite perm_sym chooseP. Qed. Fact uniq s : uniq (f s). -Proof. by rewrite (perm_eq_uniq (perm _)) undup_uniq. Qed. +Proof. by rewrite (perm_uniq (perm _)) undup_uniq. Qed. Fact E (s : seq K) : f s =i s. -Proof. by move=> x; rewrite (perm_eq_mem (perm _)) mem_undup. Qed. +Proof. by move=> x; rewrite (perm_mem (perm _)) mem_undup. Qed. Lemma eq (s s' : seq K) : s =i s' <-> f s = f s'. Proof. split=> [eq_ss'|eq_ss' k]; last by rewrite -E eq_ss' E. rewrite /f; have peq_ss' : perm_eq (undup s) (undup s'). - by apply: uniq_perm_eq; rewrite ?undup_uniq // => x; rewrite !mem_undup. + by apply: uniq_perm; rewrite ?undup_uniq // => x; rewrite !mem_undup. rewrite (@choose_id _ _ _ (undup s')) //=; apply: eq_choose => x /=. -by apply: sym_left_transitive; [exact: perm_eq_sym | exact: (@perm_eq_trans)|]. +by apply: sym_left_transitive; [exact: perm_sym | exact: (@perm_trans)|]. Qed. End SortKeys. End SortKeys. @@ -472,7 +472,7 @@ by apply/eq_sort_keys => x; rewrite -sort_keysE eq_ks_ks' sort_keysE. Qed. Lemma size_sort_keys ks : size (sort_keys ks) = size (undup ks). -Proof. exact: perm_eq_size. Qed. +Proof. exact: perm_size. Qed. End ChoiceKeys. Arguments eq_sort_keys {K s s'}. @@ -1115,7 +1115,7 @@ Lemma enum_imfset2 (T1 : choiceType) (T2 : T1 -> choiceType) [seq f x y | x <- enum_finmem p1, y <- enum_finmem (p2 x)]. Proof. move=> f_inj; rewrite unlock. -apply: uniq_perm_eq => [||i]; rewrite ?seq_fset_uniq ?seq_fsetE //. +apply: uniq_perm => [||i]; rewrite ?seq_fset_uniq ?seq_fsetE //. rewrite allpairs_uniq_dep ?enum_finmem_uniq//. by move=> x; rewrite enum_finmem_uniq. move=> t0 t0' /allpairsPdep[t1 [t2]]; rewrite !enum_finmemE => -[tp1 tp2 ->/=]. @@ -2127,7 +2127,7 @@ Proof. by rewrite enumT unlock. Qed. Lemma enum_fset1 (T : choiceType) (x : T) : enum [finType of [fset x]] = [:: [`fset11 x]]. Proof. -apply/perm_eq_small=> //; apply/uniq_perm_eq => //. +apply/perm_small_eq=> //; apply/uniq_perm => //. by apply/enum_uniq. case=> [y hy]; rewrite mem_seq1 mem_enum /in_mem /=. by rewrite eqE /=; rewrite in_fset1 in hy. @@ -2266,7 +2266,7 @@ Proof. by rewrite big_seq_fsetE big_fset1. Qed. End BigFSet. -Notation eq_big_imfset := (eq_big_perm _ (enum_imfset _ _)). +Notation eq_big_imfset := (perm_big _ (enum_imfset _ _)). Section BigComFSet. Variable (R : Type) (idx : R) (op : Monoid.com_law idx). @@ -2360,7 +2360,7 @@ End BigComFSet. Arguments big_fsetD1 {R idx op I} a [A F]. -Notation eq_big_imfset2 := (eq_big_perm _ (enum_imfset2 _ _)). +Notation eq_big_imfset2 := (perm_big _ (enum_imfset2 _ _)). Section BigComImfset2. Variables (R : Type) (idx : R) (op : Monoid.com_law idx) diff --git a/multiset.v b/multiset.v index 9579f61..af99c72 100644 --- a/multiset.v +++ b/multiset.v @@ -230,7 +230,7 @@ Qed. Lemma perm_undup_mset A : perm_eq (undup A) (finsupp A). Proof. -apply: uniq_perm_eq; rewrite ?undup_uniq // => a. +apply: uniq_perm; rewrite ?undup_uniq // => a. by rewrite mem_undup msuppE. Qed. @@ -242,7 +242,7 @@ Lemma big_mset X P F : \big[op/idx]_(i <- X | P i) F i = \big[op/idx]_(i <- finsupp X | P i) iterop (X i) op (F i) idx. Proof. -rewrite [in RHS](eq_big_perm (undup X)) 1?perm_eq_sym ?perm_undup_mset//. +rewrite [in RHS](perm_big (undup X)) 1?perm_sym ?perm_undup_mset//. rewrite -[in LHS]big_undup_iterop_count; apply: eq_bigr => i _. by rewrite count_mem_mset. Qed. @@ -271,7 +271,7 @@ Proof. by apply/msetP=> a; rewrite mset_seqE count_mem_mset. Qed. Lemma eq_seq_msetP s s' : reflect (seq_mset s = seq_mset s') (perm_eq s s'). Proof. -apply: (iffP idP) => [/perm_eqP perm_ss'|eq_ss']. +apply: (iffP idP) => [/permP perm_ss'|eq_ss']. by apply/msetP => a; rewrite !mset_seqE perm_ss'. by apply/allP => a _ /=; rewrite -!mset_seqE eq_ss'. Qed. diff --git a/opam b/opam index aedd18a..c61f489 100644 --- a/opam +++ b/opam @@ -12,8 +12,8 @@ build: [ make "-j" "%{jobs}%" ] install: [ make "install" ] depends: [ - "coq" { (>= "8.7" & < "8.11~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "1.8.0" & < "1.11~") | (= "dev") } + "coq" { (>= "8.7" & < "8.12~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "1.9.0" & < "1.12~") | (= "dev") } "coq-mathcomp-bigenough" { (>= "1.0.0" & < "1.1~") | (= "dev") } ] tags: [ "keyword:finmap" "keyword:finset" "keyword:multiset" "keyword:order"] diff --git a/shell.nix b/shell.nix index bea2794..edb0dce 100644 --- a/shell.nix +++ b/shell.nix @@ -1,10 +1,10 @@ {withEmacs ? false, nixpkgs ? (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/650a295621b27c4ebe0fa64a63fd25323e64deb3.tar.gz"; - sha256 = "0rxjkfiq53ibz0rzggvnp341b6kgzgfr9x6q07m2my7ijlirs2da"; + url = "https://github.com/NixOS/nixpkgs/archive/05f0934825c2a0750d4888c4735f9420c906b388.tar.gz"; + sha256 = "1g8c2w0661qn89ajp44znmwfmghbbiygvdzq0rzlvlpdiz28v6gy"; }), -coq-version ? "8.9", -mc ? "1.8.0", +coq-version ? "8.11", +mc ? "1.10.0", print-env ? false }: let @@ -16,6 +16,7 @@ let "8.8" = coqPackages_8_8; "8.9" = coqPackages_8_9; "8.10" = coqPackages_8_10; + "8.11" = coqPackages_8_11; }."${coq-version}"); in coqPackages.overrideScope' (self: super: {