Re: [PVS-Help] R_pred

[Cesar Munoz <munoz@xxxxxxxxxx>]

Jerome wrote:
> I think my problem comes from a misunderstanding as to what R_pred
> actually is. One of the parameters of my theory is 'R', which is a
> numeric type:
> 
>   R: TYPE FROM nnreal
> 
> Within the theory, distance and W are functions from some type to R:
> 
>   distance: [D -> R]
>   W: [D, D -> R]
> 
> Thus, to discharge [1] do I need to show that the addition of two
> non-negative real numbers is still a non-negative real number? My
> original question stems more from surprise (and lazyness) that this
> wasn't taken care of by some prelude magic :)
> 
> Is this what [1] wants me to show?

No. That is not what [1] wants you to show. R is an arbitrary TYPE that
consist of  non-negative numbers. R_pred is the characteristic predicate
of R, i.e.,

x:R

is equivalent to

x: (R_pred)


Formula [1] wants you to prove that for an arbitrary R, R(x) and R(y)
implies R(x+y), where x and y are W(...) and distance(...), respectively.

This is not true. Take as R the type of non-negative odd numbers. Then,
you have that R(3) and R(5), but R(3+5) is not true. You have to say
something more about R, for example that it's a subset of non-negative
numbers that is closed under addition.

Cesar




 And, in general, how do I interpret
> the _pred convention? Thanks
> 
> jerome
> 
> On Fri, Nov 07, 2008 at 08:52:34AM -0500, Cesar Munoz wrote:
>> Why should it work ? What is the definition of R?  For an arbitrary R,
>> the fact that R(x) and R(y) hold doesn't imply that R(x+y) holds. Take
>> R=odd? for example.
>>
>>
>> Jerome wrote:
>>> I have the following:
>>>
>>>    [-1]  W(root, j!1) >= 0
>>>    [-2]  R_pred(W(root, j!1))
>>>    [-3]  distance(s!1)(root) >= 0
>>>    [-4]  R_pred(distance(s!1)(root))
>>>      |-------
>>>    [1]   R_pred(distance(s!1)(root) + W(root, j!1))
>>>
>>> Why is "assert" not an adequate means of discharging? What am I
>>> missing? 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
>>
> 
> 

-- 
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