Lra

.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

.gitignore

@@ -15,3 +15,9 @@ Make*.coq.conf
 *#
 .lia.cache
 .nia.cache
+examples/.csdp.cache
+examples/.nra.cache
+examples/trace
+theories/.csdp.cache
+theories/.nra.cache
+theories/trace

Make

@@ -1,4 +1,5 @@
 theories/ring.v
+theories/lra.v
 
 -R theories mathcomp.algebra_tactics
 -arg -w -arg -notation-overridden

Make.test-suite

@@ -4,6 +4,7 @@ examples/ring_examples_check.v
 examples/ring_examples_no_check.v
 examples/from_sander.v
 examples/zmodule.v
+examples/lra_examples.v
 
 -R examples mathcomp.algebra_tactics.examples
 -arg -w -arg -notation-overridden

Makefile.coq.local

@@ -1 +1,2 @@
-theories/ring.vo : $(wildcard theories/*.elpi)
+theories/ring.vo : theories/common.elpi theories/ring.elpi theories/field.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: [