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
math-comp · Apr 1, 2020 · dbb98e9 · dbb98e9
1 parent ceaf677
commit dbb98e9
Show file tree

Hide file tree

Showing 5 changed files with 28 additions and 23 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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: {