From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,d4e6b104ff087788,start
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news2.google.com!news2.google.com!goblin3!goblin1!goblin2!goblin.stu.neva.ru!aioe.org!not-for-mail
From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?=
 =?utf-8?Q?=29?=
 <yannick_duchene@yahoo.fr>
Newsgroups: comp.lang.ada
Subject: SPARK : surprising failure with implication
Date: Tue, 01 Jun 2010 20:51:04 +0200
Organization: Ada At Home
Message-ID: <op.vdmxbejnule2fv@garhos>
NNTP-Posting-Host: 7g+UIcN0UM67WCCZrTfU2A.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes
Content-Transfer-Encoding: Quoted-Printable
X-Complaints-To: abuse@aioe.org
X-Notice: Filtered by postfilter v. 0.8.2
User-Agent: Opera Mail/10.53 (Win32)
Xref: g2news2.google.com comp.lang.ada:12177
Date: 2010-06-01T20:51:04+02:00
List-Id: <comp.lang.ada>

Hi all,

In an Ada/SPARK source, I had something like this:

    --# check (Source =3D 1) -> ((Source mod 2) =3D 1); -- (1)
    --# check (Source mod 2) /=3D 1;                  -- (2)
    --# check Source /=3D 1;                          -- (3)

1) Was proved by the simplifier (note that I needed a user rule for that=
).
2) Is a valid hypothesis ; an already proved conclusion (in some prior  =

check clauses)
3) Failed to be proved, while I expected this to be proved from (1) and =
 =

(2).


Naively, I had though Simplifier was not handling =E2=80=9C(Source mod 2=
) /=3D 1=E2=80=9D as  =

an equivalent of =E2=80=9Cnot ((Source mod 2) =3D 1)=E2=80=9D, so I trie=
d this:

    --# check (Source =3D 1) -> ((Source mod 2) =3D 1); -- (1)
    --# check not ((Source mod 2) =3D 1);             -- (2)
    --# check not (Source =3D 1);                     -- (3)


Hem, I'm not silly (or am I?), where =E2=80=9CA -> B=E2=80=9D is valid, =
then =E2=80=9Cnot B -> not  =

A=E2=80=9D is valid too.

Whatever was going on, I wanted to be sure, so then tried the following:=


    --# check (Source =3D 1) -> ((Source mod 2) =3D 1);             -- (=
1)
    --# check (not ((Source mod 2) =3D 1)) -> (not (Source =3D 1)); -- (=
1-bis)
    --# check not ((Source mod 2) =3D 1);                         -- (2)=

    --# check not (Source =3D 1);                                 -- (3)=


Simplifier failed on 1-bis. Ouch 8|


Do I become silly ?

I've looked in the *.SIV generated file, and it appears the simplifier  =

automatically turns things of the form =E2=80=9Cnot (A =3D B)=E2=80=9D i=
nto =E2=80=9CA /=3D B)=E2=80=9D (i.e.  =

=E2=80=9CA <> B=E2=80=9D, in an *.SIV file).

What I suspect: as Simplifier turns =E2=80=9Cnot A =3D B=E2=80=9D into =E2=
=80=9CA /=3D B=E2=80=9D, it cannot  =

see it as the negation of the antecedent and consequent of the implicati=
on  =

proved in (1), so from A -> B proved, I cannot prove not B -> not A, whi=
le  =

logically speaking, I know =E2=80=9C(A -> B) <-> (not B -> not A)=E2=80=9D=
. But it still  =

recognize =E2=80=9Cnot ((Source mod 2) =3D 1)=E2=80=9D as equivalent to =
=E2=80=9C(Source mod 2) /=3D  =

1=E2=80=9D, so I'm not sure about the reason why it fails. Or may be it =
can see it  =

as equivalent only when standalone and not in (1-bis) or against (1) ?


I was surprised to meet such an issue (unless I am missing some silly  =

things because I would perhaps be too much tired).