From: Yannick Duchêne (Hibou57) on
Hi all,

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

--# check (Source = 1) -> ((Source mod 2) = 1); -- (1)
--# check (Source mod 2) /= 1; -- (2)
--# check Source /= 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 “(Source mod 2) /= 1” as
an equivalent of “not ((Source mod 2) = 1)”, so I tried this:

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


Hem, I'm not silly (or am I?), where “A -> B” is valid, then “not B -> not
A” is valid too.

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

--# check (Source = 1) -> ((Source mod 2) = 1); -- (1)
--# check (not ((Source mod 2) = 1)) -> (not (Source = 1)); -- (1-bis)
--# check not ((Source mod 2) = 1); -- (2)
--# check not (Source = 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 “not (A = B)” into “A /= B)” (i.e.
“A <> B”, in an *.SIV file).

What I suspect: as Simplifier turns “not A = B” into “A /= B”, it cannot
see it as the negation of the antecedent and consequent of the implication
proved in (1), so from A -> B proved, I cannot prove not B -> not A, while
logically speaking, I know “(A -> B) <-> (not B -> not A)”.. But it still
recognize “not ((Source mod 2) = 1)” as equivalent to “(Source mod 2) /=
1”, 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).
From: Yannick Duchêne (Hibou57) on
Le Tue, 01 Jun 2010 20:51:04 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene(a)yahoo.fr> a écrit:

> Hi all,
>
> In an Ada/SPARK source, I had something like this:
>
> --# check (Source = 1) -> ((Source mod 2) = 1); -- (1)
> --# check (Source mod 2) /= 1; -- (2)
> --# check Source /= 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).
>
> [...]

Although late, I'm back to this topic.

I added this user rule:

my_logic(1): not B -> not A may_be_deduced_from [ (A -> B) ].

While this was looking so much obvious, I though the Simplifier already
knew it and this would probably change nothing. But this did change
something! Now the above sequence of hypothesis->conclusion is proved.

Did I made something wrong somewhere ? Did I brake something somewhere ?
Why is not this fundamental rule embedded in the Simplifier ?

I was so much surprised, that I checked it (yes, what looks obvious is
sometimes good to check). Can't say anything else that “yes, this is true”.

(A) (B) (A->B)
F F T
F T T
T F F
T T T

(not B) (not A) (not B -> not A)
T T T
F T T
T F F
F F T

(A -> B) (not B -> not A) ((A -> B) -> (not B -> not A))
T T T
T T T
F F T
T T T

This is indeed tautology.

OK, that is solved, but I'm still somewhat frightened by what I don't
understand in this experience : why did I need to add a user rule for that
? What was wrong ?


--
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.
From: Dmitry A. Kazakov on
(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

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
From: Yannick Duchêne (Hibou57) on
Le Wed, 02 Jun 2010 09:42:58 +0200, Dmitry A. Kazakov
<mailbox(a)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.
From: Yannick Duchêne (Hibou57) on
Not exactly with implication this time, this is about equality and
substitution.

Here is a case I am facing (simplified for the purpose of this message):

--# assert S = (I / X); -- (1)
--# check S = T'Pos (S); -- (2)
--# check I = T'Pos (I); -- (3)
--# check T'Pos (S) = (T'Pos (I) / X); -- (4)

(1) is proved
(2) and (3) are proved
Simplifier fails to prove (4) despite of (1) and equalities (2) and (3)
which should be used to substitute S and I in (1).

I still did not found a workaround for this one (I am busy at this now).

Does anyone already meet a case similar to this one ? Does it fails for
the reason it requires two substitutions at a time ?

S and I are both of type same T (which is a modular type). Anyway, this
should not be of any importance, as what is this about here, is that two
equalities are not used for a substitution where it could expected to be.

It is not possible to use an intermediate step like...

--# check S = (T'Pos (I) / X); -- (4.1)
--# check T'Pos (S) = (T'Pos (I) / X); -- (4.2)

....because on (4.1), this would be an Universal_Integer expression on the
right side with an expression of type T on the left side, which is not an
allowed ; so there is no way to avoid the need for two substitutions at a
time.