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

```On Friday 23 September 2005 12:13 pm, 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
>
>
>    (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?

"elements" is a function that also needs extensionality.  Try:

(hide 2)
(apply-extensionality)

> 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?

Axioms can be viewed as lemmas that don't need proofs.  All the standard
ways to "use" a lemma can be used for an axiom: (lemma ...) (use ...)
(rewrite ...) (forward-chain ...)

> 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?

This is probably more complicated than you want to get into.  May I suggest
that you drop the idea of an axiom and just define equal in a more limited
way.  Say:

equal(s1:stack, s2:stack): boolean =
s1`size = s2`size AND
(FORALL (i:nat) : i<s1`size => s1`elements(i) = s2`elements(i))

Then push_pop becomes:

push_pop: THEOREM
FORALL (s: stack, x: int): equal(s, pop(push(x, s)))

Good luck,

Jeff

```