The Coq mailing list

[Dmitrii Pasechnik <dmitrii.pasechnik AT cs.ox.ac.uk>]

On Thu, Nov 05, 2015 at 08:20:56AM -0800, Michael Shulman wrote:
> 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

It's a typo in the manual, it's csdp (as is clear from the link provided
there).
I can also (shameless self-advertising here) point out that one might prefer 
to install csdp
from https://github.com/dimpase/csdp 
(which is the "usual" ./configure + make procedure to follow, rather
than manually editing a makefile...)
Actually, not hard to install, at all.

> unclear to me from reading that chapter in the manual whether the
> other tactics it mentions (lia, nia, lra) also require cspd; do they?

I don't know, but things involving Positivestellensatz might need a
semidefinite programming solver (csdp is one of them). Unless you use
a very weak form of it, that would only need a linear programming solver
(more precisely, testing systems of linear inequalities for solvability)

Dima
> 
> 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