Re: [PVS-Help] Unrecognized equality

[Cesar Munoz <munoz@xxxxxxxxxx>]

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