On constructing the data structure vs. relying on assumptions: I think both have their place. For example, in mathematics one typically constructs, say, the real numbers via Dedekind cuts, but presents algebraic structures such as groups through characteristic axioms. For our purposes, presentation through ASSUME leaves more freedom for later implementations of the data structure later, since only the stated properties have to be satisfied – but knowing when you have stated enough properties can be difficult.
Doesn't your approach essentially use CHOOSE to magically choose a model (basically, pull it out of thin air) in case the axiomatization isn't complete, in a way that is equally opaque to proofs? I mean, in the end, all the proofs have to work with is your assumptions, not any other property of a model that's been CHOsen (unless maybe those properties are known through existing algebras, like Nat ???)
THEOREM StackExistence == \A X : \E S,mt,ps,pp,tp : StackAxioms(X,S,mt,ps,pp,tp)
You'll also want to prove
StackAxioms(X, Stack(X), empty(X), ...)
so that you can actually reason about the specification. In that sense, you need to prove well-definedness upfront – but of course, that doesn't mean that your specification is complete, since you can only rely on what the axioms assert.
When you ASSUME the structure, you are not forced to justify the assumptions, although it would perhaps be good practice to make sure that you haven't introduced an inconsistency.
Stephan |