# Algebra Tactics 1.1.1 released

**URL:** <https://discourse.rocq-prover.org/t/algebra-tactics-1-1-1-released/1929>\
**Category:** Announcements\
**Tags:** mathcomp\
**Created:** [April 13, 2023, 1:12pm UTC](https://discourse.rocq-prover.org/t/algebra-tactics-1-1-1-released/1929 "2023-04-13T13:12:33Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![pi8027](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/pi8027/32/371_2.png) [@pi8027](https://discourse.rocq-prover.org/u/pi8027)\
**Post date:** [April 13, 2023, 1:12pm UTC](https://discourse.rocq-prover.org/t/algebra-tactics-1-1-1-released/1929/1 "2023-04-13T13:12:33Z")

</div>

Dear Mathematical Components users,

We are pleased to announce the release of [Algebra Tactics](https://github.com/math-comp/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`

```coq
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

```coq
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)

```coq
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

```coq
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

```coq
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)

```coq
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