Re: [ProofPower] Proving properties of Z types.
On Wednesday 24 June 2009 16:07:02 Frank Zeyda wrote: >Since the HOL choice functions >(Choose) is not lifted to Z sets, incorporating it in a prove benefits >from a conversion that either lifts all set expressions into Z or HOL >sets. I didn't understand that bit. Though I do see that mu (which once used to be choice in Z) is definitely implemented as definite description (because Spivey decided to worry about choice and the standards group then followed suit), which is just a an exercise in making something less useful than it might have been and causing anyone who wants choice in Z a pain in the ... Presumably its easy enough to define a choice function in Z, and if you are working in axiomatic mode you won't even need to drop into HOL to get the definition validated. >My experience so far is that for the common stuff it is not >necessary to worry about underlying HOL encodings, but for the more >fancy things it is difficult to avoid it. If you start doing serious work in Z you will soon reach the limits of what can be done without knowing the underlying HOL. There are too many gaps in the Z proof automation for it to be otherwise. >PS: Is there, or would it be worth, to maintain a common repository of >ProofPower utilities and extensions such as additional conversions, >tactics, proof context, normalisations, hacks, little examples "how to >do" stuff, etc. implemented and shared by its users? It may not be >appropriate to incorporate all of them into the standard distribution, >but maybe other users could nevertheless benefit from them (I would >certainly be happy to contribute, and be interested in other users' >contributions). This hasn't happened possibily because the most extensive application of ProofPower has been by QinetiQ and they often place contracts with lemma-one for enhancements to ProofPower and the compliance tool to meet their needs. There are two ways at present for users to make their work available to others. These are also appropriate ways to submit material to Rob for him to consider whether it should be incorporated into the base. The first is patches, which applies mainly to fixing whats already there. There is a good description of how to use patches at: http://lemma-one.com/ProofPower/patches/contrib.html The other way of sharing is exemplified by Rob's maths_eqs. This involves preparing a tar file which can be distributed and which the user then unpacks and "make"s to get a new database with additional theories and or tactics etc. These things can be stacked. I have for some time done my work with ProofPower in that format, so at any time I can pack up a complete tar file of my ProofPower based work and post it off to someone else who can then replicate what I am doing. This was handy a little while ago when I found a bug, and enabled Rob to recreate the problem without any hazzle either for him or for me. My own tarfile builds on top of the maths_egs database. If you look at the maths_egs stuff its full of very solid stuff, and in particular the theory of analysis is not an "example", it is a major development of formalised mathematics and is on a larger scale than any work I have ever done. So you can see here, that Rob has a policy of not including in the distribution things which don't need to be there, even if they are solid and important. My own stuff is much more experimental, very varied, and shows the history of my painful acquisition of something like practical competence with ProofPower over many years (I didn't get much chance to do proofs in the days when ProofPower was being developed). So I don't expect anyone else to make use of my stuff, though there might be some useful ideas there. None of it is in Z so it won't be a lot of help to you, but there is a web page at: rbjones.com/rbjpub/pp/doc from which the tarfile is downloadable if you want to see or try it. The make file I use was adapted from the one in Rob's maths_egs, and knows how to build the databases, create the documents and how to build the distributable tarfile. Mine is now getting a bit complicated since I have been hacking at it for many years, so its better to start from the original if you want to do this. Rob did encourage me to set up a proper contrib system years ago, and I might have done something about it if I had ever had anything I though others might use, but my stuff is always far out on some limb or other, and I never produce nice clean complete pieces of work like those in maths_egs, so I never could motivate myself to do anything on a contrib system. Anyway, let me know if I can be of any further help. Roger Jones PS I should add that I am not associated with lemma-one in any formal way, and do not speak for lemma-one or Rob Arthan. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Proving properties of Z types.
Dear Roger, Many thanks for the reply to my message. > It seems odd for an alphabet to be a set of names, > it sounds more like a set of characters from which > one might form names as sequences. Yes, the initial model I used was more abstract in that NAMES did not have an identity e.g. as a string. I recently changed the model to give names a proper identity as a sequence of characters, so the below issue does not exists anymore - infinity should be provable here. I was interested to settle an answer nevertheless. > I'm puzzled where this came from. > In ProofPower when you introduce a given set NAME you get a > new HOL type z'NAME (as you say) about which nothing is specified > (but all types are non-empty), and you get a new Z constant NAME > defined by NAME = BBU. > BBU (the double bold U symbol) is difficult to unpick because > for Z it behaves as a primitive, but it is in fact the set of > all elements of the type x'NAME. The proof system knows enough > about BBU that you should not need to think about what's happening > underneath but simply understand that it is the set of all elements > of some type, and the type will be determined by type inference. Yes, when taking BBU apart one can verify that it is just an abbreviation for Totality (instantiated for some suitable type), which in turn is equated with Universe (instantiated for some suitable type). (Actually that's not quite true, the actual Z characterisation of BBU is "(Totality).1" but the tuple construction and selection will in effect cancel each other out). The axiom for the universe is given by the the definition of "Universe" in the HOL sets theory, and determine the (sole) properties of the carrier set. It is what I was referring to. > Though it might be better in this case to use > > F NAME propersubsetof P NAME Great, that would be a better choice of infinity axiom to prove the property I needed. As you suggest, there should be no issue about writing the infinity axiom in a certain way, best to chose whatever is more convenient for proof. > Yes. However, you should not really need to know any of the > stuff about how this is done in HOL. > The given sets are implemented as they should be in Z > and U is well understood by the Z proof contexts. Yes, I needed to dig a bit deeper just to verify what you confirmed in the email, it might have been quicker to look at the Z standard ;-) . As you said, in general there is no need to go down to the level of HOL when reasoning about Z sets, but as a side note this appear not always to be so. For example, to prove theorems about set or sequence enumerations, e.g. all enumerated sets are finite, I had to decent to the level of HOL. Also I have been developing some more elaborate normalisation conversions for Z sets, and the constructor functions sort_conv and poly_conv usually only work with HOL functions. (There is a minor issue with poly_conv and sort_conv as these conversion only work for functions whose types are fully qualified, I will posting another message to make a suggestion here ;-) . Since the HOL choice functions (Choose) is not lifted to Z sets, incorporating it in a prove benefits from a conversion that either lifts all set expressions into Z or HOL sets. My experience so far is that for the common stuff it is not necessary to worry about underlying HOL encodings, but for the more fancy things it is difficult to avoid it. > The place to look for theorems about finiteness is in > the maths examples, wrk073.pdf, not part of the standard > distribution. > However, this is all HOL, so to use it in Z you will need > to understand the relations between HOL and Z. Many thanks for the reference. Yes, no problem. I implemented two conversions that negotiated between Z and HOL sets, hence it should be easy to use HOL laws if needed. > However, I'm not convinced that you need it for the purposes > described. If you just add the constraint I mentioned above > then you should always be able to find new elements (I suppose > you need to know that the union of two finite sets is finite). I managed to find a general theorem in "z_numbers1" that states that the generalised union of a finite number of finite sets is finite, for convenience I specialised it for the binary case. > A proof context would be nice! Certainly, I will try and play around with this. Wrapping all relevant theorems in a component proof context and maybe merging with sets_ext could be a nice general solution. Thanks once more for the reply, Frank PS: Is there, or would it be worth, to maintain a common repository of ProofPower utilities and extensions such as additional conversions, tactics, proof context, normalisations, hacks, little examples "how to do" stuff, etc. implemented and shared by its users? It may not be appropriate to incorporate all of them into the standard distribution, but maybe other users could nevertheless benefit from them (I would ce
Re: [ProofPower] Proving properties of Z types.
I should have supplied references in my last (for Rob's material on finiteness): http://lemma-one.com/ProofPower/examples/examples.html http://lemma-one.com/ProofPower/examples/wrk073.pdf http://lemma-one.com/ProofPower/examples/PPZEgs.tgz Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Proving properties of Z types.
On Tuesday 16 June 2009 14:47:55 Frank Zeyda wrote: >Dear ProofPower Users, > >I have a little observation which I would like to confirm. The problem >is as follows. I defined a new Z type NAME by > >[NAME] > >and then introduced a set ALPHABET to refer to the subsets of NAME by > >ALPHABET == P NAME It seems odd for an alphabet to be a set of names, it sounds more like a set of characters from which one might form names as sequences. >At some point it showed to be necessary to construct fresh names for any >given alphabet, i.e. which are not in the alphabet. In that, I attempted >to prove the following theorem. > >FORALL a : ALPHABET @ (EXISTS n : NAME @ n \not \in a) > >I assumed it would be sufficient to restrict the set alphabet to finite >subsets of name, for instance using the following definition for >ALPHABET instead. > >ALPHABET == F NAME > >but I think this is not the case. For a new Z type, the defining axiom >we obtain is that the Z type constant (i.e. NAME) is equal to the >universe over a certain, newly introduced, HOL type (here z'NAME); a HOL >constant "Universe" is used to refer to the carrier set of a HOL type. >It guarantees that any x of the correct (HOL) type is an element of the >respective (type-instantiated) Universe, that x is not an element of the >empty set which I suppose excludes the case of an empty universe, and a >property regarding the Insert functions to reason about enumerated sets. I'm puzzled where this came from. In ProofPower when you introduce a given set NAME you get a new HOL type z'NAME (as you say) about which nothing is specified (but all types are non-empty), and you get a new Z constant NAME defined by NAME = BBU. BBU (the double bold U symbol) is difficult to unpick because for Z it behaves as a primitive, but it is in fact the set of all elements of the type x'NAME. The proof system knows enough about BBU that you should not need to think about what's happening underneath but simply understand that it is the set of all elements of some type, and the type will be determined by type inference. > From this alone one cannot prove that the corresponding Universe is >infinite. yes, it might be finite, for all anyone knows. >The underlying HOL type of the new Z type, i.e. here "z'NAME >SET" I think defines a representation function that equates the type of >a set with functions over some new HOL type into BOOL, but again I think >this cannot be used to prove that "z'NAME SET" is infinite unless >"z'NAME" is (?!). Yes. The HOL type constructor SET, which is used also for sets in Z, is represented by propositional functions. In HOL SETs are just different ways of talking about propositional functions. (though you can introduce other kinds of set if you like)> >In that, I suppose if we want a Z type to be infinite, >we need to explicitly state it, that is by an axiom along the lines of > >EXISTS f : z'NAME -> z'NAME @ (OneOne f) /\ ¬ Onto f > >(Similar to the infinity_axiom in the HOL theory init.) Though it might be better in this case to use F NAME propersubsetof P NAME >Or alternatively (maybe more useful when doing the proofs in Z rather >than HOL) that there exists an injective Z function from N to the >carrier set of the new type. The only type in ProofPower-Z that >explicitly claims its infinite seems to be the type IND. Though there are many others which are easily seen to be. e.g. N or seq T for any type T. >However, there >seems no way to prove that for a newly introduce HOL type there is an >injective function from IND to the elements of that. Even further, it >seems not possible to prove that there are two distinct elements in a >newly introduced Z type. For example, the consistency axioms for > >| x, y : NAME > >- > >| x =/= y > >Appear not to be provable by the defining axiom for NAME, unless we >introduce some axiom stating properties of the cardinality of NAME. All this is consistent (I believe) with the Z standard. >If someone could confirm or refute the above that would be great. Yes. However, you should not really need to know any of the stuff about how this is done in HOL. The given sets are implemented as they should be in Z and U is well understood by the Z proof contexts. >As a side-issue, I realised the automatic proof support for finite sets >is not as well developed as that for (possibly infinite) sets. I proved >a couple of theorems that could be useful, for instance discharging that >every enumerated set is finite. It may be worth introducing a new Z >component proof context for finite sets. The place to look for theorems about finiteness is in the maths examples, wrk073.pdf, not part of the standard distribution. However, this is all HOL, so to use it in Z you will need to understand the relations between HOL and Z. However, I'm not convinced that you need it for the purposes described. If you just add the constraint I mentioned above then you should always be able to find new elements (I suppose you ne
