Merge pull request #180 from coq-community/port_paramcoq_elpi

Port from paramcoq to elpi

Author: proux01

.github/workflows/docker-action.yml

@@ -18,8 +18,6 @@ jobs:
           - 'mathcomp/mathcomp:1.18.0-coq-8.18'
           - 'mathcomp/mathcomp:1.17.0-coq-8.17'
           - 'mathcomp/mathcomp:1.15.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

.github/workflows/nix-action-default.yml

@@ -371,9 +371,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
         --argstr job "mathcomp-zify"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: paramcoq'
+      name: 'Building/fetching previous CI target: coq-elpi'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
-        --argstr job "paramcoq"
+        --argstr job "coq-elpi"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"

.nix/config.nix

@@ -41,7 +41,7 @@
 
     ## You can override Coq and other Coq coqPackages
     ## through the following attribute
-    coqPackages.coq.override.version = "8.15";
+    coqPackages.coq.override.version = "8.16";
     coqPackages.gaia-hydras.override.version = ../.;
     coqPackages.goedel.override.version = ../.;
     coqPackages.coqprime.override.version = "master";

.nix/coq-overlays/hydra-battles-single/default.nix

@@ -1,5 +1,5 @@
 { lib, mkCoqDerivation, coq, version ? null
-, coqprime, equations, gaia, LibHyps, mathcomp-ssreflect, mathcomp-algebra, mathcomp-zify, paramcoq, zorns-lemma
+, coqprime, equations, gaia, LibHyps, mathcomp-ssreflect, mathcomp-algebra, mathcomp-zify, coq-elpi, zorns-lemma
 , python3Packages, serapi, texlive, withMovies ? true, withTex ? true }:
 
 with lib; mkCoqDerivation rec {
@@ -50,7 +50,7 @@ with lib; mkCoqDerivation rec {
     mathcomp-ssreflect
     mathcomp-algebra
     mathcomp-zify
-    paramcoq
+    coq-elpi
     zorns-lemma
   ];
 

README.md

@@ -65,8 +65,8 @@ the proceedings of [JFLA 2022](http://jfla.inria.fr/jfla2022.html).
 - Compatible Coq versions: 8.14 or later
 - Additional dependencies:
   - [Equations](https://github.com/mattam82/Coq-Equations) 1.2 or later
-  - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
-  - [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.13 or later
+  - [Coq-elpi](https://github.com/LPCIC/coq-elpi) 1.16 or later
+  - [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.15 or later
   - [MathComp Algebra](https://github.com/math-comp/math-comp)
   - [Gaia's Schütte ordinals](https://github.com/coq-community/gaia) 1.14 or later
   - [Mczify](https://github.com/math-comp/mczify)

coq-addition-chains.opam

@@ -17,9 +17,9 @@ correctness."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {>= "8.14"}
-  "coq-paramcoq" {>= "1.1.3"}
-  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.19"}
+  "coq" {>= "8.16"}
+  "coq-elpi" {>= "1.16.0"}
+  "coq-mathcomp-ssreflect" {>= "1.15.0" & < "1.19"}
   "coq-mathcomp-algebra"
 ]
 

coq-gaia-hydras.opam

@@ -16,9 +16,9 @@ similar concepts in the two projects."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {>= "8.14"}
+  "coq" {>= "8.16"}
   "coq-hydra-battles" {= version}
-  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.19"}
+  "coq-mathcomp-ssreflect" {>= "1.15.0" & < "1.19"}
   "coq-mathcomp-zify" {< "2"}
   "coq-gaia-schutte" {>= "1.14" & < "1.18"}
 ]

coq-goedel.opam

@@ -16,7 +16,7 @@ without induction) that is complete is inconsistent."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {>= "8.14"}
+  "coq" {>= "8.16"}
   "coq-hydra-battles" {= version}
   "coq-coqprime" {>= "1.3.0"}
 ]

coq-hydra-battles.opam

@@ -18,7 +18,7 @@ properties of epsilon0)."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {>= "8.14"}
+  "coq" {>= "8.16"}
   "coq-equations" {>= "1.2"}
   "coq-zorns-lemma" {>= "10.2.0"}
   "coq-libhyps"

meta.yml

@@ -126,10 +126,6 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.15.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
@@ -138,10 +134,10 @@ dependencies:
   description: |-
     [Equations](https://github.com/mattam82/Coq-Equations) 1.2 or later
 - opam:
-    name: coq-paramcoq
-    version: '{>= "1.1.3"}'
+    name: coq-elpi
+    version: '{>= "1.16.0"}'
   description: |-
-    [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
+    [Coq-elpi](https://github.com/LPCIC/coq-elpi) 1.16 or later
 - opam:
     name: coq-mathcomp-ssreflect
     version: '{>= "1.13.0" & < "1.19"}'

theories/additions/Addition_Chains.v

@@ -1,13 +1,12 @@
-
 (** *  Addition Chains
 Pierre Casteran, LaBRI, University of Bordeaux
 
 *)
+From elpi Require Import derive param2.
 
 From additions Require Export Monoid_instances Pow.
 From Coq Require Import Relations RelationClasses Lia List.
-From Param Require Import Param.
- 
+
 From additions Require Import More_on_positive.
 Generalizable Variables A op one Aeq.
 Infix "==" := Monoid_def.equiv (at level 70) : type_scope.
@@ -232,7 +231,7 @@ Abort.
 (** Binary trees of multiplications over A *)
 
 Inductive Monoid_Exp (A:Type) : Type :=
- Mul_node (t t' : Monoid_Exp A) | One_node | A_node (a:A).
+ Mul_node (t t' : Monoid_Exp) | One_node | A_node (a:A).
 
 Arguments Mul_node {A} _ _.
 Arguments One_node {A} .
@@ -399,7 +398,7 @@ the corresponding variables of type A  and B are always bound to related
 
 
 (* begin snippet paramDemo *)
-Parametricity computation.
+Elpi derive.param2 computation.
 
 Print computation_R.
 (* end snippet paramDemo *)
@@ -507,7 +506,7 @@ Lemma  power_R_is_a_refinement (a:A) :
              (computation_eval (M:= Natplus) gamma_nat).
 (* end snippet powerRRef *)
 Proof.
-  induction 1;simpl;[auto | ].
+  induction 1 as [|x1 x2 x_R y1 y2 y_R];simpl;[auto | ].
   apply H; destruct x_R, y_R;  split.
   unfold mult_op, nat_plus_op.  
   + lia. 
@@ -560,9 +559,9 @@ Proof.
                 (fun n p => n = Pos.to_nat p) 1 xH
                 (refl_equal 1)).
  unfold the_exponent, the_exponent_nat, chain_execute, chain_apply.
- generalize (c nat 1), (c _ 1%positive); induction 1.
+ generalize (c nat 1), (c _ 1%positive); induction 1 as [|x1 x2 x_R y1 y2 y_R].
  - cbn; assumption. 
- -  apply (H (x₁ + y₁)%nat (x₂ + y₂)%positive); rewrite Pos2Nat.inj_add;
+ -  apply (H (x1 + y1)%nat (x2 + y2)%positive); rewrite Pos2Nat.inj_add;
     now subst.
 Qed.