Merge pull request #30 from coq-community/coqeal_99

Adapt to coq-community/coqeal#99

Author: proux01

.github/workflows/docker-action.yml

@@ -17,20 +17,13 @@ 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-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.18'
-          - 'mathcomp/mathcomp-dev:coq-8.19'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.3.0-coq-dev'
+          - 'mathcomp/mathcomp-dev:coq-8.20'
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-mathcomp-apery.opam'

README.md

@@ -46,7 +46,7 @@ remains the sole trusted code base.
   - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp field](https://math-comp.github.io)
-  - [CoqEAL 2.0.0 or later](https://github.com/coq-community/coqeal)
+  - [CoqEAL 2.0.4 or later](https://github.com/coq-community/coqeal)
   - [MathComp real closed fields 2.0.0 or later](https://github.com/math-comp/real-closed)
   - [MathComp bigenough 1.0.1 or later](https://github.com/math-comp/bigenough)
   - [Mczify](https://github.com/math-comp/mczify) 1.5.0 or later

coq-mathcomp-apery.opam

@@ -24,10 +24,10 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" {(>= "8.16" & < "8.20~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "2.1" & < "2.3~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "2.3" & < "2.4~") | (= "dev")}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-field" 
-  "coq-coqeal" {>= "2.0.0"}
+  "coq-coqeal" {>= "2.0.4"}
   "coq-mathcomp-real-closed" {>= "2.0.0"}
   "coq-mathcomp-bigenough" {>= "1.0.1"}
   "coq-mathcomp-zify" {>= "1.5.0"}

meta.yml

@@ -55,33 +55,19 @@ supported_coq_versions:
   opam: '{(>= "8.16" & < "8.20~") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: '2.1.0-coq-8.16'
+- version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: '2.1.0-coq-8.17'
+- version: '2.3.0-coq-dev'
   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-dev'
-  repo: 'mathcomp/mathcomp'
-- version: 'coq-8.18'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.19'
+- version: 'coq-8.20'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "2.1" & < "2.3~") | (= "dev")}'
+    version: '{(>= "2.3" & < "2.4~") | (= "dev")}'
   description: |-
     [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
 - opam:
@@ -94,9 +80,9 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-coqeal
-    version: '{>= "2.0.0"}'
+    version: '{>= "2.0.4"}'
   description: |-
-    [CoqEAL 2.0.0 or later](https://github.com/coq-community/coqeal)
+    [CoqEAL 2.0.4 or later](https://github.com/coq-community/coqeal)
 - opam:
     name: coq-mathcomp-real-closed
     version: '{>= "2.0.0"}'

theories/rho_computations.v

@@ -196,16 +196,23 @@ Context (RexpAQ : refines (RAQ ==> Logic.eq ==> RAQ)%rel (@GRing.exp _) exp_op).
 Context (RZtoAQ : refines (Logic.eq ==> RAQ)%rel rat_of_Z cast).
 Context (Rnat_to_AQ : refines (Logic.eq ==> RAQ)%rel natr cast).
 
-Parametricity positive.
-Parametricity Z.
-Parametricity generic_beta.
-Parametricity generic_alpha.
-Parametricity generic_h.
-Parametricity generic_h_iter.
+Elpi derive.param2 positive.
+Elpi derive.param2 Z.
+Elpi derive.param2 generic_beta.
+Elpi derive.param2 generic_alpha.
+Elpi derive.param2 generic_h.
+Elpi derive.param2 generic_h_iter.
 
 Global Instance refines_bool_eq x y : refines Z_R x y -> refines eq x y.
 Proof. by rewrite !refinesE; case => // p q; elim => // ? ? _ [->]. Qed.
 
+Global Instance refines_expAQ :
+  refines (exp_of_R RAQ nat_R) (GRing.exp (R:=rat)) expAQ.
+Proof. by rewrite /exp_of_R refinesE => *; apply: refinesP. Qed.
+
+Global Instance refines_ZtoAQ : refines (cast_of_R Z_R RAQ) rat_of_Z ZtoAQ.
+Proof. by rewrite /cast_of_R refinesE => *; apply: refinesP. Qed.
+
 Global Instance refines_beta :
   refines (RAQ ==> RAQ)%rel beta (generic_beta _ _ _ _).
 Proof. by param generic_beta_R. Qed.
@@ -218,9 +225,13 @@ Global Instance refines_h :
   refines (RAQ ==> RAQ ==> RAQ)%rel h (generic_h _ _ _ _ _ _).
 Proof. by param generic_h_R. Qed.
 
+Global Instance refines_nat_to_AQ :
+  refines (cast_of_R nat_R RAQ) natr nat_to_AQ.
+Proof. by rewrite /cast_of_R refinesE => *; apply: refinesP. Qed.
+
 Global Instance refines_h_iter n :
   refines (RAQ)%rel (h_iter n) (generic_h_iter _ _ _ _ _ _ _ _ n).
-Proof. by param generic_h_iter_R; rewrite refinesE; elim: n => //= *; constructor. Qed.
+Proof. by param generic_h_iter_R; rewrite refinesE; apply: nat_Rxx. Qed.
 
 End parametric.