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

```David,

I guess that you can prove that property by induction. However, you can
take advantage of the PVS typing features to specify multiple_push_pop in
different way.

First, define

Stack: TYPE = [# size: nat, elements: [below(size) -> Value] #]

(Note that you don't need the the predicate equals any longer)

Then,  specify

multiple_push_pop(s: Stack, values: list[Value]): RECURSIVE
{s1 : Stack | s1 = s}  =
IF (values = null) THEN
s
ELSE
LET (first_value, remaining_values) = (car(values), cdr(values)) IN
pop(multiple_push_pop(push(first_value,s), remaining_values))
ENDIF
MEASURE length(values)

All tccs are proven automatically, except for the following two (manually
prove them first as it takes several minutes if you let PVS to prove them
automatically):

%|- multiple_push_pop_TCC3 : PROOF
%|- (then
%|-   (skosimp*)
%|-   (typepred "v!1(push(first_value!1, s!1), remaining_values!1)")
%|-   (grind))
%|- QED

%|- multiple_push_pop_TCC4 : PROOF
%|- (then (skosimp*)
%|-   (beta)
%|-   (typepred "v!1(push(car(values!1), s!1), cdr(values!1))")
%|-   (replace -1 :hide? t)
%|-   (branch (decompose-equality 2)
%|-           ((grind)
%|-            (then (decompose-equality 1) (grind)))))
%|- QED

The new specificiation of multiple_push_prop is stronger than the previous
one and you get the
lemmas:

multiple_push_pop_size,
multiple_push_pop_values,
multiple_plush_pop,

by free.

I attach the PVS files.

Cesar
David Coppit said:
> Hello all,
>
> This is a followup to my previous stack question. Suppose I defined a
> predicated subtype of Stack called Nonempty_Stack, in order to define
> the "top" operation on only nonempty stacks.
>
> Now, later, I have a recursive function called multiple_push_pop:
>
>    multiple_push_pop(s: Stack, values: list[Value]): RECURSIVE Stack =
>      IF (values = null) THEN
>        s
>      ELSE
>        LET (first_value, remaining_values) = (car(values), cdr(values))
> IN
>          pop(multiple_push_pop(push(first_value,s), remaining_values))
>      ENDIF
>    MEASURE length(values)
>
> I have a TCC now to prove that the result of the recursive call to
> multiple_push_pop(push(first_value,s), remaining_values) returns a
> nonempty stack:
>
>    multiple_push_pop_TCC3 :
>
>      |-------
>    {1}   FORALL (s: Stack, values: list[Value],
>                  v:
>                    [{z: [Stack, list[Value]] |
>                              length(z`2) < length(values)} ->
>                       Stack]):
>            NOT (values = null) IMPLIES
>             (FORALL (first_value: Value, remaining_values: list[Value]):
>                remaining_values = cdr(values) AND first_value =
> car(values)
>                 IMPLIES
>                 NOT is_empty?(v(push(first_value, s),
> remaining_values)))
>
> How do I go about proving this?  Attached is the complete .pvs file.
>
> Thanks,
> David

--
Cesar A. Munoz H., Senior Staff Scientist
National Institute of Aerospace
100 Exploration Way
Hampton, VA 23666, USA
Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988

```

stack_as_function.pvs

stack_as_function.prf