The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

According to the manual
https://coq.inria.fr/distrib/current/refman/Reference-Manual024.html
the tactic psatz requires the external program "cspd".  But it's
unclear to me from reading that chapter in the manual whether the
other tactics it mentions (lia, nia, lra) also require cspd; do they?

On Thu, Nov 5, 2015 at 4:27 AM, Laurent Thery 
<Laurent.Thery AT inria.fr>
 wrote:
>
>
> 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