Re: SPARK : surprising failure with implication

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Wed, 02 Jun 2010 09:42:58 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> (forall A,B in Boolean)
>
> not B => not A =
>    = not not B or not A =
>    = B or not A =
>    = not A or B =
>    = A => B
>
Yes, you confirmed that is right and so I'm not silly. But why Simplifier  
do not seems to know it ? It is the basis of inference logic. That is why  
I have such a weighty question in my mind : I wonder if I did something  
wrong somewhere or if something is broken.

Do you have an idea ?

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.