Re: SPARK : surprising failure with implication

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

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.