Merge pull request #4 from pi8027/algebra-tactics

Replace `lia_tactics` and `field_tactics` with mczify and Algebra Tactics
coq-community · May 3, 2022 · aa7d914 · aa7d914
2 parents 16f2cbe + 7335782
commit aa7d914
Show file tree

Hide file tree

Showing 36 changed files with 895 additions and 1,960 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -17,17 +17,18 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
           - 'mathcomp/mathcomp:1.12.0-coq-8.13'
           - 'mathcomp/mathcomp:1.12.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.12'
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.12'
           - 'mathcomp/mathcomp:1.14.0-coq-8.13'
           - 'mathcomp/mathcomp:1.14.0-coq-8.14'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
+          - 'mathcomp/mathcomp-dev:coq-8.13'
+          - 'mathcomp/mathcomp-dev:coq-8.14'
+          - 'mathcomp/mathcomp-dev:coq-8.15'
+          - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

diff --git a/README.md b/README.md
@@ -40,14 +40,16 @@ remains the sole trusted code base.
 - Coq-community maintainer(s):
   - Assia Mahboubi ([**@amahboubi**](https://github.com/amahboubi))
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: 8.12 or later
+- Compatible Coq versions: 8.13 or later
 - Additional dependencies:
   - [MathComp ssreflect 1.12 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp field](https://math-comp.github.io)
   - [CoqEAL 1.0.5 or later](https://github.com/coq-community/coqeal)
   - [MathComp real closed fields 1.1.2 or later](https://github.com/math-comp/real-closed)
   - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)
+  - [Mczify](https://github.com/math-comp/mczify) 1.2.0 or later
+  - [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 0.2.0 or later
 - Coq namespace: `mathcomp.apery`
 - Related publication(s):
   - [A Formal Proof of the Irrationality of ζ(3)](https://arxiv.org/abs/1912.06611) 

diff --git a/_CoqProject b/_CoqProject
@@ -21,13 +21,10 @@ theories/b_props.v
 theories/bigopz.v
 theories/binomialz.v
 theories/c_props.v
-theories/conj.v
 theories/extra_cauchyreals.v
 theories/extra_mathcomp.v
-theories/field_tactics.v
 theories/harmonic_numbers.v
 theories/initial_conds.v
-theories/lia_tactics.v
 theories/ops_for_a.v
 theories/ops_for_b.v
 theories/ops_for_s.v
@@ -40,8 +37,7 @@ theories/reduce_order.v
 theories/s_props.v
 theories/seq_defs.v
 theories/shift.v
-theories/test_conj.v
-theories/test_field_tactics.v
+theories/tactics.v
 theories/z3irrational.v
 theories/z3seq_props.v
 theories/rho_computations.v

diff --git a/coq-mathcomp-apery.opam b/coq-mathcomp-apery.opam
@@ -23,13 +23,15 @@ remains the sole trusted code base."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.11" & < "8.16~") | (= "dev")}
+  "coq" {(>= "8.13" & < "8.16~") | (= "dev")}
   "coq-mathcomp-ssreflect" {(>= "1.12" & < "1.15~") | (= "dev")}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-field" 
   "coq-coqeal" {>= "1.0.5"}
   "coq-mathcomp-real-closed" {>= "1.1.2"}
   "coq-mathcomp-bigenough" {>= "1.0.0"}
+  "coq-mathcomp-zify" {(>= "1.2.0") | (= "dev")}
+  "coq-mathcomp-algebra-tactics" {(>= "0.2.0") | (= "dev")}
 ]
 
 tags: [

diff --git a/include/ops_header.v b/include/ops_header.v
@@ -1,6 +1,6 @@
 Require Import BinInt.
 From mathcomp Require Import all_ssreflect all_algebra.
-Require Import field_tactics lia_tactics conj bigopz shift.
+Require Import tactics rat_of_Z bigopz shift.
 Require punk.
 
 Set Implicit Arguments.

diff --git a/meta.yml b/meta.yml
@@ -46,32 +46,34 @@ license:
   identifier: CECILL-C
 
 supported_coq_versions:
-  text: 8.12 or later
-  opam: '{(>= "8.11" & < "8.16~") | (= "dev")}'
+  text: 8.13 or later
+  opam: '{(>= "8.13" & < "8.16~") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: '1.12.0-coq-8.12'
-  repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.12'
-  repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.12'
-  repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
+- version: 'coq-8.13'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.14'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.15'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-dev'
+  repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:
@@ -102,6 +104,16 @@ dependencies:
     version: '{>= "1.0.0"}'
   description: |-
     [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)
+- opam:
+    name: coq-mathcomp-zify
+    version: '{(>= "1.2.0") | (= "dev")}'
+  description: |-
+    [Mczify](https://github.com/math-comp/mczify) 1.2.0 or later
+- opam:
+    name: coq-mathcomp-algebra-tactics
+    version: '{(>= "0.2.0") | (= "dev")}'
+  description: |-
+    [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 0.2.0 or later
 
 namespace: mathcomp.apery