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

Re: [PVS-Help] Confused about proving extensionality of overriddenfunctions



David Coppit wrote:
> Hello all,
> 
> I'm trying to learn PVS, and need a gentle push in the right direction.
> 
> Assume this specification for a function-based implementation of stacks:
> 
>   stacks: THEORY BEGIN
> 
>     stack: TYPE = [# size: nat, elements: ARRAY[nat->int] #]
>     empty: stack = (# size:=0, elements:=(LAMBDA (j: nat): 0) #)
> 
>     push(x: int, s:stack): { s: stack | s`size>=1 } =
>       (# size:=s`size+1,
>          elements:=s`elements WITH [(s`size):=x] #)
> 
>     pop(s:stack | s`size>=1): stack =
>       (# size:=s`size-1,
>          elements:=s`elements WITH [(s`size-1):=0] #)
> 
>     % Hack for now
>     all_above_are_zero: LEMMA
>       FORALL (s: stack, x: int): x>s`size => s`elements(x) = 0
> 
>     push_pop: THEOREM
>       FORALL (s: stack, x: int): pop(push(x, s))=s
> 
>   END stacks
> 
> When proving push_pop, I start with
> 
>   (skolem!)
>   (expand* "push" "pop")
>   (lemma "all_above_are_zero" ("s" "s!1" "x" "s!1`size"))
>   (assert)
>   (apply-extensionality)
> 
> This results in the sequent:
> 
> [-1]  s!1`elements(s!1`size) = 0
>   |-------
> {1}   s!1`elements WITH [(s!1`size) := 0] = s!1`elements
> [2]   (# size := s!1`size,
>          elements := s!1`elements WITH [(s!1`size) := 0] #)
>        = s!1
> 
> Question #1: Now what? Shouldn't formula -1 be enough for formula 1?
> 

Yes, but you need to apply extensionality once more (since the equality
in {1} is between two functions).

> Question #2: I tried writing all_above_are_zero as an axiom, but didn't
> know how to utilize it in my proof. Is there some way to "use" an axiom?
> 

An axiom can be used like any other lemma/theorem in your theory.
Any proof command that takes lemma or theorem names as parameters
also accepts axiom names. For example, you can do
   (lemma "all_above_are_zero" ...)
if all_above_are_zero is stated as an axiom.

> Question #3: How do I rewrite my axiom so that it is higher-level, stating
> that all stacks are either the empty stack, or derived from it?
> 

The problem here is that "all_above_are_zero" is not true in your theory,
so turning it into an axiom will make the specification inconsistent.

You can change the definition of type "stack" so that all
stacks satisfy the constraint you want:

    stack: TYPE = { s: [# size: nat, elements: ARRAY[nat->int] #] | FORALL (x: nat): x > s`size => s`elements(x) = 0 }

then there's no need for any axiom anymore. But you'll get more TCCs to show
that empty/push/pop are type correct.

Another approach is to define a subtype of well-formed stacks inductively (where
well-formed means either empty, or obtained from empty by a sequence of push operations).
You keep the original definition of stack then define a well-formed predicate
by induction:

   well_formed(s: stack): INDUCTIVE bool =
       s = empty OR (EXISTS (s0: stack, x0: int): well_formed(s0) AND s = push(x0, s0))

Then you can define the type of well-formed stacks:

    good_stack: TYPE = { s: stack | well_formed(s) }

and now you can prove a variant of all_above_are_zero:

    all_above_are_zero_var: LEMMA
	FORALL (s: good_stack, x: nat) : x > s`size => s`elements(x) = 0


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