SPARK : surprising failure with implication
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 1 Jun 2010 14:51 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 2 Jun 2010 00:34 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 2 Jun 2010 03:42 (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 2 Jun 2010 03:56 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 2 Jun 2010 04:50
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. |