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

Re: [PVS-Help] Deferring TCCs

PVS sub-typing mechanism is intended for this kind of situations. You
can declare:

first_one: THEORY 

  l: VAR (cons?[nat])
  first_one(l): bool = car(l) = 1

END first_one

cons? is the subtype of lists with at least one element. No TCCS are
generated during the type-checking of the theory. TCCs will be generated
for actual arguments of first_one and in most cases they will be
automatically discharged.


On Wed, 2005-01-05 at 05:09, robert wrote:
> Hi, is there a way of deferring TCCs generated from definitions to
> being checked where the definitions are used in a theorem?
> For instance, consider the following theory:
> first_one: THEORY BEGIN
> 	l: VAR list[nat]
> 	first_one(l): bool = car(l) = 1
> END first_one
> It generates one TCC:
> first_one_TCC1: OBLIGATION FORALL (l: list[nat]): cons?[nat](l);
> This can apparently never be satisfied, ie, every proof that
> depends on first_one will only ever be "proved - incomplete".
> However I can be careful with my use of first_one such that any time
> it is used in a theorem its actual parameter will satisfy the TCC
> (ie. is non-null).  (In fact, it seems to me that I would not be
> able to prove anything useful using first_one if the parameter is
> nonempty since 'car' is meaningless in this case.)
> Is there a general workaround that scales for many theorems like
> first_one with possibly non-trivial TCCs?  
> One option is to add "cons?(l) and" to the definition, but this is
> redundant if I know first_one will only be used in a context where
> cons?(l) is satisfied, and in general the approach can clutter
> the definitions if the conditions required to avoid generating 
> TCCs are nontrivial.  Perhaps there is another way of dealing with
> the situation, along the lines of using judgements.
> What I'd like to see is first_one generate a TCC 'flag', as above.
> Then consider a theorem which uses first_one, eg,
> 	importing first_one
> 	l: VAR list[nat]
> 		(forall l: l = (: 1 :) implies first_one(l))
> END th
> The theorem generates the TCC 
> 	(forall l: l = (: 1 :) implies cons?(l))
> Can this sort of behaviour be achieved in PVS?  Or is there some
> reason why it is a bad idea?  
> Rob
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
144 Research Drive                  http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855