Algebra Tactics 1.1.1 released

Announcements
1

Dear Mathematical Components users,

We are pleased to announce the release of Algebra Tactics 1.1.1.
In addition to the already provided ring and field tactics, this
release gives access to the lra, nra and psatz tactics from the
Micromega plugin shipped with Coq. For the moment, the new tactics are
considered experimental features and subject to change.

The new release is available in the OPAM package
coq-mathcomp-algebra-tactics.1.1.1 compatible with Coq 8.16 and 8.17
and MathComp 1.15 and 1.16. A Nix package is also available.

The new tactics work for any abstract realDomainType

From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum lra.
Local Open Scope ring_scope.

Example any_realDomain (F : realDomainType) (x y : F) :
  x + 2 * y <= 3 -> 2 * x + y <= 3 -> x + y <= 2.
Proof. lra. Qed.

Print Assumptions any_realDomain.  (* Closed under the global context *)

or any realFieldType with divisions

From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum lra.
Local Open Scope ring_scope.

Example any_field (F : realFieldType) (x y : F) :
  x / 2 + y <= 3 -> x + y / 2 <= 3 -> x + y <= 4.
Proof. lra. Qed.

They also handle any concrete instance of the above (like the rational
numbers for instance)

From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum rat lra.
Local Open Scope ring_scope.

Example rat (x y : rat) :
  x + 2 * y <= 3 -> 2 * x + y <= 3 -> x + y <= 2.
Proof. lra. Qed.

The nra (non-linear real arithmetic) tactic is an extension of the
lra tactic that handles some non-linear goals

From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum lra.
Local Open Scope ring_scope.

Example non_linear (F : realDomainType) (x y : F) : - x * x >= 0 -> x * y = 0.
Proof. nra. Qed.

One can also use the psatz tactic, provided the CSDP solver is installed.

Just like the ring and field tactics, lra, nra and psatz
handle any ring morphism, either abstract

From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum lra.
Local Open Scope ring_scope.

Example abstract_rmorphism (R : realDomainType) (f : {rmorphism R -> R})
  (x y : R) : f y >= 0 -> f x + 2 * f (y + 1) <= f (3 * y + x) + 2.
Proof. lra. Qed.

or concrete (ratr is the injection from rat to any ring)

From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum rat lra.
Local Open Scope ring_scope.

Example ratr (R : realFieldType) (x y : rat) :
  ratr y >= 0 :> R -> ratr x + 2 * ratr (y + 1) <= ratr (3 * y + x) + 2 :> R.
Proof. lra. Qed.

We would like to thank Frédéric Besson and Enrico Tassi for their help
respectively with Micromega and Coq-Elpi.

Kazuhiko and Pierre

1 Like