The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 11/04/2015 05:09 PM, Michael Shulman wrote:
> I wanted a version of the tactic "ring" which is able to make use of
> equalities in the context.  So I wrote my own:
>
> Ltac ring_useeq :=
>    first [ ring
>          | match goal with
>              | [ H : ?a = ?b |- _ ] =>
>                first [ rewrite H; clear H; ring_useeq
>                      | rewrite <- H; clear H; ring_useeq
>                      | clear H; ring_useeq ]
>            end ].
>
> If I did it right, this is doing a tree search through all possible
> combinations of rewriting in either direction or not at all with each
> equality in the context.  However, one could imagine it being even
> smarter and trying more things, e.g. in theory it might matter what
> order the rewrites happen in.  Does a tactic like this exist already
> somewhere?
>
> Mike

As a mattern of fact one can use assumptions with ring if there are of 
the form A = P where addition and multiplication do not occur in A.

Example 1 :

Require Import ZArith Ring.

Open Scope Z_scope.

Goal forall x y z,
x = y ^ 2 -> (y - z) * (y + z) = x - z^2.
Proof.
intros x y z H; ring [H].
Qed.

You have also grobner like computation available with Loïc Pottier's 
tactic nsatz. Grobner is a very powerful technique but even for simple 
example it can be very CPU intensive.

Example 2 from cyclic 3 :

Require Import Reals Nsatz.

Open Scope R_scope.

Goal forall x y z,
   x + y + z = 0 ->
   x * y + x * z + y * z = 0 ->
   x * y * z = 0 -> x * x * x = 0.
Proof.
intros x y z H1 H2 H3; nsatz.
Qed.

There is also a third tactic called nia developed by Frédéric Besson
It just adds some non-linear tricks on top of psatz. In practice  I find 
this tactic very impressive.

Example 3 from bresenham's algo :

Require Import Psatz ZArith.

Open Scope Z_scope.

Goal forall a b c,
 0 < a -> Zabs (2 * a * b - 2 * c) <= a -> forall b', Zabs (a * b - c)
<= Zabs (a * b' - c).
Proof.
intros a b c _ H b'.
assert (H1:  b = b' \/ Zabs (b - b') >= 1) by nia.
nia.
Qed.

--
Laurent