NOTES ON VERSIONS OF THE MARK2 PROVER New stuff is now added at the beginning of the file! Note that version information about the Watson prover is found in the source file, in a format similar to this. June 4: New official version of the prover posted. In addition to the changes already embodied in the draft source of May 17, the script command has been modified so that it automatically invokes thmsonly when it starts up and speakup when it stops. (also setpause and setnopause). It no longer pauses when it issues the message that a script has already been run; it still stops for all other messages. If it is desired to run a script in verbose mode, the "scriptinscript" command will do this (the reason for the name is that this is the version of script which the script command itself invokes internally). I do not necessarily have confidence in all the new features since the last official version; please tell me about any bugs... May 29: No change to prover; extensive modifications of files natorder.mk2 and realorder.mk2. The latter file, which is not yet complete, is a theory of the order relation on the reals which is now invoked as part of the omnibus theory (it is called at the end of algebra2.mk2). An error in the definition of =< and >= in natorder.mk2 was corrected. Some theorems at the end of natorder.mk2 are in the process of being modified to more useful forms. May 17: corrected error in the implementation of UNEVAL in the draft version. May 14: A new built-in tactic UNEVAL has been added. The effect of UNEVAL@[---?1---] is to convert terms of the form ---?t--- to the form [---?1---]@?t (the reverse of EVAL); this makes it possible to get tactics to find terms of more general forms. For example, if we run (UNEVAL@[?1=?1]) => (?a+?b)=?a+?b we should get [?1=?1]@?a=?b This tactic needs to be tested. I'm hoping that it will be useful in the context of induction proofs and proofs involving quantifiers. These changes are only reflected in the draft version. January 9: Two changes, now available in the draft version only: It is now possible to declare infixes containing alphanumeric characters. They must start with the backquote "`". `plus is a legitimate infix, and so are things like *`2 which begin with special characters and have a ` followed by alphanumerics at the end (this possibility of "subscripting" infixes is important, I think, and it is a complete accident!) Be sure to provide space between alphanumeric infixes and following terms! The other change is that the "prove" command and its relatives no longer save the environment to the desktop, and the script command no longer clears saved environments. The reason for this is to make it possible to use saved environments created during scripts after the script is run; most "junk" saved environments have been created in the course of proofs, so I doubt that the desktop or saved theories will get too cluttered in practice. Something to note: one can use saved environments in proofs (as lemmas) using the "applyenv" and "applyconvenv" commands; this allows one to prove equations needed for a particular proof and use them repeatedly during the proof (though not with the same freedom as theorems) and be able to get rid of them when they are no longer needed! (This is not a new feature, just a note on strategy). An important use of saveenv is to save long proofs at various stages so that one does not need to re-run the entire proof. It was in the course of using these ideas in combination with repeatedly rerunning a script that the need for the second change became apparent. Try out the new infixes and tell me if you find any bugs. October 10: Minor modification: setprecedence was added to the list of commands understood by the script reader. New version is needed for combinators.mk2 to be understood correctly; otherwise not a big deal. Sol Espinosa's simplesets.mk2 file has been added to the Web page. The set definitions originally found in logicdefs.mk2 have been commented out. August 29: BUG FIX!!! There was a serious problem with steps; under certain conditions, it would get the numbering of hypotheses wrong, with disastrous effects. This was a nasty bug because intermittent; steps wasn't initializing an environment variable it needs, but this environment variable often has the correct value anyway :-( August 27: More stuff! I added more commands which are used interactively but not in scripts to the vocabulary of the new file parser, and installed the new command noml(); which will have the effect of executelines std_in: it invokes a new interface free of ML messages. In this interface you will not get any ML messages; you will also not have a prompt (I may fix this). It may have curious gaps in its vocabulary ( it will tell you if it does not recognize a command). Lines must end with a semicolon to be noticed. quit(); (or quit;) will exit this interface. The argument () for commands with no parameters is optional (but the semicolon is not). The interface will accept multiple commands on one line or arguments on multiple lines; like ML, it does not allow a string to extend over more than one line. It ignores comments, and handles nested comments correctly. I don't know whether it is safe to run scripts in the noml() interface. August 27: New version posted. The "script" command no longer runs ML use files; it parses the files itself. It can handle every prover command that is in the scripts currently on the web page; if you find a command that it won't handle, I can easily install it (the error message will tell you what command it can't read). The new command bequiet(); will suppress the output from a script; speakup(); will reverse the effects of bequiet(); (you will need to use it, or you won't see any of the usual output from the prover!) There is a further change in the display of terms with prefix operators; the last change was not good. There are now spaces after prefix operators (but not before them) so that nested prefix operators don't merge. Scripts now need to end with the command quit(); (or quit;) so that they will exit correctly. August 20: Revision of logical preamble, further commenting and fine-tuning of script files. This new version should be used if the new version of structural.mk2 is used. August 19: There is an improvement in the backup behaviour of the script command. This version is still being treated as a "draft" version until the "invisible type labels" feature has been tested in practice (it is in sourcedraft.txt). The overhaul of posted script files has been completed, except for substantial files expected from students. August 14: Some entries in this file were lost due to the destruction of the web page. A new "draft" version is available (sourcedraft.txt) which supports assignment of default types to free variables: the command dti "x" "Real", for example, will allow the prover to read :?x as Real:?x, and display Real:?x as :?x. This information is a feature of desktop but not of saved theories. The August 14th version also eliminates the extra space in front of prefix operators and improves the backup behaviour of the gettheory and backuptheory commands in relation to "remembering" environments. July 15th: this upgrade introduced the setpause() and setnopause() commands, which turn on and off a switch which makes the prover pause unti a key is hit when it issues an error message. Useful when running scripts. (entry reconstructed after destruction of web page) June 12: a technical fix, harmonizing the type raising operation on infixes (initial colon) (which no one is using at the moment!) with the "strongly Cantorian sets as types" features. The prover was mistakenly treating type-raised versions of "scin" or "scout" infixes as likewise being "scin" or "scout", which is not the case! June 11: the script command now automatically saves to a theory file of the same name as the script when it is done. The 1|-|n hypothesis tactic now introduces new objects ?x_m @ ?n when inside a variable binding context; this may cause some old files not to run correctly. The theorm ALT_QUANT_IMP in my quantifiers.mk2 script would not run under the old version, for example. I don't think this will happen a lot! I have run all the major scripts under the new version of the prover. The new version of 1|-|n might fail (just as conventional theorems which introduce "new" objects in variable binding contexts can sometimes fail) due to failures of stratification with the new variable. A new hypothesis tactic, (2|-|n)@parameter (the parameter is required) is introduced; this will behave the same as 1|-|n in the forward direction (why bother!), but in the reverse direction it will use the parameter as the "new" object. This gives full flexibility for this kind of command. March 12: Problems with higher-order matching are avoided in the new posted version by restricting higher order matching to one variable. A term ?P@?n matches any expression in ?n (in which ?n has the correct type) in the context where ?n is the highest numbered variable free. New variables introduced by theorems will depend on the variable ?n (but not any lower numbered variables) in such a context; this may cause stratification problems, in which case using parameterized inverse theorems (in Parvin's style) rather than theorems which introduce new variables becomes a good idea. Please tell me if any problems come up which look as if they might be related to this kind of matching. Last version on March 12 posted at 3:57 Boise time; another version was posted earlier. March 11: Defined functions and infixes can now have formal function parameters. For example, the definition of forall could be changed to defineconstant "forall@[?P@?1]" "[?P@?1]=[true]" This suggests that logicdefs ought to be rewritten to support this definition (which has definite advantages) but I have not yet done so (it will take work!) March 9: New version of logicdefs2.mk2 proof script fixes bugs noted earlier. New version of prover fixes another problem with stratification. March 6: New posted version fixes serious bug in EVAL and BIND built- in theorems, which were not doing "alpha-conversion" correctly for function arguments. March 5: The situation with removedefdeps() remains the same; all versions now do not automatically remove definition dependencies, and the user command reallyremovedefdeps() will do this if wanted. A bug in a cache which could cause the prover to exhibit an ML error with theorems called by form has been fixed. I am working on fixing a real logical problem in the relation between "higher-order matching" and stratification; I'll discuss this at the meeting March 6-9. Notice that there are a lot of new scripts; sorry about the low level of documentation on these, and I will try to do better! Jan 24th: The internal function removedefdeps() is disabled in the draft version now supplied (the Postscript and regular source files are not replaced). The problem is that the function (which is designed to remove unneeded dependencies on definitions) is extremely slow! If you want to run the function as a user to remove unnecessary deps before proving a theorem, the command is now reallyremovedefdeps() Definitely use the draft version with this date to run the logicdefs2.mk2 script; the official version takes a _very_ long time to record the proof of the GCLEAN tactic, for example. The logicdefs2.mk2 script should now run correctly. I will be updating it to Parvin's full file as soon as possible. There is an intermittent ML bug in the execution of theorems called by form ("x = y" theorems). I don't understand it yet. This is not a feature that is used very much, so I'm not too worried about it (the bug does not allow false theorems to be proved). Dec. 5: Smart scripts! The script command now keeps track of what scripts have already been run and does not allow one to repeatedly run the same script. This means that scripts can include one another safely without risks of long lists of declaration errors (a tree structure of dependencies among scripts is OK, not just a linear structure). The clear command also clears the list of scripts. Script information is not saved in theory files. Dec. 3: The documentation now at least mentions the new features (types as strongly Cantorian sets), though I think it is rather cryptic without some discussion of the math. Something about the math can be found in the last chapter of my naive set theory text, but it is not really right for Mark2 users. A new prover version to be posted later today corrects some technical problems with these features. I will work on putting together a demo about stratification and types as strongly Cantorian sets. The command "demoline" used in my introductory demo is now built into the prover. The new documentation mentions the versiondate() and script commands (but not demoline). Dec. 2: Technical improvement to type machinery not likely to mean much to the reader yet + correction to behaviour of the remainder function on division by zero + introduced a new function "script": the ML command script "file-name" translates to use "file-name.mk2"; the intention is that .mk2 will be the extension for Mark2 prover script files. November 21: The official version now has the full machinery for types as strongly Cantorian sets, with automatic relaxation of stratification restrictions. This feature needs to be documented in the manual; I will note in this file when the documentation is provided. A minor note (but useful): the versiondate() command will from now on report the date of the version of the prover being used. November 20: A draft version implementing "strongly Cantorian sets as data types" has been put in file sourcedraft.txt. A list of new commands needs to be described before this means very much to the reader :-) September 30: The documentation has been updated to reflect recent changes and upgrades. September 27: The update of September 26 is now available in all files with the following additions: "forget" and theorem export now work with modules: forget will delete an entire module if any component contains a reference to the object being forgotten. Theorem export exports modules, but does not export module structure; exported modules are completely unpacked. Commands moddisplay and showallmodules work like thmdisplay and showalltheorems except that they display theorems inside modules. Variants pushtheorem2 and poptheorem2 of the module construction/deconstruction commands do not post automatic comments. This is handy if one wants to take a component out in order to edit it. The command showallaxioms() is now available; it displays all axioms and definitions. The command initializecounter() can be used to set the new variable counter to zero; this would make it possible to use new variables in demos, for example. (This command was already present). The steps() command has been changed: one must now type "q" (not just any key but Enter) to break out, and it will stop automatically when the term stabilizes. This makes it possible to step through demos safely with just Enter. September 26: FURTHER UPGRADES: This announces a "draft version": "forget" is now available: "forget " will delete all theorems that depend on the parameter. It is very slow; to keep you from being bored, it announces the names of the theorems it is deleting. Your theory will be backed up onto the desktop so that you can recover if you don't like the results. It will not delete references to "forgotten" theorems from the list of functional program bindings or from the definitions list (this will be cleaned up later). By the way, the clear() command now backs up the current theory onto the desktop. The fact that this didn't happen before caused me all kinds of annoyance; I don't know why I didn't do this sooner. A "module system" is now available. The command "pushtheorem " will hide theorem 1 inside of theorem 2, in effect; theorem 1 will only be visible while theorem 2 is executing. Thmdisplay will give the name of theorem 1 (in a list labelled "module components"), but no other information about it; showdec will reveal an automatically generated comment that theorem 1 has been pushed into the module theorem 2. The command "poptheorem will get theorem 1 back onto the main theorem list. The idea is that subcommands of tactics can be hidden inside the tactics and not clutter up the theorem list. Notice that the names of "hidden" theorems are _not_ freed for other uses! Modules should be nestable, though I have not tested this. Modules will apparently save to and load from theory files correctly. The theorem export commands and the new "forget" command will NOT behave correctly in the presence of modules; this is why this is a draft version! The module system does _not_ test whether a use of pushtheorem is wise; don't push theorem 2 into theorem 1 if theorem 2 has any other "client" than theorem 1! Also, if theorem 3 is hidden inside theorem 2, which is in turn hidden inside theorem 1, theorem 1 will not be able to see theorem 3! There is currently no way to view a theorem in a module except to bring it out of the module using "poptheorem" and look at it. The documentation has not yet been upgraded to reflect recent changes. Minor comment: the annoying error message in the proof of the structural tactic "$" in Parvin's file is now eliminated. September 24: USEFUL UPGRADE: the system now allows comments to be stored with declarations. Use the command newcomment "" ""; to write new comments (and erase any previous comments); use the command appendcomment "" ""; to append new material to existing comments. Comments are stored in theory files. Comments are displayed by showdec and thmdisplay. Carriage returns and tabs can be included in comments for readability (\n and \t represent return and tab respectively in ML strings). September 21: Michael Parvin's abbreviations for commonly used command names are installed. Views are now saved in theory files. Theories are now "impredicative" by default (this is a technicality; it means that things now behave sensibly where before they did not!) September 12: The correction announced in the August 2 note has now been made in all files. August 2: This correction has only been made in the file sourcedraft.txt; I will make it in the other versions as soon as I am back in Boise on Aug. 7. The prover does not handle context-based rewriting inside lambda-terms correctly in the tactic interpreter, because the tactic interpreter does not record the environment of automatically introduced hypotheses correctly. Get file sourcedraft.txt until I update the other files. When doing variable binding with multiple variables, you need to be very careful to preserve stratification; using strongly cantorian types can help. A planned upgrade will supply the information that the input or output of certain operators is s.c. to the stratification checker; this will make stratification much less obtrusive except where it really matters. May 6: The original implementation of retractions onto strongly Cantorian types was unsound; this should be fixed now. The implementatation of "predicativity" and "opacity" restrictions is improved, and EVAL and BIND will now work as intended in predicative theories (the restriction is that one cannot abstract into functions). "New" variables introduced by theorem applications inside "lambda-terms" now are introduced as depending on appropriate bound variables. I have been doing extensive reasoning with the variable binding machinery; this has uncovered bugs in stratification checking which needed to be fixed (and apparently have been fixed). Apr. 17: commands like matchruleintro, targetruleintro now are level-sensitive, so will work correctly inside variable binding contexts. Overly strict enforcement of stratification which forbade perfectly nice expressions like [?1]@[?1] corrected (weak stratification instead of strong stratification is now enforced). Restrictions on opaque infixes were also too strong. Error message reference added to documentation. These corrections are the result of extensive work being done for the first time using the bound variable features. They seem to help! Also, corrected bug in application of hypotheses: they were being compared literally to target terms without appropriate changes of bound variables and hypotheses. Apr. 9: The theorems EVAL and BIND do not check "predicativity", and so should not be used in a predicative theory. The next version will enforce this restriction, but it has not yet been posted (posted Apr. 17) Apr. 4: Adds new built-in "theorems" EVAL and BIND which implement abstraction and reduction for variable-binding contexts directly. Adds "type labels" implemented as retractions onto "strongly Cantorian sets" with the natural privileges relative to stratification. Relaxes stratification restrictions on embedded theorem names in variable binding contexts. Technical improvements in matching (limited higher-order matching) make it possible to prove the built-in theorem VALUE directly. VALUE is still supported. Nov. 28: Fixes a bug in the internal "textmatch" function which made it difficult for functions in the "upto" family to locate subexpressions with case structure. Removes a feature which was making backups of theorem environments very slow under some circumstances (and so making operations like "start", "startover", "workback" rather slow). Fixes a problem with the pretty-printer in relation to long terms built with left-associative infixes. Introduces a new built in theorem ORDERED (described in the documentation) which enables sorting of terms linked by commutative infixes. Improved the format of the "lookhyps" command. I have used the hypothesis machinery to build a complete tautology checker, whose behaviour seems to be correct. This and other theory files are available on request. Nov. 9: Fixes a serious bug in the behaviour of the 1|-|n theorems which implement one aspect of the hypothesis engine. The hypothesis system seems to make proofs much more straightforward. Also fixes a minor irregularity in the precedence system; type-raised operators now get the same precedence as their parent operator, rather than default precedence. Oct. 23: New built-in theorems INPUT and OUTPUT added; these enable display of subterms of interest during processes and the interactive introduction of theorems/tactics during processes. There are some brief remarks in the documentation on these. Commands for display of hypotheses were added and other technical modifications related to the hypothesis function were made. Oct. 19: The official source now has the hypothesis machinery. There are some other minor modifications; the annoying behaviour of theorem export with respect to numerals may have been fixed. Oct. 18: The documentation describes new facilities for automatic handling of reasoning under locally applicable hypotheses in case expressions. Examples are needed, though. The draft version of the source implements the new hypothesis facility, but the official version does not as yet. Oct. 12: Extended the section on programming style with examples of abstraction and reduction algorithms and their applications. New code fixing an error in the behavior of the infixes *> and <* in the new implementation of the debugger (they worked correctly for "execute" but not for "steps"). Oct. 11: The new documentation now includes a new section on Logic and Programming Style, which might be useful in understanding the way in which the prover is intended to be used, and the motivation for some of the design decisions. This section is by no means finished! Note that the unpublished paper an excerpt of which appears in the Logical Style subsection is available on this site. Oct. 5: New code has been posted. It corrects the bug in the redefinition facility (which causes the prover to go into infinite loops in situations which have nothing obvious to do with redefinition!) and incorporates a new version of the code for the tactic interpreters "execute" and "onestep". The old code is still present as a very large comment in case of difficulties. The new code for the tactic interpreters has a sensible structure; for example, it is now possible to introduce a new control structure by modifying one function and have it work correctly in both execute and onestep without having to modify either of those functions directly, and it should be posible to write functions implementing new execution orders for the tactic interpreter without much difficulty. Up until now the two tactic interpreters have been maintained in parallel (and the behaviour of each rule infix has been maintained in parallel as well, in each function!). Performance of the new code seems to be comparable to that of the old. (* up to Oct. 3, I was adding comments at the end of this file; from Oct. 5 on, I will add new comments at the beginning. The comments up to Oct. 3 follow in their original order *) May 20 -- a bug in the user defined precedence corrected (under some circumstances (as in the "interaxiom" command) terms were being read from the session using the correct parser then displayed using the default precedence)). May 22 -- the draft version has better program-generated variables and the ability to search for theorems by form rather than by name. Look in the source code for the commands "showmatchthm", "matchruleintro", and "targetruleintro". May 23 -- the draft version now supports impredicative abstraction via the RAISE built-in theorem; this is a mostly undocumented feature of the higher-order logic of the prover. May 24 -- the features mentioned in the May 22-23 notes are now official; in addition, the location of the current subterm is now marked by brackets in term displays. June 7 -- the internal programming language has been enhanced with some new features, as yet not documented. The theorem export procedure is now more likely to succeed. A number of bugs in the previous version were found and fixed. June 21 -- a number of revisions have taken place. Some have not been extensively tested. The theorem export system is improved. There are now commands for restructuring the definitions in a theory. Saved proof environments are stored in the master theorem list; the reason for doing this was so that global dependency fixes would affect them as they should (fixing a bug), but this has the side effect that proof environments in the workspace are now saved with the theory! June 28 -- Fixed a bug in the parsing of expressions with prefix operators which right-associate. The definition restructuring commands have been tested. June 29 -- In the "draft version", find a recommented and reorganized version of the source code. It also has some new features: the assign command is more general and the base of numeration is now a feature of theories. July 6 (date on file may be misleading) -- moved recommented version to official status. Corrected a bug in the basic matching procedure (a missing pair of parentheses in a boolean expression; I don't know how it didn't get noticed for so long!). The draft version now supports bound variables (it uses deBruijn levels -- not indices! -- the constant function constructor (brackets) of previous versions is now the variable binding environment, with ?n the variable bound in the nth level of brackets for each positive n. The draft version with bound variables is _certain_ to have various bugs in it! Sept. 8: fixed a bug which could cause environments from a previous theory to be saved when entering a new theory. All loops which earlier needed Control-C to break out now can be broken with any non-return character. The default "load", "storeall", and "safesave" commands now use the "walk" interface save file format; the old commands are present as "oldload", etc. The official version now has the deBruijn level implementation of variable binding in it; it is likely to have bugs in this connection! Sept. 21 -- a new version of the source with some additional commands was posted yesterday. As well, the documentation has been extended and collected into one 65-page document which covers every aspect of the prover at least in general terms. One odd thing about it is that it contains not one but two command reference lists, organized along somewhat different lines. also Sept. 21, a warning (I'll put these in, too): the delay operator which is supposed to help functional programming work does not work exactly as advertised. As a result, attempts at recursive functional programming (which no one is likely to try in a great hurry!) are not likely to work until I fix this bug. This does not affect programming entirely with explicit tactics at all. Sept. 22 -- the bug announced on Sept. 21 was not what I thought it was; it arose not from a problem with functional programming but from the failure of the program to correctly identify the built-in arithmetic operation of equality :-( This caused automated evaluation of case expressions to fail in a way which looks like a bug in the delay operator but isn't! I fixed the bug and will post the changed version of the source code today. This will also incorporate a change in the default prefix for constants declared with "declareunary" from "0" to "defaultprefix", a new built-in constant, which avoids problems with theorem export where numerals are involved. Sept. 22 (later) -- The bug has been fixed. Source code and documentation have been updated. Tests seem to indicate that recursive functional programming _does_ work correctly. Also some new movement commands, allowing movement to places where given theorems can be applied, have been implemented; see either command reference list in the documentation for a description. The "load" command temporarily includes commands designed to retroactively fix the default "default left argument" in old theories. These commands will cause mysterious error messages about an illegal or repeated declaration of "defaultprefix"; please ignore, and this will disappear in due course. Sept. 29: A technical change in the matching procedure (to enforce confluence) is partially implemented. A new feature, the addition of a prefix implementing lazy execution of the tactic language, has been added and is documented. The prover will issue another mysterious message since the load command automatically redeclares the laziness infix. Once all of my old theories have the declaration inserted, I'll remove these extra declarations from subsequent versions. Also, a quite serious pair of bugs in the handling of theorem application inside variable binding contexts has been fixed; parameters of embedded theorems could not previously include any bound variables, and theorems were not applied correctly to subterms of nonzero de Bruijn level (that is, subterms with bound variables free in them). If anyone is trying to use the prover, tell me if any other bugs crop up in connection with variable binding. Do note that free variables always represent top-level objects; a theorem like [?a] :+ [?b] = [?a+?b] applies only to constant functions (?a and ?b cannot be replaced with terms with nontrivial occurrences of the variable ?1 bound in this context); this is a feature (though an annoying one) not a bug. Oct. 3: Warning: there is a serious, recently introduced bug in the redefinition facility which has the side-effect of making the system "hang up" in quite unexpected situations. I have repaired it and will post the new code either today or on the 6th.