Ssreflect Users Discussion List

[Kazuhiko Sakaguchi <>]

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