Re: [PVS-Help] TCC Question (Stack followup)

[Bruno Dutertre <bruno@csl.sri.com>]

David Coppit wrote:
> On Mon, 3 Oct 2005, Jeff Maddalon wrote:
> 
>> Now back to the version with TCCs.  Since the TCCs arise in the 
>> definition of
>> multiple_add_sub, you cannot "expand" multiple_add_sub.  In the same 
>> way as
>> trying to prove gt0, you will need more information about the return 
>> type.
> 
> 
> First, thanks to jeff and Bruno for helping me to understand the issue.
> 
> One final question: What do I do in cases where the value of the return
> type cannot be easily expressed in terms of the arguments?
> 
> e.g. This works:
> 
>   multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | u=x } =
>     IF y=0 THEN
>       x
>     ELSE
>       multiple_add_sub(x+1,y-1)-1
>     ENDIF
>   MEASURE y
> 
> but this does not:
> 
>   multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | y>0 => u>0 } =
>     IF y=0 THEN
>       x
>     ELSE
>       multiple_add_sub(x+1,y-1)-1
>     ENDIF
>   MEASURE y
> 

You don't have to write x=u. For typecheking, the important property
is that multiple_add_sub(x, y) > 0 when x>0 so there are many options.
You could write

     multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | x>0 => u>0 }

or  multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | u >= x  }

etc.


> In the above I was trying to just provide the type information and not
> x=u. If I have to provide x=u, I wonder what I would do for a nasty
> function whose value isn't easily expressed in terms of the arguments:
> 
>   complex(x:nat, y:nat): RECURSIVE { u: nat | u=??? } =
>     IF y=0 THEN
>       x
>     ELSE
>       complex( (x+1) * y * complex(x+2,y-1), y-1)-1
>     ENDIF
>   MEASURE y
> 

That's the same thing here. The type {u: nat | x>0 => u>0 } would work.

Bruno

> Thanks,
> David
> 
> _____________________________________________________________________
> David Coppit                           david@coppit.org
> The College of William and Mary        http://coppit.org/
> 
> "They have computers, and they may have other weapons of mass destruction."
> Former Attorney General Janet Reno, speaking at LLNL of modern criminals
> 


-- 
Bruno Dutertre                             | bruno@csl.sri.com
CSL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717