[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: Jerome <jerome@xxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] R_pred*From*: Cesar Munoz <munoz@xxxxxxxxxx>*Date*: Fri, 07 Nov 2008 16:26:03 -0500*Cc*: PVS Help <pvs-help@xxxxxxxxxxx>*In-reply-to*: <20081107205525.GD3397@cs.caltech.edu>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20081106233402.GA16079@cs.caltech.edu> <49144822.5010608@nianet.org> <20081107205525.GD3397@cs.caltech.edu>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Thunderbird 1.5.0.14ubu (X11/20080925)

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

**References**:**[PVS-Help] R_pred***From:*Jerome

**Re: [PVS-Help] R_pred***From:*Cesar Munoz

**Re: [PVS-Help] R_pred***From:*Jerome

- Prev by Date:
**Re: [PVS-Help] R_pred** - Next by Date:
**Re: [PVS-Help] R_pred** - Previous by thread:
**Re: [PVS-Help] R_pred** - Next by thread:
**Re: [PVS-Help] R_pred** - Index(es):