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

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



David,

There is even a different solution using dependent types.

stack : THEORY
BEGIN

  stack : TYPE = [#
    size    : nat,
    elements : ARRAY[below(size)->int]
  #]

  s : VAR stack
  x : VAR int

  nonempty?(s) : bool = s`size > 0

  n: VAR (nonempty?)

  empty : stack = (# size := 0, elements := LAMBDA(x:below(0)):0 #)

  push(x,s) : stack = (#
    size := s`size+1,
    elements := s`elements WITH [(s`size) := x]
  #)

  pop(n) : stack = (#
    size :=  n`size - 1,
    elements := LAMBDA(x:below(n`size-1)):n`elements(x)
  #)

  push_pop : THEOREM
    pop(push(x,n)) = n
  %|- push_pop :
  %|- PROOF (then (skosimp)
  %|-                        (branch (decompose-equality)
  %|-                                ((grind) (then (decompose-equality)
  %|-                                               (grind)))))
  %|- QED

END stack

David Coppit said:
> 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?
>
> 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?
>
> 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?
>
> 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


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