The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hello,

When time permits, I am maintaining those tactics.

> On 05 Nov 2015, at 17:20, Michael Shulman 
> <shulman AT sandiego.edu>
>  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
> unclear to me from reading that chapter in the manual whether the
> other tactics it mentions (lia, nia, lra) also require cspd; do they?
- lia and lra are for linear arithmetics. The prover is independent from csdp.
  It is a pure ml prover based on fourier elimination.
  In some corner cases, it does solve non-linear goals because
   it first develops polynomials (in a sense calls ring_simplify) before 
calling the linear prover.
- nia is also independent from csdp
  It does a VERY limited form of non-linear reasoning.
  The prover is the same linear prover but the goal is first saturated with 
product of the hypotheses.
  (If you find a « simple » non-linear goal that it does not solve, let me 
know…)
- psatz requires csdp. To my experience, it is very difficult to anticipate 
whether it will succeed

As mentioned earlier, if you only have equalities nsatz is probably the way 
to go.


Best,
—
Frédéric

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

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail