Re: Lost in translation (with SPARK user rules)

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 26 May, 11:09, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
[...]
> I tried with this:
>
>     bitwise(112): bit__and(X div (2**N), 1)=0 may_be_deduced_from [  
> (bit__and(X, 2**N)=0), X>=0, N>=0 ].
>     bitwise(113): bit__and(X, 2**N)=0 may_be_deduced_from [ (bit__and(X div  
> (2**N), 1)=0), X>=0, N>=0 ].
>
> But this fails, although the simplifier does not returns me any syntax  
> error messages about this *.RLU file. This fails, because it cannot prove  
> something like this:
>
>     --# check ((Instance and 2) = 0) -> (((Instance / 2) and 1) = 0);
>
> The latter should be directly deduced from the two previous rules if these  
> were OK. So I suppose something is wrong with these rules, and the  
> expression in “[...]” 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 “and 1” is always replaced by “mod 2”  
> in the simplifier's *.SIV output files. As an example, the latter Check  
> clause is replaced by:
>
>     C1:    bit__and(instance, 2) = 0 -> instance div 2 mod 2 = 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) = 0 -> X div 2 mod 2 = 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