Fix, remove the compat layer, and add a better support for GRing.inv

.github/workflows/docker-action.yml

@@ -17,22 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.14'
-          - '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.13'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
           - 'mathcomp/mathcomp:1.15.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.15.0-coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.13'
-          - 'mathcomp/mathcomp-dev:coq-8.14'
-          - 'mathcomp/mathcomp-dev:coq-8.15'
           - 'mathcomp/mathcomp-dev:coq-8.16'
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false

Makefile.coq.local

@@ -1,2 +1,2 @@
 theories/ring.vo : theories/common.elpi theories/ring.elpi theories/field.elpi
-theories/lra.vo : theories/lra.elpi theories/compat815.elpi
+theories/lra.vo : theories/lra.elpi

README.md

@@ -12,28 +12,29 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 
 
-This library provides `ring` and `field` tactics for Mathematical Components,
-that work with any `comRingType` and `fieldType` instances, respectively.
-Their instance resolution is done through canonical structure inference.
-Therefore, they work with abstract rings and do not require `Add Ring` and
-`Add Field` commands. Another key feature of this library is that they
-automatically push down ring morphisms and additive functions to leaves of
-ring/field expressions before normalization to the Horner form.
+This library provides `ring`, `field`, and `lra` tactics for Mathematical
+Components, that work with any `comRingType`, `fieldType`, and
+`realDomainType` or `realFieldType` instances, respectively. Their instance
+resolution is done through canonical structure inference.  Therefore, they
+work with abstract rings and do not require `Add Ring` and `Add Field`
+commands. Another key feature of this library is that they automatically push
+down ring morphisms and additive functions to leaves of ring/field expressions
+before applying the proof procedures.
 
 ## Meta
 
 - Author(s):
   - Kazuhiko Sakaguchi (initial)
 - License: [CeCILL-B Free Software License Agreement](CeCILL-B)
-- Compatible Coq versions: 8.13 or later
+- Compatible Coq versions: 8.16 or later
 - Additional dependencies:
-  - [MathComp](https://math-comp.github.io) ssreflect 1.12 or later
+  - [MathComp](https://math-comp.github.io) ssreflect 1.15 or later
   - [MathComp](https://math-comp.github.io) algebra
   - [Mczify](https://github.com/math-comp/mczify) 1.1.0 or later
-  - [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.10.1 or later
+  - [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.15.0 or later
 - Coq namespace: `mathcomp.algebra_tactics`
 - Related publication(s):
-  - [Reflexive tactics for algebra, revisited](https://arxiv.org/abs/2202.04330) 
+  - [Reflexive tactics for algebra, revisited](https://drops.dagstuhl.de/opus/volltexte/2022/16738/) doi:[10.4230/LIPIcs.ITP.2022.29](https://doi.org/10.4230/LIPIcs.ITP.2022.29)
 
 ## Building and installation instructions
 

coq-mathcomp-algebra-tactics.opam

@@ -12,22 +12,23 @@ license: "CECILL-B"
 
 synopsis: "Ring and field tactics for Mathematical Components"
 description: """
-This library provides `ring` and `field` tactics for Mathematical Components,
-that work with any `comRingType` and `fieldType` instances, respectively.
-Their instance resolution is done through canonical structure inference.
-Therefore, they work with abstract rings and do not require `Add Ring` and
-`Add Field` commands. Another key feature of this library is that they
-automatically push down ring morphisms and additive functions to leaves of
-ring/field expressions before normalization to the Horner form."""
+This library provides `ring`, `field`, and `lra` tactics for Mathematical
+Components, that work with any `comRingType`, `fieldType`, and
+`realDomainType` or `realFieldType` instances, respectively. Their instance
+resolution is done through canonical structure inference.  Therefore, they
+work with abstract rings and do not require `Add Ring` and `Add Field`
+commands. Another key feature of this library is that they automatically push
+down ring morphisms and additive functions to leaves of ring/field expressions
+before applying the proof procedures."""
 
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.13"}
-  "coq-mathcomp-ssreflect" {>= "1.12"}
+  "coq" {>= "8.16"}
+  "coq-mathcomp-ssreflect" {>= "1.15"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-zify" {>= "1.1.0"}
-  "coq-elpi" {>= "1.10.1"}
+  "coq-elpi" {>= "1.15.0"}
 ]
 
 tags: [

meta.yml

@@ -9,17 +9,19 @@ synopsis: >-
   Ring and field tactics for Mathematical Components
 
 description: |-
-  This library provides `ring` and `field` tactics for Mathematical Components,
-  that work with any `comRingType` and `fieldType` instances, respectively.
-  Their instance resolution is done through canonical structure inference.
-  Therefore, they work with abstract rings and do not require `Add Ring` and
-  `Add Field` commands. Another key feature of this library is that they
-  automatically push down ring morphisms and additive functions to leaves of
-  ring/field expressions before normalization to the Horner form.
+  This library provides `ring`, `field`, and `lra` tactics for Mathematical
+  Components, that work with any `comRingType`, `fieldType`, and
+  `realDomainType` or `realFieldType` instances, respectively. Their instance
+  resolution is done through canonical structure inference.  Therefore, they
+  work with abstract rings and do not require `Add Ring` and `Add Field`
+  commands. Another key feature of this library is that they automatically push
+  down ring morphisms and additive functions to leaves of ring/field expressions
+  before applying the proof procedures.
 
 publications:
-- pub_url: https://arxiv.org/abs/2202.04330
+- pub_url: https://drops.dagstuhl.de/opus/volltexte/2022/16738/
   pub_title: Reflexive tactics for algebra, revisited
+  pub_doi: 10.4230/LIPIcs.ITP.2022.29
 
 authors:
 - name: Kazuhiko Sakaguchi
@@ -33,44 +35,14 @@ license:
   file: CeCILL-B
 
 supported_coq_versions:
-  text: 8.13 or later
-  opam: '{>= "8.13"}'
+  text: 8.16 or later
+  opam: '{>= "8.16"}'
 
 tested_coq_nix_versions:
 
 tested_coq_opam_versions:
-- 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.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.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: '1.15.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
 - version: '1.15.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-dev'
-  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-8.16'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'
@@ -79,9 +51,9 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.12"}'
+    version: '{>= "1.15"}'
   description: |-
-    [MathComp](https://math-comp.github.io) ssreflect 1.12 or later
+    [MathComp](https://math-comp.github.io) ssreflect 1.15 or later
 - opam:
     name: coq-mathcomp-algebra
   description: |-
@@ -93,9 +65,9 @@ dependencies:
     [Mczify](https://github.com/math-comp/mczify) 1.1.0 or later
 - opam:
     name: coq-elpi
-    version: '{>= "1.10.1"}'
+    version: '{>= "1.15.0"}'
   description: |-
-    [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.10.1 or later
+    [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.15.0 or later
 
 namespace: mathcomp.algebra_tactics