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

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

"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