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: 103376,ec6f74e58e86b38b
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,CP1252
Path: 
 g2news1.google.com!postnews.google.com!z17g2000vbd.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: Lost in translation (with SPARK user rules)
Date: Wed, 26 May 2010 03:38:52 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <0466e131-cc80-4db4-b080-eec9aefcb1c7@z17g2000vbd.googlegroups.com>
References: <op.vda45rsfule2fv@garhos>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1274870333 8347 127.0.0.1 (26 May 2010 10:38:53
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Wed, 26 May 2010 10:38:53 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: z17g2000vbd.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
	Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
	3.0.30729; Media Center PC 6.0),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:11053
Date: 2010-05-26T03:38:52-07:00
List-Id: <comp.lang.ada>

On 26 May, 11:09, Yannick Duch=EAne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
[...]
> I tried with this:
>
> =A0 =A0 bitwise(112): bit__and(X div (2**N), 1)=3D0 may_be_deduced_from [=
 =A0
> (bit__and(X, 2**N)=3D0), X>=3D0, N>=3D0 ].
> =A0 =A0 bitwise(113): bit__and(X, 2**N)=3D0 may_be_deduced_from [ (bit__a=
nd(X div =A0
> (2**N), 1)=3D0), X>=3D0, N>=3D0 ].
>
> But this fails, although the simplifier does not returns me any syntax =
=A0
> error messages about this *.RLU file. This fails, because it cannot prove=
 =A0
> something like this:
>
> =A0 =A0 --# check ((Instance and 2) =3D 0) -> (((Instance / 2) and 1) =3D=
 0);
>
> The latter should be directly deduced from the two previous rules if thes=
e =A0
> were OK. So I suppose something is wrong with these rules, and the =A0
> expression in =93[...]=94 is not interpreted the way it seems to be to me=
.

I don't think there us anything wrong with these rules, but the
Simplifier will not use a *combination* of user rules to discharge a
proof.  (They are not as 'powerful' as the built-in rules as they are
not consulted until the Simplifier has tried all its other
strategies).

For example, section 7.3.1 of the Simplifier User Manual says:
   "For an inference rule of the form
      rulename(1): Goal may_be_deduced_from Conditions.
   the Simplifier will attempt to find a means of instantiating
   all of the wildcards in Goal such that it becomes an exact
   match for an existing undischarged conclusion."

This means that a single inference rule is applied only if it
*directly* matches a conclusion.

Also, since user rules are applied right at the end, you have to use
the form of the conclusion as it appears in the SIV file, so:
> One entertaining thing: I've noticed =93and 1=94 is always replaced by =
=93mod 2=94 =A0
> in the simplifier's *.SIV output files. As an example, the latter Check =
=A0
> clause is replaced by:
>
> =A0 =A0 C1: =A0 =A0bit__and(instance, 2) =3D 0 -> instance div 2 mod 2 =
=3D 0 .

If that is the conclusion left in the SIV file then the user rule to
prove it is:
   user_bitwise(1): bit__and(X, 2) =3D 0 -> X div 2 mod 2 =3D 0
may_be_deduced .

(and a minor comment is that it is probably not a good idea to use the
Proof Checker rule family names for Simplifier user rules - it just
adds to the confusion about how the rules are used.)

Cheers,

Phil