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

*To*: pvs-help@csl.sri.com*Subject*: type vs. set*From*: Hanne Gottliebsen <hago@dcs.st-and.ac.uk>*Date*: Wed, 20 Oct 1999 15:55:36 +0100 (BST)

I am having difficulties proving a particular TCC, and as far as I can see my problem comes from not being able to deduce from (fullset[T])(u) that T_pred(u) is true. I am using PVS2.3 Here is an example: notation : THEORY BEGIN x, y, z : VAR real T : VAR set[real] closed_interval(x,y) : set[real] = { z : real | x <= z AND z <= y } compact_interval_subset?(x,y,T) : bool = x <= y AND subset?(closed_interval(x,y),T) END notation test[ T : NONEMPTY_TYPE FROM real ] : THEORY BEGIN IMPORTING notation R((f:[T -> real]), (c:T), (d: {x:T | compact_interval_subset?(c,x,fullset[T])} )) : [(closed_interval(c,d)) -> real] = LAMBDA (u : (closed_interval(c,d))) : f(u) END test To explain: R is the restriction of f to a compact (closed and bounded) interval, which is also a subset of fullset[T]. The generated TCC is: R_TCC1: OBLIGATION FORALL (c: T, d: {x: T | compact_interval_subset?(c, x, fullset[T])}, u: (closed_interval(c, d))): T_pred(u); This is a reasonable TCC, and it is obviously true (once one unfolds the definitions!). Using grind gives this: {-1} T_pred(c!1) {-2} T_pred(d!1) {-3} c!1 <= d!1 {-4} c!1 <= u!1 {-5} u!1 <= d!1 |------- {1} T_pred(u!1) which looks hopeless to me. By hand one can easily get to: [-1] T_pred(c!1) [-2] T_pred(d!1) [-3] c!1 <= d!1 {-4} member(u!1, closed_interval(c!1, d!1)) => member(u!1, fullset[T]) [-5] closed_interval(c!1, d!1)(u!1) |------- [1] T_pred(u!1) However, any further expansion only leads to the same result as grind above (not a big surprise, I guess). Now, can I actually prove this TCC, or can I change my definition of R to something equivalent which will work? Thanks, Hanne --------------------------------------------------------- Hanne Gottliebsen Office P337 Dept. of Computer Science Ph: +44 1334 46 3265 University of St Andrews hago@dcs.st-and.ac.uk - Who moved the stone? ---------------------------------------------------------

- Prev by Date:
**help with a question about unions (and sums)** - Next by Date:
**Re: type vs. set** - Prev by thread:
**Re: Help about Induction Scheme defination!** - Next by thread:
**Re: type vs. set** - Index(es):