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

Re: [PVS-Help] TCC question


Note that when you write derivable[T](f), you are not declaring the type
of f, as f was defined somewhere.

For instance, when you write

sqrt_derivable_fun : LEMMA derivable[posreal](sqrt)

the type of sqrt is [nnreal -> real]. The type-checker tries to check
this type against [posreal -> real],  which is the type derivable

In some instances, PVS magically restricts the type of a function to the
type it expects. In this case sqrt : [nnreal->real] is automatically
restricted to LAMBDA(x:posreal):sqrt(x). This is the function that you
are actually passing to derivable. Use the Emacs command:
prettyprint-expanded (C-c C-q e) to see all the "invisible" coercions.

Now, in your case:  

inv_sqrt_derivable_fun: LEMMA derivable[posreal](1/sqrt)

the PVS type-checker fails to compute the coercion you expect. You can
solve the problem easily by explicitly writing the restriction:

inv_sqrt_derivable_fun: LEMMA

No TCC is generated in this case.

Hope that it helps,

On Tue, 2006-02-14 at 09:16, Francisco Jose CHAVES ALONSO wrote:
> Hello,
> I have the following LEMMA:
>   inv_sqrt_derivable_fun: LEMMA derivable[posreal](1/sqrt)
> By the definition of derivable, in the theory derivatives with the
> parameter posreal, I have that  1/sqrt is of type
>   posreal -> real 
> then the parameter of sqrt must be of type posreal, but my lemma
> generate the TCC
>   inv_sqrt_derivable_fun_TCC1: OBLIGATION FORALL (x1: nonneg_real):
> sqrt(x1) /= 0;
> That I can't prove. Why x1 in the TCC is not of type posreal as I
> expected and how can I solve it?
> Thanks in advance
> Francisco
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way                 http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988