Replace paramcoq with elpi derive.param2

.github/workflows/docker-action.yml

@@ -17,18 +17,9 @@ jobs:
     strategy:
       matrix:
         image:
-          - '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.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-8.20'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
           - 'mathcomp/mathcomp:2.3.0-coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.18'
-          - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-8.20'
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false

.github/workflows/nix-action-coq-8.20.yml

@@ -244,10 +244,6 @@ jobs:
       name: 'Building/fetching previous CI target: bignums'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
         --argstr job "bignums"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: paramcoq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
-        --argstr job "paramcoq"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: multinomials'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"

.nix/config.nix

@@ -31,8 +31,8 @@
   ## Cachix caches to use in CI
   ## Below we list some standard ones
   cachix.coq = {};
-  cachix.coq-community = {};
-  cachix.math-comp.authToken = "CACHIX_AUTH_TOKEN";
+  cachix.math-comp.authToken = {};
+  cachix.coq-community = "CACHIX_AUTH_TOKEN";
 
   ## If you have write access to one of these caches you can
   ## provide the auth token or signing key through a secret
@@ -124,13 +124,15 @@
       mathcomp-real-closed.override.version = "master";
       stdlib.override.version = "master";
       bignums.override.version = "master";
+      mathcomp-apery.override.version = "coqeal_99";
     };
     "coq-8.20".coqPackages = common-bundles // {
       coq.override.version = "8.20";
       coq-elpi.override.version = "master";
       coq-elpi.override.elpi-version = "2.0.7";
       hierarchy-builder.override.version = "master";
-      mathcomp.override.version = "2.2.0";
+      mathcomp.override.version = "2.3.0";
+      mathcomp-apery.override.version = "coqeal_99";
     };
   };
 }

.nix/coq-overlays/coqeal/default.nix

@@ -0,0 +1,124 @@
+{
+  coq,
+  mkCoqDerivation,
+  mathcomp,
+  bignums,
+  paramcoq,
+  multinomials,
+  mathcomp-real-closed,
+  lib,
+  version ? null,
+}:
+
+let
+derivation = mkCoqDerivation {
+
+  pname = "CoqEAL";
+
+  inherit version;
+  defaultVersion =
+    with lib.versions;
+    lib.switch
+      [ coq.version mathcomp.version ]
+      [
+        {
+          cases = [
+            (range "8.16" "8.20")
+            (isGe "2.1.0")
+          ];
+          out = "2.0.3";
+        }
+        {
+          cases = [
+            (range "8.16" "8.20")
+            (isGe "2.0.0")
+          ];
+          out = "2.0.1";
+        }
+        {
+          cases = [
+            (range "8.16" "8.17")
+            (isGe "2.0.0")
+          ];
+          out = "2.0.0";
+        }
+        {
+          cases = [
+            (range "8.15" "8.18")
+            (range "1.15.0" "1.18.0")
+          ];
+          out = "1.1.3";
+        }
+        {
+          cases = [
+            (range "8.13" "8.17")
+            (range "1.13.0" "1.18.0")
+          ];
+          out = "1.1.1";
+        }
+        {
+          cases = [
+            (range "8.10" "8.15")
+            (range "1.12.0" "1.18.0")
+          ];
+          out = "1.1.0";
+        }
+        {
+          cases = [
+            (isGe "8.10")
+            (range "1.11.0" "1.12.0")
+          ];
+          out = "1.0.5";
+        }
+        {
+          cases = [
+            (isGe "8.7")
+            "1.11.0"
+          ];
+          out = "1.0.4";
+        }
+        {
+          cases = [
+            (isGe "8.7")
+            "1.10.0"
+          ];
+          out = "1.0.3";
+        }
+      ]
+      null;
+
+  release."2.0.3".sha256 = "sha256-5lDq7IWlEW0EkNzYPu+dA6KOvRgy53W/alikpDr/Kd0=";
+  release."2.0.1".sha256 = "sha256-d/IQ4IdS2tpyPewcGobj2S6m2HU+iXQmlvR+ITNIcjI=";
+  release."2.0.0".sha256 = "sha256-SG/KVnRJz2P+ZxkWVp1dDOnc/JVgigoexKfRUh1Y0GM";
+  release."1.1.3".sha256 = "sha256-xhqWpg86xbU1GbDtXXInNCTArjjPnWZctWiiasq1ScU=";
+  release."1.1.1".sha256 = "sha256-ExAdC3WuArNxS+Sa1r4x5aT7ylbCvP/BZXfkdQNAvZ8=";
+  release."1.1.0".sha256 = "1vyhfna5frkkq2fl1fkg2mwzpg09k3sbzxxpyp14fjay81xajrxr";
+  release."1.0.6".sha256 = "0lqkyfj4qbq8wr3yk8qgn7mclw582n3fjl9l19yp8cnchspzywx0";
+  release."1.0.5".sha256 = "0cmvky8glb5z2dy3q62aln6qbav4lrf2q1589f6h1gn5bgjrbzkm";
+  release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk";
+  release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
+
+  propagatedBuildInputs = [
+    mathcomp.algebra
+    bignums
+    multinomials
+  ];
+
+  meta = {
+    description = "CoqEAL - The Coq Effective Algebra Library";
+    license = lib.licenses.mit;
+  };
+};
+patched-derivation1 = derivation.overrideAttrs
+  (o: {
+    propagatedBuildInputs =
+      o.propagatedBuildInputs
+      ++ lib.optional (lib.versions.isGe "1.1" o.version || o.version == "dev") mathcomp-real-closed;
+  });
+patched-derivation = patched-derivation1.overrideAttrs
+  (o: {
+    propagatedBuildInputs =
+      o.propagatedBuildInputs
+      ++ lib.optional (lib.versions.isLe "2.0.3" o.version && o.version != "dev") paramcoq;
+  });
+in patched-derivation

README.md

@@ -47,7 +47,7 @@ of the ForMath EU FP7 project (2009-2013). It has two parts:
 - Compatible Coq versions: 8.16 or later (use releases for other Coq versions)
 - Additional dependencies:
   - [Bignums](https://github.com/coq/bignums) same version as Coq
-  - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
+  - [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 2.4.1 or later
   - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.4.0 or later
   - [MathComp ssreflect](https://math-comp.github.io) 2.1 or later
   - [MathComp algebra](https://math-comp.github.io) 2.1 or later

coq-coqeal.opam

@@ -23,7 +23,7 @@ install: [make "install"]
 depends: [
   "coq" {(>= "8.16" & < "8.21~") | (= "dev")}
   "coq-bignums" 
-  "coq-paramcoq" {>= "1.1.3"}
+  "coq-elpi" {>= "2.4.1"}
   "coq-hierarchy-builder" {>= "1.4.0"}
   "coq-mathcomp-ssreflect" {>= "2.1"}
   "coq-mathcomp-algebra" 

meta.yml

@@ -85,10 +85,10 @@ dependencies:
   description: |-
     [Bignums](https://github.com/coq/bignums) same version as Coq
 - opam:
-    name: coq-paramcoq
-    version: '{>= "1.1.3"}'
+    name: coq-elpi
+    version: '{>= "2.4.1"}'
   description: |-
-    [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
+    [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 2.4.1 or later
 - opam:
     name: coq-hierarchy-builder
     version: '{>= "1.4.0"}'
@@ -115,30 +115,12 @@ dependencies:
     [MathComp real-closed](https://math-comp.github.io) 2.0 or later
 
 tested_coq_opam_versions:
-- 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.2.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.17'
-  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-8.20'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-dev'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.18'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.19'
-  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.20'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'

refinements/bareiss_eff.v

@@ -63,10 +63,11 @@ Definition bdet n (M : mxR (1 + n) (1 + n)) := head (bareiss_char_poly (- M)%C).
 
 End generic_bareiss.
 
-Parametricity bareiss_rec.
-Parametricity bareiss.
-Parametricity bareiss_char_poly.
-Parametricity bdet.
+Elpi derive.param2 hmul_op.
+Elpi derive.param2 bareiss_rec.
+Elpi derive.param2 bareiss.
+Elpi derive.param2 bareiss_char_poly.
+Elpi derive.param2 bdet.
 
 (* First some general lemmas *)
 Section prelude.
@@ -301,41 +302,57 @@ Context `{forall m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2),
           refines ((RpolyC ==> RpolyC) ==> RmxpolyC rm rn ==> RmxpolyC rm rn)
                   (fun f => @matrix.map_mx _ _ f m1 n1) (@map_mxC m2 n2)}.
 Context `{forall m1 m2 (rm : nat_R m1 m2),
-          refines (RmxpolyC (nat_R_S_R rm) (nat_R_S_R rm) ==> RpolyC)
+          refines (RmxpolyC (S_R rm) (S_R rm) ==> RpolyC)
                   (@top_left m1) (@top_leftC m2)}.
 Context `{!refines (RpolyC ==> RpolyC ==> RpolyC) (@rdivp R) divpC}.
 Context `{forall n1 n2 (rn : nat_R n1 n2),
           refines (RmxC rn rn ==> RmxpolyC rn rn) (@char_poly_mx _ n1)
                   (@char_poly_mxC n2)}.
 Context `{!refines (RpolyC ==> rC) head headC}.
 
+#[export] Instance RmxpolyC_ursubmx :
+  refines (ursubmx_of_R (@RmxpolyC)) ursubmx ursubmxC.
+Proof. by rewrite /ursubmx_of_R refinesE => *; apply: refinesP. Qed.
+
+#[export] Instance RmxpolyC_dlsubmx :
+  refines (dlsubmx_of_R (@RmxpolyC)) dlsubmx dlsubmxC.
+Proof. by rewrite /dlsubmx_of_R refinesE => *; apply: refinesP. Qed.
+
+#[export] Instance RmxpolyC_drsubmx :
+  refines (drsubmx_of_R (@RmxpolyC)) drsubmx drsubmxC.
+Proof. by rewrite /drsubmx_of_R refinesE => *; apply: refinesP. Qed.
+
+#[export] Instance RmxpolyC_hmul :
+  refines (hmul_of_R (@RmxpolyC)) hmul_of_instance_0 hmul_of0.
+Proof. by rewrite /hmul_of_R refinesE => *; apply: refinesP. Qed.
+
 #[export] Instance RpolyC_bareiss_rec m1 m2 (rm : nat_R m1 m2) :
-  refines (RpolyC ==> RmxpolyC (nat_R_S_R rm) (nat_R_S_R rm) ==> RpolyC)
+  refines (RpolyC ==> RmxpolyC (S_R rm) (S_R rm) ==> RpolyC)
           (bareiss_rec (polyR:={poly R}) (mxpolyR:=matrix {poly R}) (m:=m1))
           (bareiss_rec (polyR:=polyC) (mxpolyR:=mxpolyC) (m:=m2)).
 Proof. param bareiss_rec_R. Qed.
 
 #[export] Instance refine_bareiss_rec m :
-  refines (RpolyC ==> RmxpolyC (nat_R_S_R (nat_Rxx m)) (nat_R_S_R (nat_Rxx m))
+  refines (RpolyC ==> RmxpolyC (S_R (nat_Rxx m)) (S_R (nat_Rxx m))
                   ==> RpolyC)
           (bareiss_rec (polyR:={poly R}) (mxpolyR:=matrix {poly R}) (m:=m))
           (bareiss_rec (polyR:=polyC) (mxpolyR:=mxpolyC) (m:=m)).
 Proof. exact: RpolyC_bareiss_rec. Qed.
 
 #[export] Instance RpolyC_bareiss n1 n2 (rn : nat_R n1 n2) :
-  refines (RmxpolyC (nat_R_S_R rn) (nat_R_S_R rn) ==> RpolyC)
+  refines (RmxpolyC (S_R rn) (S_R rn) ==> RpolyC)
           (bareiss (polyR:={poly R}) (mxpolyR:=matrix {poly R}) (n:=n1))
           (bareiss (polyR:=polyC) (mxpolyR:=mxpolyC) (n:=n2)).
 Proof. param bareiss_R. Qed.
 
 #[export] Instance refine_bareiss n :
-  refines (RmxpolyC (nat_R_S_R (nat_Rxx n)) (nat_R_S_R (nat_Rxx n)) ==> RpolyC)
+  refines (RmxpolyC (S_R (nat_Rxx n)) (S_R (nat_Rxx n)) ==> RpolyC)
           (bareiss (polyR:={poly R}) (mxpolyR:=matrix {poly R}) (n:=n))
           (bareiss (polyR:=polyC) (mxpolyR:=mxpolyC) (n:=n)).
 Proof. exact: RpolyC_bareiss. Qed.
 
 #[export] Instance RpolyC_bareiss_char_poly n1 n2 (rn : nat_R n1 n2) :
-  refines (RmxC (nat_R_S_R rn) (nat_R_S_R rn) ==> RpolyC)
+  refines (RmxC (S_R rn) (S_R rn) ==> RpolyC)
           (bareiss_char_poly (polyR:={poly R}) (mxR:=matrix R)
                              (mxpolyR:=matrix {poly R}) (@char_poly_mx R)
                              (n:=n1))
@@ -344,7 +361,7 @@ Proof. exact: RpolyC_bareiss. Qed.
 Proof. param bareiss_char_poly_R. Qed.
 
 #[export] Instance refine_bareiss_char_poly n :
-  refines (RmxC (nat_R_S_R (nat_Rxx n)) (nat_R_S_R (nat_Rxx n)) ==> RpolyC)
+  refines (RmxC (S_R (nat_Rxx n)) (S_R (nat_Rxx n)) ==> RpolyC)
           (bareiss_char_poly (polyR:={poly R}) (mxR:=matrix R)
                              (mxpolyR:=matrix {poly R}) (@char_poly_mx R)
                              (n:=n))
@@ -353,16 +370,16 @@ Proof. param bareiss_char_poly_R. Qed.
 Proof. exact: RpolyC_bareiss_char_poly. Qed.
 
 #[export] Instance RC_bdet n1 n2 (rn : nat_R n1 n2) :
-  refines (RmxC (nat_R_S_R rn) (nat_R_S_R rn) ==> rC)
+  refines (RmxC (S_R rn) (S_R rn) ==> rC)
           (bdet (R:=R) (polyR:={poly R}) (mxR:=matrix R)
                 (mxpolyR:=matrix {poly R}) (@char_poly_mx R) head
                 (n:=n1))
           (bdet (R:=C) (polyR:=polyC) (mxR:=mxC) (mxpolyR:=mxpolyC)
                 char_poly_mxC headC (n:=n2)).
-Proof. param bdet_R. Qed.
+Proof. by param bdet_R; rewrite /opp_of_R refinesE => *; apply: refinesP. Qed.
 
 #[export] Instance refine_bdet n :
-  refines (RmxC (nat_R_S_R (nat_Rxx n)) (nat_R_S_R (nat_Rxx n)) ==> rC)
+  refines (RmxC (S_R (nat_Rxx n)) (S_R (nat_Rxx n)) ==> rC)
           (bdet (R:=R) (polyR:={poly R}) (mxR:=matrix R)
                 (mxpolyR:=matrix {poly R}) (@char_poly_mx R) head
                 (n:=n))
@@ -371,7 +388,7 @@ Proof. param bdet_R. Qed.
 Proof. exact: RC_bdet. Qed.
 
 #[export] Instance RC_det_bdet n1 n2 (rn : nat_R n1 n2) :
-  refines (RmxC (nat_R_S_R rn) (nat_R_S_R rn) ==> rC) determinant
+  refines (RmxC (S_R rn) (S_R rn) ==> rC) determinant
           (bdet (R:=C) (polyR:=polyC) (mxpolyR:=mxpolyC) char_poly_mxC headC
                 (n:=n2)).
 Proof.
@@ -381,7 +398,7 @@ Proof.
 Qed.
 
 #[export] Instance refine_det n :
-  refines (RmxC (nat_R_S_R (nat_Rxx n)) (nat_R_S_R (nat_Rxx n)) ==> rC)
+  refines (RmxC (S_R (nat_Rxx n)) (S_R (nat_Rxx n)) ==> rC)
           determinant (bdet (R:=C) (polyR:=polyC) (mxpolyR:=mxpolyC)
                             char_poly_mxC headC (n:=n)).
 Proof. exact: RC_det_bdet. Qed.