Re: [PVS-Help] Unrecognized equality

[Jerome <jerome@xxxxxxxxxxxxxx>]

Is there a way to get PVS to explicitly parenthesize? I'm running into
this issue again (in a separate proof) and it'd be nice to see what
PVS is thinking rather than trying to infer it. Thanks.

jerome

On Wed, Jun 25, 2008 at 06:01:03PM -0400, Cesar Munoz wrote:
>The reason you cannot replace -2 in 2 is that infix symbols are
>associated to the left. Therefore, what you have in 2 (lhs) is actually:
>
>((s!1(e!1) o fold(s!1, U!1)) o (fold(t!1, U!1)) o t!1(e!1))
>
>which doesn't match -2 (rhs):
>
>(fold(s!1, U!1) o (fold(t!1, U!1)) o t!1(e!1)).
>
>Before the replacement you have to use the fact that "o" is associative,
>and reorganize either -2 or 2.
>
>Cesar
>
>Jerome wrote:
>> Here's another equality that should be straighforward, but PVS doesn't
>> seem to understand:
>> 
>>   [-1]  t!1(e!1) o fold(t!1, U!1) = fold(t!1, U!1) o t!1(e!1)
>>   [-2]  (fold(s!1, U!1) o fold(t!1, U!1)) o t!1(e!1) =
>> 	  fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1))
>>   [-3]  fold(s!1, U!1) o fold(t!1, U!1) =
>> 	 fold(LAMBDA (k: D): s!1(k) o t!1(k), U!1)
>> 	  |-------
>>   [1]   U!1(e!1)
>>   {2}   s!1(e!1) o fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1)) =
>> 	 s!1(e!1) o t!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1))
>> 
>>   Rule? (replace -2 (2) :dir RL)
>>   No change on: (REPLACE -2 (2) :DIR RL)
>>   fold_distributive.2 :
>> 
>>   [-1]  t!1(e!1) o fold(t!1, U!1) = fold(t!1, U!1) o t!1(e!1)
>>   [-2]  (fold(s!1, U!1) o fold(t!1, U!1)) o t!1(e!1) =
>> 	  fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1))
>>   [-3]  fold(s!1, U!1) o fold(t!1, U!1) =
>> 	  fold(LAMBDA (k: D): s!1(k) o t!1(k), U!1)
>>     |-------
>>   [1]   U!1(e!1)
>>   {2}   s!1(e!1) o fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1)) =
>> 	  s!1(e!1) o t!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1))
>> 
>> What I want is for [2] to become:
>> 
>>   {2}   s!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1)) o t!1(e!1) =
>>           s!1(e!1) o t!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1))
>> 
>> What could be going on? Unlike my last mysterious equality, doing a
>> check of 'show-expanded-sequent' doesn't yield any red flags...
>> 
>> jerome
>> 
>> On Tue, Jun 24, 2008 at 03:25:55PM -0700, Jerome wrote:
>>> Does anyone know why the following doesn't produce Q.E.D in PVS?
>>>
>>>  {-1}  strict_subset?(K!1, J!1) IMPLIES
>>> 	  fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
>>>  [-2]  strict_subset?(K!1, J!1)
>>>    |-------
>>>  [1]   fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
>>>
>>>  Rerunning step: (ASSERT)
>>>  Simplifying, rewriting, and recording with decision procedures,
>>>  this simplifies to:
>>>  composable :
>>>
>>>  {-1}  fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
>>>  [-2]  strict_subset?(K!1, J!1)
>>>    |-------
>>>  [1]   fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
>>>
>>> After I make ASSERT call I would think the proof was finished... am I
>>> missing something? Thanks
>>>
>>> jerome
>>>
>> 
>> 
>
>-- 
>Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@xxxxxxxxxx
>National Institute of Aerospace         mailto:Cesar.A.Munoz@xxxxxxxx
>100 Exploration Way  Room 214       http://research.nianet.org/~munoz
>Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
>GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4
>