helphome pageduck scriptspecificationfirst proof pagepage 2page 1 1 2 xclosing page

Implementing Stack with Pointer and Array
This time we succeed using the lemma.


We want to prove
      pop (< 0 , nil >) = empty
and
       ( A  : Arr  N  I  : Nat  ) top push(N , < I , A >) = N
and
       ( A  : Arr  N  I  : Nat  ) pop (< (s I) , put(N , I , A) >) = < I , A > .
Conjunction elimination yields 3 subgoals:
  1. pop (< 0 , nil >) = empty
  2. ( A  : Arr  N  I  : Nat  ) top push(N , < I , A >) = N
  3. ( A  : Arr  N  I  : Nat  ) pop (< (s I) , put(N , I , A) >) = < I , A >

And thus the main goal is proved.

Explanation

As in the previous attempt, the first rule applied is conjunction elimination, resulting in three subgoals, with the first succeeding by circular coinduction and the second by reduction. But now the third subgoal succeeds using circular coinduction, after the lemma has been introduced. Since the proof failed on the previous page without the lemma, we know that the lemma is needed.


BOBJ proof scoreLeft    Up    Down    Right   
 

       This page was generated by Kumo on Tue Feb 13 19:32:22 PST 2001.