Implementing Stack with Pointer and Array

page 2

1 2 x

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 , ) = N
and
 ( A : Arr N I : Nat ) pop (< (s I) , put(N , I , A) >) = .
Conjunction elimination yields 3 subgoals:

pop (< 0 , nil >) = empty

We show pop (< 0 , nil >) = empty by circular coinductive rewriting.

( A : Arr N I : Nat ) top push(N , ) = N

Quantifier elimination introduces the new constant(s) a : Arr n, i : Nat .
We show top push(n , ) = n by reduction.

( A : Arr N I : Nat ) pop (< (s I) , put(N , I , A) >) =

Quantifier elimination introduces the new constant(s) a : Arr n, i : Nat .

We introduce the lemma

( A : Arr I J N : Nat )
 I <= J
 implies
 = .

Click here to see its proof.

We show pop (< (s i) , put(n , i , a) >) =  by circular coinductive rewriting.

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.

Left Up Down Right

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