From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,d4e6b104ff087788
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!usenet-fr.net!gegeweb.org!aioe.org!not-for-mail
From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?=
 =?utf-8?Q?=29?=
 <yannick_duchene@yahoo.fr>
Newsgroups: comp.lang.ada
Subject: Re: SPARK : surprising failure with implication
Date: Wed, 02 Jun 2010 10:50:55 +0200
Organization: Ada At Home
Message-ID: <op.vdnz65ucule2fv@garhos>
References: <op.vdmxbejnule2fv@garhos>
NNTP-Posting-Host: FWfoAwrKC5rz12vcTu3tlw.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
X-Notice: Filtered by postfilter v. 0.8.2
User-Agent: Opera Mail/10.53 (Win32)
Xref: g2news2.google.com comp.lang.ada:12190
Date: 2010-06-02T10:50:55+02:00
List-Id: <comp.lang.ada>

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.