387 Prove that the following definitions implement the simple data-stack theory. stack = [nil], [stack; X]
push = 〈s: stack→ 〈x: X→ [s; x]〉〉 pop = 〈s: stack→ s 0〉
top = 〈s: stack→ s 1〉
§ Consider the implementation to be four axioms, named by their left sides. Now I prove each of the axioms of simple data-stack theory. First, stack ⧧ null by contradiction.
stack = null
= stack = null ∧ stack = [nil], [stack; X] ⇒ null = [nil], [null; X]
= null = [nil], null
= null = [nil]
⇒ ¢ null = ¢ [nil]
= 0 = 1
=⊥
Let s:stack and x:X. Then
conjoin stack axiom context, then specialize [ ] distributes over , null is identity for , transparency size axioms; note that [nil] is an element because all 0 of its items are elements arithmetic axiom
push s x : stack
= 〈s: stack→ 〈x: X→ [s; x]〉〉 s x : [nil], [stack; X]
= [s; x]: [nil], [stack; X] ⇐ [s; x]: [stack; X] =⊤
pop (push s x) = s
= 〈s:stack→s0〉〈s:stack→〈x:X→[s;x]〉〉sx=s
= 〈s: stack→ s 0〉 [s; x] = s
= [s; x] 0 = s =⊤
top (push s x) = x
= 〈s:stack→s1〉〈s:stack→〈x:X→[s;x]〉〉sx=x
= 〈s: stack→ s 1〉 [s; x] = x
= [s; x] 1 = x
=⊤
The last step, indexing, requires x to be an item, so this implementation requires X to be a bunch of items.
use push and stack axioms apply generalization
use pop and push axioms apply apply index
use top and push axioms apply apply index