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

[PVS-Help] TCC Question (Stack followup)



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
stack_as_function1: THEORY
BEGIN

Value: NONEMPTY_TYPE
Stack: TYPE = [# size: nat, elements: [nat -> Value] #]

is_empty?(s: Stack):bool = s`size = 0

Nonempty_Stack: TYPE = {s:Stack | NOT is_empty?(s)}

push(v: Value, s: Stack):Nonempty_Stack =
  (# size := s`size+1, elements := s`elements WITH [(s`size) := v ] #)

pop(s:Nonempty_Stack): Stack = 
  (# size := s`size-1, elements := s`elements #)

top(s:Nonempty_Stack):Value =
  s`elements(s`size-1)

equals(s1:Stack, s2:Stack):bool = 
  s1`size = s2`size AND
  FORALL (i:nat | i < s1`size):
    s1`elements(i) = s2`elements(i)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%pop_empty_is_empty: THEOREM
%  FORALL (s:Stack):
%    is_empty?(s) => is_empty?(pop(s))

not_empty_after_push: THEOREM
  FORALL (s:Stack, v: Value): NOT is_empty?(push(v,s))

push_pop_return_same : THEOREM
  FORALL (s:Stack, v: Value): equals(pop(push(v,s)),s)

top_element_after_push : THEOREM
  FORALL (s:Stack, v: Value): top(push(v,s)) = v

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

double_push_pop : THEOREM
  FORALL (s:Stack, v1: Value, v2: Value):
    equals(pop(pop(push(v2, push(v1,s)))), s)

%multiple_push_pop_of_nonempty_is_nonempty: JUDGEMENT
%  multiple_push_pop(s: Nonempty_Stack, values: list[Value]) HAS_TYPE
%    Nonempty_Stack

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)

multiple_push_pop_size: LEMMA
  FORALL (s:Stack, values: list[Value]):
    multiple_push_pop(s, values)`size = s`size

multiple_push_pop_values: LEMMA
  FORALL (s:Stack, values: list[Value], i:nat | i < s`size):
    multiple_push_pop(s, values)`elements(i) = s`elements(i)

multiple_push_pop: THEOREM
  FORALL (s:Stack, values: list[Value]):
    equals(multiple_push_pop(s, values), s)

END stack_as_function1