Re: Lost in translation (with SPARK user rules)

[stefan-lucks@see-the.signature]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 1088 bytes --]

On Thu, 27 May 2010, Yannick Duch�ne (Hibou57) wrote:

> Le Thu, 27 May 2010 10:13:55 +0200, Yannick Duch�ne (Hibou57)
> <yannick_duchene@yahoo.fr> a �crit:
> >
> >That is, if there a user rule of the form
> >
> >    my_rule(1) Conclusion_1 may_be_deduced_from [Expression_1].
> >
> >and the source unfortunately contains only
> >
> >    Expression_2
> >
> >then try something like
> >
> >    --# check Expression_2 -> Intermediate_Expression(1);
> >    --# check ...;
> >    --# check ...;
> >    --# check Intermediate_Expression(N) -> Expression_1;
> >
> >and here it is.
> 
> Unfortunately, I came into another trouble. I was trying this, and used
> intermediate variables to help. But Simplifier insist on using expressions
> instead of variables, so it can't find a match.

Wouldn't it be much simpler to use the proof checker, instead of the 
simplifier?

Stefan

-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------