[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 8b16d1d 04/13: Remove LEGO support
|
From: |
ELPA Syncer |
|
Subject: |
[nongnu] elpa/proof-general 8b16d1d 04/13: Remove LEGO support |
|
Date: |
Thu, 25 Nov 2021 10:57:57 -0500 (EST) |
branch: elpa/proof-general
commit 8b16d1d48b54a853d8cc3f872ab009afd3386b8f
Author: Stefan Monnier <monnier@iro.umontreal.ca>
Commit: Stefan Monnier <monnier@iro.umontreal.ca>
Remove LEGO support
---
BUGS | 10 +-
INSTALL | 2 +-
Makefile | 8 +-
Makefile.devel | 2 +-
README.md | 7 +-
doc/PG-adapting.texi | 16 +-
doc/ProofGeneral.texi | 163 +++------------
etc/ProofGeneral.spec | 2 +-
etc/README | 1 -
etc/lego/GoalGoal.l | 13 --
etc/lego/error-eg.l | 16 --
etc/lego/lego-site.el | 37 ----
etc/lego/long-line-backslash.l | 22 ---
etc/lego/multiple/A.l | 1 -
etc/lego/multiple/B.l | 4 -
etc/lego/multiple/C.l | 1 -
etc/lego/multiple/D.l | 1 -
etc/lego/multiple/README | 33 ----
etc/lego/pbp.l | 30 ---
etc/lego/unsaved-goals.l | 54 -----
generic/proof-config.el | 25 ++-
generic/proof-script.el | 2 +-
generic/proof-shell.el | 4 +-
generic/proof-site.el | 4 +-
lego/BUGS | 53 -----
lego/README | 37 ----
lego/example.l | 15 --
lego/example2.l | 1 -
lego/lego-syntax.el | 131 ------------
lego/lego.el | 439 -----------------------------------------
lego/legotags | 91 ---------
lego/root2.l | 368 ----------------------------------
proof-general.el | 2 +-
33 files changed, 57 insertions(+), 1538 deletions(-)
diff --git a/BUGS b/BUGS
index 92aef30..61e7494 100644
--- a/BUGS
+++ b/BUGS
@@ -100,12 +100,4 @@ See manual for further description of this.
** coqtags doesn't find all declarations.
It cannot handle lists e.g., with "Parameter x,y:nat" it only tags x
-but not y. [The same problem exists for legotags] Workaround: don't
-rely too much on the etags mechanism.
-
-
-* LEGO Proof General Bugs
-
-See lego/BUGS
-
-
+but not y. Workaround: don't rely too much on the etags mechanism.
diff --git a/INSTALL b/INSTALL
index 3b496bd..6b08e3b 100644
--- a/INSTALL
+++ b/INSTALL
@@ -148,7 +148,7 @@ Removing support for unwanted provers
You cannot run more than one instance of Proof General at a time in
the same Emacs process: e.g. if you're using Coq, you won't be able to
-run LEGO scripts.
+run EasyCrypt scripts.
If there are some assistants supported that you never want to use, you
can remove them from the variable `proof-assistants' to prevent Proof
diff --git a/Makefile b/Makefile
index 9a6edc0..912d246 100644
--- a/Makefile
+++ b/Makefile
@@ -35,7 +35,7 @@ PREFIX=$(DESTDIR)/usr
DEST_PREFIX=$(DESTDIR)/usr
# subdirectories for provers: to be compiled and installed
-PROVERS=acl2 coq easycrypt hol-light isar lego pghaskell pgocaml pgshell phox
+PROVERS=acl2 coq easycrypt hol-light isar pghaskell pgocaml pgshell phox
# generic lisp code: to be compiled and installed
OTHER_ELISP=generic lib
@@ -58,17 +58,17 @@ ELISP_EXTRAS=
EXTRA_DIRS = images
DOC_FILES=AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER
doc/*.pdf
-DOC_EXAMPLES=acl2/*.acl2 isar/*.thy lclam/*.lcm lego/*.l pgshell/*.pgsh
phox/*.phx plastic/*.lf
+DOC_EXAMPLES=acl2/*.acl2 isar/*.thy lclam/*.lcm pgshell/*.pgsh phox/*.phx
plastic/*.lf
DOC_SUBDIRS=${DOC_EXAMPLES} */README* */CHANGES */BUGS
BATCHEMACS=${EMACS} --batch --no-site-file -q
# Scripts to edit paths to shells
BASH_SCRIPTS = isar/interface
-PERL_SCRIPTS = lego/legotags coq/coqtags isar/isartags
+PERL_SCRIPTS = coq/coqtags isar/isartags
# Scripts to install to bin directory
-BIN_SCRIPTS = lego/legotags coq/coqtags isar/isartags
+BIN_SCRIPTS = coq/coqtags isar/isartags
# Setting load path might be better in Elisp, but seems tricky to do
# only during compilation. Another idea: put a function in proof-site
diff --git a/Makefile.devel b/Makefile.devel
index 8705af3..4f4004f 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -147,7 +147,7 @@ TAR=tar
# Files not to include the distribution area or tarball
UNFINISHED_ELISP=
-ETC_FILES=etc/lego etc/coq etc/demoisa etc/isa etc/isar etc/lego etc/patches
etc/*.txt
+ETC_FILES=etc/coq etc/demoisa etc/isa etc/isar etc/patches etc/*.txt
NONDISTFILES=.gitignore */.gitignore Makefile.devel etc/trac etc/testsuite
$(UNFINISHED_ELISP) $(ETC_FILES)
DOCDISTFILES=ProofGeneral.info PG-adapting.info
diff --git a/README.md b/README.md
index 230caee..a4a4422 100644
--- a/README.md
+++ b/README.md
@@ -138,11 +138,12 @@ Proof General used to support other proof assistants, but
those
instances are no longer maintained nor available in the MELPA package:
* Legacy support of
- [Isabelle](https://www.cl.cam.ac.uk/research/hvg/Isabelle/) and
- [LEGO](http://www.dcs.ed.ac.uk/home/lego)
+ [Isabelle](https://www.cl.cam.ac.uk/research/hvg/Isabelle/)
+
* Experimental support of: ACL2, Hol-Light, Lambda-Clam, Shell
* Obsolete instances: Demoisa, Lambda-Clam, Plastic
-* Removed instances: Twelf, CCC, HOL98
+* Removed instances: Twelf, CCC, HOL98,
+ [LEGO](http://www.dcs.ed.ac.uk/home/lego)
A few example proofs are included in each prover subdirectory.
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 4e0ec65..3f1374e 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -139,7 +139,7 @@ of @b{Proof General}, a generic Emacs interface for proof
assistants.
Proof General @value{version} has been tested with GNU Emacs
@value{emacsversion}. It is supplied ready customized for the proof
-assistants Coq, Lego, Isabelle, and HOL.
+assistants Coq, EasyCrypt, Isabelle, and HOL.
This manual contains information for customizing to new proof
assistants; see the user manual for details about how to use
@@ -1634,7 +1634,7 @@ prompts than expected, things will break! Extending the
variable
stripped of carriage returns before being sent.
Example uses:
-@var{lego} uses this hook for setting the pretty printer width if
+Lego used this hook for setting the pretty printer width if
the window width has changed;
Plastic uses it to remove literate-style markup from @samp{string}.
@@ -2012,9 +2012,7 @@ quote characters must be escaped. The setting
'(("@var{\\\\}" . "@var{\\\\}")
("\"" . "\\\""))
@end lisp
-achieves this. This does not apply to @var{lego}, which does not
-need backslash escapes and does not allow filenames with
-quote characters.
+achieves this.
This setting is used inside the function @samp{@code{proof-format-filename}}.
@end defvar
@@ -3319,7 +3317,7 @@ only select the proof assistants you (or your site) may
need.
You can select which proof assistants you want by setting this
variable before @samp{proof-site.el} is loaded, or by setting
the environment variable @samp{PROOFGENERAL_ASSISTANTS} to the
-symbols you want, for example "lego isa". Or you can
+symbols you want, for example "coq easycrypt". Or you can
edit the file @samp{proof-site.el} itself.
Note: to change proof assistant, you must start a new Emacs session.
@@ -3938,7 +3936,7 @@ Choice of syntax tree encoding for terms.
If nil, prover is expected to make no optimisations.
If non-nil, the pretty printer of the prover only reports local changes.
-For @var{lego} 1.3.1 use nil, for Coq 6.2, use t.
+For Coq 6.2, use t.
@end defvar
@@ -4016,7 +4014,7 @@ It is up to the proof assistant how much context is
cleared: for
example, theories already loaded may be "cached" in some way,
so that loading them the next time round only performs a re-linking
operation, not full re-processing. (One way of caching is via
-object files, used by Lego and Coq).
+object files, used by Coq).
@end deffn
@c
@@ -4488,7 +4486,7 @@ This is a note by David Aspinall about proof by pointing
and similar
features.
Proof General already supports proof by pointing, and experimental
-support is provided in LEGO. We would like to extend this support to
+support was provided in LEGO. We would like to extend this support to
other proof assistants. Unfortunately, proof by pointing requires
rather heavy support from the proof assistant. There are two aspects to
the support:
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 143ad20..48468b1 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -158,7 +158,6 @@ assistants Coq, EasyCrypt, and PhoX.
* Graphical Proof-Tree Visualization::
* Customizing Proof General::
* Hints and Tips::
-* LEGO Proof General::
* Coq Proof General::
* Isabelle Proof General::
* HOL Light Proof General::
@@ -209,7 +208,7 @@ other documentation, system downloads, etc.
@cindex news
The old code for the support of the following systems have been
-removed: Twelf, CCC, HOL98.
+removed: Twelf, CCC, Lego, HOL98.
@node News for Version 4.4
@unnumberedsec News for Version 4.4
@@ -310,7 +309,6 @@ webpage}. Help us to help you organize your proofs!
@node Credits
@unnumberedsec Credits
-@cindex @code{lego-mode}
@cindex maintenance
The original developers of the basis of Proof General were:
@@ -516,7 +514,6 @@ script file for your proof assistant, for example:
@multitable @columnfractions .35 .3 .35
@item @b{Prover} @tab @b{Extensions} @tab @b{Mode}
-@item LEGO @tab @file{.l} @tab @code{lego-mode}
@item Coq @tab @file{.v} @tab @code{coq-mode}
@item Isabelle @tab @file{.thy} @tab @code{isar-mode}
@item Phox @tab @file{.phx} @tab @code{phox-mode}
@@ -529,8 +526,8 @@ script file for your proof assistant, for example:
@end multitable
(the exact list of Proof Assistants supported may vary according to the
version of Proof General and its local configuration). You can also
-invoke the mode command directly, e.g., type @kbd{M-x lego-mode}, to
-turn a buffer into a lego script buffer.
+invoke the mode command directly, e.g., type @kbd{M-x coq-mode}, to
+turn a buffer into a Coq script buffer.
You'll find commands to process the proof script are available from the
toolbar, menus, and keyboard. Type @kbd{C-h m} to get a list of the
@@ -665,9 +662,6 @@ proof assistants, including these:
@c FLAG VERSIONS HERE
@itemize @bullet
@item
-@b{LEGO Proof General} for LEGO Version 1.3.1@*
-@xref{LEGO Proof General}, for more details.
-@item
@b{Coq Proof General} for Coq Version 8.2@*
@xref{Coq Proof General}, for more details.
@item
@@ -705,7 +699,7 @@ standard instances documented in this manual are listed
above.
Note that there is some variation between the features supported by
different instances of Proof General. The main variation is proof by
-pointing, which is only supported in LEGO at the moment. For advanced
+pointing, which has been supported only in LEGO so far. For advanced
features like this, some extensions to the output routines of the proof
assistant are required, typically. If you like Proof General, @b{please
help us by asking the implementors of your favourite proof assistant to
@@ -1283,9 +1277,9 @@ file and a @code{.thy} theory file which defines its
theory.
If you have a partly processed scripting buffer and use @kbd{C-c C-s},
or you attempt to use script processing in a new buffer, Proof General
will ask you if you want to retract what has been proved so far,
-@code{Scripting incomplete in buffer myproof.l, retract?}
+@code{Scripting incomplete in buffer myproof.v, retract?}
or if you want to process the remainder of the active buffer,
-@code{Completely process buffer myproof.l instead?}
+@code{Completely process buffer myproof.v instead?}
before you can start scripting in a new buffer. If you refuse to do
either, Proof General will give an error message:
@code{Cannot have more than one active scripting buffer!}.
@@ -1407,7 +1401,7 @@ Set point to end of command at point.
@vindex proof-terminal-string
The variable @code{proof-terminal-string} is a prover-specific string
-to terminate proof commands. LEGO and Isabelle use a semicolon,
+to terminate proof commands. LEGO and Isabelle used a semicolon,
@samp{;}. Coq employs a full-stop @samp{.}.
@c TEXI DOCSTRING MAGIC: proof-goto-end-of-locked
@@ -1483,7 +1477,7 @@ design, by allowing successive assertion commands without
complaining.}
The last command, @code{proof-electric-terminator-toggle}, is triggered
using the character which terminates proof commands for your proof
-assistant's script language. For LEGO and Isabelle, use @kbd{C-c ;},
+assistant's script language. LEGO and Isabelle used @kbd{C-c ;},
for Coq, use @kbd{C-c .}. This not really a script processing
command. Instead, if enabled, it causes subsequent key presses of
@kbd{;} or @kbd{.} to automatically activate
@@ -1799,7 +1793,7 @@ It is up to the proof assistant how much context is
cleared: for
example, theories already loaded may be "cached" in some way,
so that loading them the next time round only performs a re-linking
operation, not full re-processing. (One way of caching is via
-object files, used by Lego and Coq).
+object files, used by Coq).
@end deffn
@@ -2121,8 +2115,8 @@ Basic modularity in large proof developments can be
achieved by
splitting proof scripts across various files. Let's assume that you are
in the middle of a proof development. You are working on a soundness
proof of Hoare Logic in a file called@footnote{The suffix may depend of
-the specific proof assistant you are using e.g, LEGO's proof script
-files have to end with @file{.l}.} @file{HSound.l}. It
+the specific proof assistant you are using e.g, Coq's proof script
+files have to end with @file{.v}.} @file{HSound.v}. It
depends on a number of other files which develop underlying
concepts e.g. syntax and semantics of expressions, assertions,
imperative programs. You notice that the current lemma is too difficult
@@ -2131,11 +2125,11 @@ about determinism of the programming language. Or
perhaps a previous
definition is too cumbersome or even wrong.
At this stage, you would like to visit the appropriate file, say
-@file{sos.l} and retract to where changes are required. Then, using
+@file{sos.v} and retract to where changes are required. Then, using
script management, you want to develop some more basic theory in
-@file{sos.l}. Once this task has been completed (possibly involving
+@file{sos.v}. Once this task has been completed (possibly involving
retraction across even earlier files) and the new development has been
-asserted, you want to switch back to @file{HSound.l} and replay to the
+asserted, you want to switch back to @file{HSound.v} and replay to the
point you got stuck previously.
Some hours (or days) later you have completed the soundness proof and
@@ -2156,7 +2150,7 @@ or retract the current script buffer.
Proof General tries to be aware of all files that the proof assistant
has processed or is currently processing. In the best case, it relies
on the proof assistant explicitly telling it whenever it processes a new
-file which corresponds@footnote{For example, LEGO generates additional
+file which corresponds@footnote{For example, LEGO generated additional
compiled (optimised) proof script files for efficiency.} to a file
containing a proof script.
@@ -2200,16 +2194,6 @@ you are back on track.
-@c only true for LEGO!
-@c If the proof assistant is not happy with the script and
-@c complains with an error message, the buffer will still be marked as
-@c having been completely processed. Sorry. You need to visit the
-@c troublesome file, retract (which will always retract to the beginning of
-@c the file) and debug the problem e.g., by asserting all of the buffer
-@c under the supervision of Proof General, see @ref{Script processing
-@c commands}.
-
-
@node Retracting across files
@section Retracting across files
@cindex Retraction
@@ -2830,7 +2814,6 @@ and @code{etags}.
@node Syntax highlighting
@section Syntax highlighting
-@vindex lego-mode-hooks
@vindex coq-mode-hooks
@vindex isa-mode-hooks
@cindex font lock
@@ -2996,8 +2979,8 @@ through all the files with one command. Recording the
function names
and positions makes possible the @kbd{M-.} command which finds the
definition of a function by looking up which of the files it is in.
-Some instantiations of Proof General (currently LEGO and Coq) are
-supplied with external programs (@file{legotags} and @file{coqtags}) for
+Some instantiations of Proof General (currently Coq) are
+supplied with external programs (@file{coqtags}) for
making tags tables. For example, invoking @samp{coqtags *.v} produces a
file @file{TAGS} for all files @samp{*.v} in the current
directory. Invoking @samp{coqtags `find . -name \*.v`} produces a file
@@ -3042,7 +3025,7 @@ Add completions from the current tags table.
This chapter describes what you can do from inside the goals buffer,
providing support for these features exists for your proof assistant.
-As of Proof General 4.0, this support only exists for LEGO and
+As of Proof General 4.4, this support has existed only for LEGO and
proof-by-pointing functionality has been temporarily removed from the
interface. If you would like to see subterm activation support for
Proof General in another proof assistant, please petition the developers
@@ -3995,8 +3978,8 @@ and save these variables, saving them may have no
practical effect
because the default settings are mostly hard-wired into the proof
assistant code. Ones we expect may need changing appear as proof
assistant specific configurations. For example,
-@code{proof-assistant-home-page} is set in the LEGO code from the value
-of the customization setting @code{lego-www-home-page}. At present
+@code{proof-assistant-home-page} is set in the Coq code from the value
+of the customization setting @code{coq-www-home-page}. At present
there is no easy way to save changes to other configuration variables
across sessions, other than by editing the source code. (In future
versions of Proof General, we plan to make all configuration
@@ -4191,107 +4174,6 @@ mode you can expand an abbreviation by pressing
@kbd{C-x '}
@c =================================================================
@c
-@c CHAPTER: LEGO Proof General
-@c
-@node LEGO Proof General
-@chapter LEGO Proof General
-@cindex LEGO Proof General
-
-LEGO proof script mode is a mode derived from proof script mode for
-editing LEGO scripts. An important convention is that proof script
-buffers @emph{must} start with a module declaration. If the proof script
-buffer's file name is @file{fermat.l}, then it must commence with a
-declaration of the form
-
-@lisp
-Module fermat;
-@end lisp
-
-If, in the development of the module @samp{fermat}, you require material
-from other module e.g., @samp{lib_nat} and @samp{galois}, you need to
-specify this dependency as part of the module declaration:
-
-@lisp
-Module fermat Import lib_nat galois;
-@end lisp
-
-No need to worry too much about efficiency. When you retract back to a
-module declaration to add a new import item, LEGO does not actually
-retract the previously imported modules. Therefore, reasserting the
-extended module declaration really only processes the newly imported
-modules.
-
-Using the LEGO Proof General, you never ever need to use administrative
-LEGO commands such as @samp{Forget}, @samp{ForgetMark}, @samp{KillRef},
-@samp{Load}, @samp{Make}, @samp{Reload} and @samp{Undo} again
-@footnote{And please, don't even think of including those in your LEGO
-proof script!}.
-
-@menu
-* LEGO specific commands::
-* LEGO tags::
-* LEGO customizations::
-@end menu
-
-
-@node LEGO specific commands
-@section LEGO specific commands
-
-In addition to the commands provided by the generic Proof General (as
-discussed in the previous sections) the LEGO Proof General provides a
-few extensions. In proof scripts, there are some abbreviations for
-common commands:
-
-@kindex C-c C-a C-i
-@kindex C-c C-a C-I
-@kindex C-c C-a C-R
-@table @kbd
-@item C-c C-a C-i
-intros
-@item C-c C-a C-I
-Intros
-@item C-c C-a C-R
-Refine
-@end table
-
-@node LEGO tags
-@section LEGO tags
-
-You
-might want to ask your local system administrator to tag the directories
-@file{lib_Prop}, @file{lib_Type} and @file{lib_TYPE} of the LEGO
-library. See @ref{Support for tags}, for further details on tags.
-
-
-
-@node LEGO customizations
-@section LEGO customizations
-
-We refer to chapter @ref{Customizing Proof General}, for an introduction
-to the customisation mechanism. In addition to customizations at the
-generic level, for LEGO you can also customize:
-
-@defopt lego-tags
-The directory of the @var{tags} table for the @var{lego} library
-
-The default value is @code{"/usr/lib/lego/lib_Type/"}.
-@end defopt
-
-@defvar lego-www-home-page
-Lego home page URL.
-@end defvar
-
-@c We don't worry about the following for now. These are too obscure.
-@c lego-indent
-@c lego-test-all-name
-
-@c We also don't document any of the internal variables which have been
-@c set to configure the generic Proof General and which the user should
-@c not tamper with
-
-
-@c =================================================================
-@c
@c CHAPTER: Coq Proof General
@c
@node Coq Proof General
@@ -5898,7 +5780,7 @@ The distribution is available in the master branch of the
repository.
Tagged versions of the sources may be redistributed by third party
packagers in other forms.
-The sources includes the generic elisp code, and code for Coq, LEGO,
+The sources includes the generic elisp code, and code for Coq, EasyCrypt,
Isabelle, and other provers. Also included are installation
instructions (reproduced in brief below) and this documentation.
@@ -5986,7 +5868,7 @@ providing the variables in @file{proof-site.el} are
adjusted
accordingly (see @i{Proof General site configuration} in
@i{Adapting Proof General} for more details). Make sure that
the @file{generic/} and assistant-specific elisp files are kept in
-subdirectories (@file{coq/}, @file{isa/}, @file{lego/}) of
+subdirectories (@file{coq/}, @file{isa/}, @file{easycrypt/}, ...) of
@code{proof-home-directory} so that the autoload directory calculations
are correct.
@@ -6095,7 +5977,6 @@ l'INRIA Sophia Antipolis RR-3286
@c
@node History of Proof General
@unnumbered History of Proof General
-@cindex @code{lego-mode}
@cindex history
It all started some time in 1994. There was no Emacs interface for LEGO.
diff --git a/etc/ProofGeneral.spec b/etc/ProofGeneral.spec
index f1d006a..fac40af 100644
--- a/etc/ProofGeneral.spec
+++ b/etc/ProofGeneral.spec
@@ -16,7 +16,7 @@ BuildArchitectures: noarch
%description
Proof General is a generic Emacs interface for proof assistants,
suitable for use by pacifists and Emacs militants alike.
-It is supplied ready-customized for LEGO, Coq, and Isabelle.
+It is supplied ready-customized for EasyCrypt, Coq, and Isabelle.
You can adapt Proof General to other proof assistants if you know a
little bit of Emacs Lisp.
diff --git a/etc/README b/etc/README
index 1b1b0f3..43f47bf 100644
--- a/etc/README
+++ b/etc/README
@@ -15,7 +15,6 @@ ProofGeneral.menu Menu file for some Linux versions.
ProofGeneral.desktop Menu file for some Linux versions.
Install in /etc/X11/applnk/Applications/
-lego Files for testing: LEGO Proof General
isa Isabelle Proof General
isar Isar PG
demoisa Isabelle Demo PG
diff --git a/etc/lego/GoalGoal.l b/etc/lego/GoalGoal.l
deleted file mode 100644
index c4826e0..0000000
--- a/etc/lego/GoalGoal.l
+++ /dev/null
@@ -1,13 +0,0 @@
-Module GoalGoal;
-
-Goal first : {A:Prop}A->A;
-intros; Immed;
-(* no Save *)
-
-Goal second : {A:Prop}A->A;
-intros; Immed;
-Save second;
-(* asserting until here caused Proof General to swap first and second.
-This is a bug for LEGO. Thanks to Martin Hofmann for pointing this
-out. An obvious bug fix would be to make the function
-proof-lift-global Coq specific. *)
\ No newline at end of file
diff --git a/etc/lego/error-eg.l b/etc/lego/error-eg.l
deleted file mode 100644
index f6872c9..0000000
--- a/etc/lego/error-eg.l
+++ /dev/null
@@ -1,16 +0,0 @@
-Init LF;
-
-[prop:Type];
-[prf:prop->Type];
-[type:Type];
-[el:type->Type];
-
-[FA : {A:type}((el A) -> prop) -> prop];
-[LL : {A:type}{P:(el A) -> prop}
- ({x:el A}prf(P(x)))->
- (********************************)
- prf(FA A P)];
-
-[P_FA : {A:type}{P:(el A) -> prop}{C_FA:prf(FA A P) -> prop}
- ((g:{x:el A}prf(P(x)))prf(C_FA(LL A P g))) ->
- {z:prf(FA A P)}prf(C_FA(z))];
\ No newline at end of file
diff --git a/etc/lego/lego-site.el b/etc/lego/lego-site.el
deleted file mode 100644
index 1a31f35..0000000
--- a/etc/lego/lego-site.el
+++ /dev/null
@@ -1,37 +0,0 @@
-;;; lego-site.el --- Site-specific Emacs support for LEGO
-
-;; This file is part of Proof General.
-
-;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc.
-;; Portions © Copyright 2001-2017 Pierre Courtieu
-;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
-;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
-;; Portions © Copyright 2015-2017 Clément Pit-Claudel
-
-;;; Author: Thomas Kleymann <T.Kleymann@ed.ac.uk>
-;;; Maintainer: lego@dcs.ed.ac.uk
-
-;;; Commentary:
-;;
-
-;;; Code:
-
-(let ((version (getenv "PROOFGENERAL")))
- (cond ((not version) ;default
- (setq load-path
- (cons "/usr/local/share/elisp/script-management" load-path))
- (setq load-path
- (cons "/usr/local/share/elisp/script-management/lego" load-path))
- (setq auto-mode-alist (cons '("\\.l$" . lego-mode) auto-mode-alist))
- (autoload 'lego-mode "lego" "Major mode for editing Lego proof
scripts." t))
- ((string= version "ancient")
- (setq load-path (cons "/usr/local/share/elisp/lego" load-path))
- (setq auto-mode-alist (cons '("\\.l$" . lego-mode) auto-mode-alist))
- (autoload 'lego-mode "lego" "Major mode for editing Lego proof
scripts." t)
- (autoload 'lego-shell "lego" "Inferior shell invoking lego." t))
- ((string= version "latest")
- (load-file
"/usr/local/share/elisp/ProofGeneral/generic/proof-site.el"))))
-
-
-
diff --git a/etc/lego/long-line-backslash.l b/etc/lego/long-line-backslash.l
deleted file mode 100644
index c85dcdc..0000000
--- a/etc/lego/long-line-backslash.l
+++ /dev/null
@@ -1,22 +0,0 @@
-(*
-
- long-line-backslash.l
-
- Test for long lines with backslashes in them.
- Cause problem with pty communication where line length
- is limited to 256 characters sometimes (e.g. on Solaris).
-
-*)
-
-echo
"\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\
[...]
-
-(* Test subsequent commands can be processed *)
-
-[one = Prop];
-[two = Prop -> Prop];
-[three = Prop -> two];
-
-(* Test something with eager annotations *)
-
-Make "/usr/local/share/lego/lib-alpha/lib_Type/lib_logic";
-
diff --git a/etc/lego/multiple/A.l b/etc/lego/multiple/A.l
deleted file mode 100644
index d45f8db..0000000
--- a/etc/lego/multiple/A.l
+++ /dev/null
@@ -1 +0,0 @@
-Module A;
\ No newline at end of file
diff --git a/etc/lego/multiple/B.l b/etc/lego/multiple/B.l
deleted file mode 100644
index 3a8df7b..0000000
--- a/etc/lego/multiple/B.l
+++ /dev/null
@@ -1,4 +0,0 @@
-(* B.l Module with a comment *)
-Module B;
-
-[prop = Prop];
\ No newline at end of file
diff --git a/etc/lego/multiple/C.l b/etc/lego/multiple/C.l
deleted file mode 100644
index 5a3afdd..0000000
--- a/etc/lego/multiple/C.l
+++ /dev/null
@@ -1 +0,0 @@
-Module C Import A B;
\ No newline at end of file
diff --git a/etc/lego/multiple/D.l b/etc/lego/multiple/D.l
deleted file mode 100644
index b794253..0000000
--- a/etc/lego/multiple/D.l
+++ /dev/null
@@ -1 +0,0 @@
-Module D;
\ No newline at end of file
diff --git a/etc/lego/multiple/README b/etc/lego/multiple/README
deleted file mode 100644
index 11f2152..0000000
--- a/etc/lego/multiple/README
+++ /dev/null
@@ -1,33 +0,0 @@
-Handling of Multiple Files
-==========================
-
-[C depends on A and B]
-
-Notation: A means that buffer A.l is unlocked
- A+ means that buffer A.l is partly locked
- A* means that buffer A.l is locked
- ? means that behaviour might be different for proof systems
- with non-linear contexts
-
-
-Test Protocol
--------------
-
- 1) visit A.l EFFECTS A
- 2) visit C.l EFFECTS A C
- 3) assert C EFFECTS A* C*
- 4) visit B.l EFFECTS A* B* C*
- 5) visit D.l EFFECTS A* B* C* D
- 6) retract to middle of B EFFECTS A* B C D
- 7) assert first command of B EFFECTS A* B+ C D
- 8) assert C EFFECTS A* B+ C D [error message]
- 9) assert B EFFECTS A* B* C D
-10) assert D EFFECTS A* B* C D*
-11) retract B EFFECTS A* B C D?
-12) assert C EFFECTS A* B* C* D?
-13) retract B EFFECTS A* B C D?
-14) assert B EFFECTS A* B* C D?
-15) assert C EFFECTS A* B* C* D?
-16) retract to middle of B EFFECTS A* B+ C D?
-14) M-x proof-shell-restart EFFECTS A B C D
-
diff --git a/etc/lego/pbp.l b/etc/lego/pbp.l
deleted file mode 100644
index 66a6df7..0000000
--- a/etc/lego/pbp.l
+++ /dev/null
@@ -1,30 +0,0 @@
-(* How to prove a sample theorem by PBP. *)
-
-(* All using middle-clicks.
-
- 1. Click on -> (Pbp 0 3 1: Intros A B)
- 2. Click on left (A/\B) (Pbp 1 2 1: Intros H; Try Refine H)
- 3. Click on A (Pbp 4 2 1: Intros H1; Try Refine H1)
- 4. Click on B (Pbp 5 2 1: Intros H2; Try Refine H2)
- 5. Click on A in A/\B (Pbp 6 2 1: Refine pair; Try Assumption)
- 6. Click on final B (Pbp 10: Try Assumption)
- OR:
- Click on assumption B (PbpHyp H2: Try Refine H2)
- QED!!
-*)
-
-Module pbp Import lib_logic;
-
-Goal {A,B:Prop}(A /\ B) -> (B /\ A);
-Intros A B;
-Intros H; Try Refine H;
-Intros H1; Try Refine H1;
-Intros H2; Try Refine H2;
-Refine pair; Try Assumption;
-Try Assumption;
-Save and_comms;
-
-
-
-
-
diff --git a/etc/lego/unsaved-goals.l b/etc/lego/unsaved-goals.l
deleted file mode 100644
index dd9c964..0000000
--- a/etc/lego/unsaved-goals.l
+++ /dev/null
@@ -1,54 +0,0 @@
-(*
- Some test cases for closing off unsaved goals,
- and the setting proof-completed-proof-behaviour.
-
- David Aspinall, November 1999.
-
- Things work fairly well in lego with
-
- proof-completed-proof-behaviour='closeany
-
- In that case, undoing/redoing later declarations
- (E and F) following the completed proof works okay, and
- in the absence of declarations, things work fine.
-
- Declarations in LEGO are global, and forgetting a
- declaration when a proof is still open (even if complete)
- aborts the proof! So a proper handling would need to
- trigger a *further* retraction when the "Forget D" is
- issued undoing the definition of D. Never mind.
-
- With proof-completed-proof-behaviour='closegoal or 'extend,
- undoing the first goal doesn't forget the declarations.
-
- This file even causes internal errors in LEGO!
-
- Warning: forgetting a finished proof
-
- LEGO detects unexpected exception named "InfixInternal"
-
- Test with undoing and redoing, and various settings
- for proof-completed-proof-behaviour
-*)
-
-
-
-Module unsaved Import lib_logic;
-
-Goal {A,B:Prop}(and A B) -> (and B A);
-intros;
-Refine H;
-intros;
-andI;
-Immed;
-[D = Type];
-[E = Type];
-[F = Type];
-
-Goal {A,B:Prop}(and A B) -> (and B A);
-intros;
-Refine H;
-intros;
-andI;
-Immed;
-
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 951aade..3106d4e 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -3,7 +3,7 @@
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
@@ -1581,9 +1581,7 @@ they appear inside ML strings and the backslash character
and
quote characters must be escaped. The setting
'((\"\\\\\\\\\" . \"\\\\\\\\\")
(\"\\\"\" . \"\\\\\\\"\"))
-achieves this. This does not apply to LEGO, which does not
-need backslash escapes and does not allow filenames with
-quote characters.
+achieves this.
This setting is used inside the function `proof-format-filename'."
:type '(list (cons string string))
@@ -1662,7 +1660,7 @@ prompts than expected, things will break! Extending the
variable
stripped of carriage returns before being sent.
Example uses:
-LEGO uses this hook for setting the pretty printer width if
+Lego used this hook for setting the pretty printer width if
the window width has changed;
Plastic uses it to remove literate-style markup from `string'.
@@ -1679,10 +1677,9 @@ by the user. It is run by `proof-assert-until-point'.
WARNING: don't call `proof-assert-until-point' in this hook, you
would loop forever.
-Example of use: Insert a command to adapt printing width. Note
-that `proof-shell-insert-hook' may be use instead (see lego mode)
-if no more prompt will be displayed (see
-`proof-shell-insert-hook' for details)."
+Example of use: Insert a command to adapt printing width.
+Note that `proof-shell-insert-hook' (which see) may be use instead
+if no more prompt will be displayed."
:type '(repeat function)
:group 'proof-shell)
@@ -1694,10 +1691,9 @@ Can be used to insert commands. It is run by
WARNING: don't call `proof-retract-until-point' in this hook, you
would loop forever.
-Example of use: Insert a command to adapt printing width. Note
-that `proof-shell-insert-hook' may be use instead (see lego mode)
-if no more prompt will be displayed (see
-`proof-shell-insert-hook' for details)."
+Example of use: Insert a command to adapt printing width.
+Note that `proof-shell-insert-hook' (which see) may be use instead
+if no more prompt will be displayed."
:type '(repeat function)
:group 'proof-shell)
@@ -1855,11 +1851,12 @@ Leave unset if no special characters are being used."
:group 'proof-goals)
(defcustom pg-subterm-anns-use-stack nil
+ ;; FIXME: The docstring suggest we should use t!?
"Choice of syntax tree encoding for terms.
If nil, prover is expected to make no optimisations.
If non-nil, the pretty printer of the prover only reports local changes.
-For LEGO 1.3.1 use nil, for Coq 6.2, use t."
+For Coq 6.2, use t."
:type 'boolean
:group 'proof-goals)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4855813..04868f5 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2258,7 +2258,7 @@ No effect if prover is busy."
;;
;; Most of the hard work (computing the commands to do the retraction)
-;; is implemented in the customisation module (lego.el or coq.el), so
+;; is implemented in the customisation module (e.g. coq.el), so
;; code here is fairly straightforward.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 8222fb3..d706fd5 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -3,7 +3,7 @@
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
@@ -627,7 +627,7 @@ It is up to the proof assistant how much context is
cleared: for
example, theories already loaded may be \"cached\" in some way,
so that loading them the next time round only performs a re-linking
operation, not full re-processing. (One way of caching is via
-object files, used by Lego and Coq)."
+object files, used by Coq)."
(interactive)
(when proof-shell-busy
(proof-interrupt-process)
diff --git a/generic/proof-site.el b/generic/proof-site.el
index a66f41f..59e3c84 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -51,8 +51,6 @@
;; Obscure instances or conflict with other Emacs modes.
- ;; (lego "LEGO" "l")
-
;; (hol-light "HOL Light" "ml") ; [for testing]
;; Cut-and-paste management only
@@ -234,7 +232,7 @@ only select the proof assistants you (or your site) may
need.
You can select which proof assistants you want by setting this
variable before `proof-site.el' is loaded, or by setting
the environment variable `PROOFGENERAL_ASSISTANTS' to the
-symbols you want, for example \"lego isa\". Or you can
+symbols you want, for example \"coq easycrypt\". Or you can
edit the file `proof-site.el' itself.
Note: to change proof assistant, you must start a new Emacs session.")
diff --git a/lego/BUGS b/lego/BUGS
deleted file mode 100644
index bfe3975..0000000
--- a/lego/BUGS
+++ /dev/null
@@ -1,53 +0,0 @@
--*- mode:outline -*-
-
-* LEGO Proof General Bugs
-
-See also ../BUGS for generic bugs.
-
-
-** PBP doesn't work on FSF, reason mentioned in generic bugs.
-
-** [FSF specific] `proof-zap-commas-region' does not work for Emacs
-
- On lego/example.l . On *initially* fontifying the buffer,
- commas are not zapped [unfontified]. However, when entering text,
- commata are zapped correctly. Workaround: don't stare too much at commata
-
-** If LEGO attempts to write a (object) file in a non-writable directory
-
- It forgets the protocol mechanism on how to interact with
- Proof General and gets stuck. Workaround: Directly enter "Configure
- AnnotateOn" in the Proof Shell to recover.
-
-** After a `Discharge', retraction ought to only be possible back
-
- to the first declaration/definition which is discharged. However,
- LEGO Proof General does not know that Discharge has such a non-local
- effect. Workaround: retract back to the first declaration/definition
- which is discharged.
-
-** A thorny issue is local definitions in a proof state.
-
- LEGO cannot undo them explicitly. Workaround: retract back to a
- command before a definition.
-
-** Normalisation commands such as `Dnf', `Hnf' `Normal' cannot be undone
-
- in a proof state by Proof General. Workaround: retract back to the
- start of the proof.
-
-** After LEGO has issued a `*** QED ***' you may undo steps in the proof
-
- as long as you don't issue a `Save' command or start a new proof.
- LEGO Proof General assumes that all proofs are terminated with a
- proper `Save' command. Workaround: Always issue a `Save' command after
- completing a proof. If you forget one, you should retract to a point
- before the offending proof development.
-
-** legotags doesn't find all declarations.
-
- It cannot handle lists e.g., with [x,y:nat]; it only tags x but not y.
- [The same problem exists for coqtags]
- Workaround: don't rely too much on the etags mechanism.
-
-
diff --git a/lego/README b/lego/README
deleted file mode 100644
index ee92ec2..0000000
--- a/lego/README
+++ /dev/null
@@ -1,37 +0,0 @@
-LEGO Proof General
-
-Written by Thomas Kleymann and Dilip Sequeira.
-Later maintainance by David Aspinall and Paul Callaghan.
-
-Status: *unsupported* (but tell us about problems)
-Maintainer: Paul Callaghan / David Aspinall
-LEGO version: 1.3.1
-LEGO homepage: http://www.lfcs.informatics.ed.ac.uk/lego
-
-========================================
-
-LEGO Proof General has full support for multiple file scripting, and
-experimental support for proof by pointing.
-
-There is support for X Symbol, but not using a proper token language.
-
-There is a tags program, legotags.
-
-========================================
-
-Installation notes:
-
-Install legotags in a standard place or add <proofgeneral-home>/lego
-to your PATH.
-NB: You may need to change the path to perl at the top of the file.
-
-Generate a TAGS file for the Lego library by running
- legotags `find . -name \*.l -print`
-in the root directory of the library.
-
-
-
-========================================
-
-$Id$
-
diff --git a/lego/example.l b/lego/example.l
deleted file mode 100644
index 535d571..0000000
--- a/lego/example.l
+++ /dev/null
@@ -1,15 +0,0 @@
-(*
- Example proof script for Lego Proof General.
-
- $Id$
-*)
-
-Module example Import lib_logic;
-
-Goal {A,B:Prop}(A /\ B) -> (B /\ A);
-intros;
-Refine H;
-intros;
-andI;
-Immed;
-Save and_comms;
diff --git a/lego/example2.l b/lego/example2.l
deleted file mode 100644
index 37d1e56..0000000
--- a/lego/example2.l
+++ /dev/null
@@ -1 +0,0 @@
-Module example2 Import "readonly/readonly";
\ No newline at end of file
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
deleted file mode 100644
index 1cca4cf..0000000
--- a/lego/lego-syntax.el
+++ /dev/null
@@ -1,131 +0,0 @@
-;;; lego-syntax.el --- Syntax of LEGO
-
-;; This file is part of Proof General.
-
-;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc.
-;; Portions © Copyright 2001-2017 Pierre Courtieu
-;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
-;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
-;; Portions © Copyright 2015-2017 Clément Pit-Claudel
-
-;; Author: Thomas Kleymann and Dilip Sequeira
-;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk>
-
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
-
-;;; Commentary:
-;;
-
-;;; Code:
-
-(require 'proof-syntax)
-
-;; ----- keywords for font-lock.
-
-(defconst lego-keywords-goal '("$?Goal"))
-
-(defconst lego-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen"))
-
-(defconst lego-commands
- (append lego-keywords-goal lego-keywords-save
- '("allE" "allI" "andE" "andI" "Assumption" "Claim"
- "Cut" "Discharge" "DischargeKeep"
- "echo" "exE" "exI" "Expand" "ExpAll"
- "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed"
- "impE" "impI" "Induction" "Inductive"
- "Invert" "Init" "intros" "Intros" "Module" "Next"
- "Normal" "notE" "notI" "orE" "orIL" "orIR" "qnify" "Qnify"
- "Qrepl" "Record" "Refine" "Repeat" "Try" "Unfreeze"))
- "Subset of LEGO keywords and tacticals which are terminated by a \?;")
-
-(defconst lego-keywords
- (append lego-commands
- '("Constructors" "Double" "ElimOver" "Fields" "Import" "Inversion"
- "NoReductions" "Parameters" "Relation" "Theorems")))
-
-(defconst lego-tacticals '("Then" "Else" "Try" "Repeat" "For"))
-
-;; ----- regular expressions for font-lock
-(defconst lego-error-regexp "^\\(cannot assume\\|Error\\|Lego parser\\)"
- "A regular expression indicating that the LEGO process has identified an
error.")
-
-(defvar lego-id proof-id)
-
-(defvar lego-ids (concat lego-id "\\(\\s *,\\s *" lego-id "\\)*")
- "*For font-lock, we treat \",\" separated identifiers as one identifier
- and refontify commata using \\{lego-fixup-change}.")
-
-(defconst lego-arg-list-regexp "\\s *\\(\\[[^]]+\\]\\s *\\)*"
- "Regular expression maching a list of arguments.")
-
-(defun lego-decl-defn-regexp (char)
- (concat "\\[\\s *\\(" lego-ids "\\)" lego-arg-list-regexp char))
-; Examples
-; ^ ^^^^ ^^^^^^^^^^^^^^^^^^^^^^^ ^^^^
-; [ sort =
-; [ sort [n:nat] =
-; [ sort [abbrev=...][n:nat] =
-
-(defconst lego-definiendum-alternative-regexp
- (concat "\\(" lego-id "\\)" lego-arg-list-regexp "\\s * ==")
- "Regular expression where the first match identifies the definiendum.")
-
-(defvar lego-font-lock-terms
- (list
-
- ; lambda binders
- (list (lego-decl-defn-regexp "[:|?]") 1
- 'proof-declaration-name-face)
-
- ; let binders
- (list lego-definiendum-alternative-regexp 1 'font-lock-function-name-face)
- (list (lego-decl-defn-regexp "=") 1 'font-lock-function-name-face)
-
- ; Pi and Sigma binders
- (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1
- 'proof-declaration-name-face)
-
- ;; Kinds
- (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\(("
- lego-id ")\\)?") 'font-lock-type-face)
-
- ;; Special hacks!!
- (cons "Discharge.." 'font-lock-keyword-face)
- (cons "\\*\\*\\* QED \\*\\*\\*" 'font-lock-keyword-face))
- "*Font-lock table for LEGO terms (displayed in output buffers).")
-
-;; Instead of "[^:]+", it may be better to use "lego-id". Furthermore,
-;; it might be safer to append "\\s-*:".
-(defconst lego-goal-with-hole-regexp
- (concat "\\(" (proof-ids-to-regexp lego-keywords-goal)
"\\)\\s-+\\([^(){},:]+\\)")
- "Regular expression which matches an entry in `lego-keywords-goal'
- and the name of the goal.")
-
-(defconst lego-save-with-hole-regexp
- (concat "\\(" (proof-ids-to-regexp lego-keywords-save) "\\)\\s-+\\([^;]+\\)")
- "Regular expression which matches an entry in
- `lego-keywords-save' and the name of the goal.")
-
-(defvar lego-font-lock-keywords-1
- (append
- lego-font-lock-terms
- (list
- (cons (proof-ids-to-regexp lego-keywords) 'font-lock-keyword-face)
- (cons (proof-ids-to-regexp lego-tacticals) 'proof-tacticals-name-face)
- (list lego-goal-with-hole-regexp 2 'font-lock-function-name-face)
- (list lego-save-with-hole-regexp 2 'font-lock-function-name-face)
- ;; Remove spurious variable and function faces on commas.
- '(proof-zap-commas))))
-
-(defun lego-init-syntax-table ()
- "Set appropriate values for syntax table in current buffer."
-
- (modify-syntax-entry ?_ "_")
- (modify-syntax-entry ?\' "_")
- (modify-syntax-entry ?\| ".")
- (modify-syntax-entry ?\* ". 23")
- (modify-syntax-entry ?\( "()1")
- (modify-syntax-entry ?\) ")(4"))
-
-(provide 'lego-syntax)
diff --git a/lego/lego.el b/lego/lego.el
deleted file mode 100644
index 248e9d0..0000000
--- a/lego/lego.el
+++ /dev/null
@@ -1,439 +0,0 @@
-;;; lego.el --- Major mode for LEGO proof assistants
-
-;; This file is part of Proof General.
-
-;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
-;; Portions © Copyright 2001-2017 Pierre Courtieu
-;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
-;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
-;; Portions © Copyright 2015-2017 Clément Pit-Claudel
-
-;; Author: Thomas Kleymann and Dilip Sequeira
-;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk>
-
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
-
-;;; Commentary:
-;;
-
-;;; Code:
-
-(require 'cl-lib) ;cl-member-if
-(require 'proof)
-(require 'lego-syntax)
-(eval-when-compile
- (require 'outline))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;; User Configuration ;;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; I believe this is standard for Linux under RedHat -tms
-(defcustom lego-tags "/usr/lib/lego/lib_Type/"
- "*The directory of the TAGS table for the LEGO library"
- :type 'file
- :group 'lego)
-
-(defcustom lego-test-all-name "test_all"
- "*The name of the LEGO module which inherits all other modules of the
- library."
- :type 'string
- :group 'lego)
-
-(defpgdefault help-menu-entries
- '(["LEGO Reference Card" (browse-url lego-www-refcard) t]
- ["LEGO library (WWW)" (browse-url lego-library-www-page) t]))
-
-(defpgdefault menu-entries
- '(["intros" lego-intros t]
- ["Intros" lego-Intros t]
- ["Refine" lego-Refine t]))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;; Configuration of Generic Proof Package ;;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Users should not need to change this.
-
-(defvar lego-shell-handle-output
- (lambda (cmd string)
- (when (proof-string-match "^Module" cmd)
- ;; prevent output and just give a minibuffer message
- (setq proof-shell-last-output-kind 'systemspecific)
- (message "Imports done!")))
- "Acknowledge end of processing import declarations.")
-
-(defconst lego-process-config
- ;; da: I think "Configure AnnotateOn;" is only included here for
- ;; safety since there is a bug in LEGO which turns it off
- ;; inadvertently sometimes.
- "Init XCC; Configure PrettyOn; Configure AnnotateOn;"
- "Command to initialise the LEGO process.
-
-Initialises empty context and prepares XCC theory.
-Enables pretty printing.
-Activates extended printing routines required for Proof General.")
-
-(defconst lego-pretty-set-width "Configure PrettyWidth %s; "
- "Command to adjust the linewidth for pretty printing of the LEGO
- process.")
-
-(defconst lego-interrupt-regexp "Interrupt.."
- "Regexp corresponding to an interrupt")
-
-;; ----- web documentation
-
-(defcustom lego-www-home-page "http://www.dcs.ed.ac.uk/home/lego/";
- "Lego home page URL."
- :type 'string
- :group 'lego)
-
-(defcustom lego-www-latest-release
- "http://www.dcs.ed.ac.uk/home/lego/html/release-1.3.1/";
- "The WWW address for the latest LEGO release."
- :type 'string
- :group 'lego)
-
-(defcustom lego-www-refcard
- (concat lego-www-latest-release "refcard.ps.gz")
- "URL for the Lego reference card."
- :type 'string
- :group 'lego)
-
-(defcustom lego-library-www-page
- (concat lego-www-latest-release "library/library.html")
- "The HTML documentation of the LEGO library."
- :type 'string
- :group 'lego)
-
-
-;; ----- lego-shell configuration options
-
-(defvar lego-prog-name "lego"
- "*Name of program to run as lego.")
-
-(defvar lego-shell-cd "Cd \"%s\";"
- "*Command of the inferior process to change the directory.")
-
-(defvar lego-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*"
- "*Regular expression indicating that the proof has been completed.")
-
-(defvar lego-save-command-regexp
- (concat "^" (proof-ids-to-regexp lego-keywords-save)))
-(defvar lego-goal-command-regexp
- (concat "^" (proof-ids-to-regexp lego-keywords-goal)))
-
-(defvar lego-kill-goal-command "KillRef;")
-(defvar lego-forget-id-command "Forget %s;")
-
-(defvar lego-undoable-commands-regexp
- (proof-ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal"
- "Qrepl" "Claim" "For" "Repeat" "Succeed" "Fail" "Try" "Assumption"
- "UTac" "Qnify" "qnify" "andE" "andI" "exE" "exI" "orIL" "orIR" "orE" "ImpI"
- "impE" "notI" "notE" "allI" "allE" "Expand" "Induction" "Immed"
- "Invert")) "Undoable list")
-
-;; ----- outline
-
-(defvar lego-goal-regexp "\\?\\([0-9]+\\)")
-
-(defvar lego-outline-regexp
- (concat "[[*]\\|"
- (proof-ids-to-regexp
- '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record"
"Inductive"
- "Unfreeze"))))
-
-(defvar lego-outline-heading-end-regexp ";\\|\\*)")
-
-(defvar lego-shell-outline-regexp lego-goal-regexp)
-(defvar lego-shell-outline-heading-end-regexp lego-goal-regexp)
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Derived modes - they're here 'cos they define keymaps 'n stuff ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-derived-mode lego-shell-mode proof-shell-mode
- "lego-shell"
- "Major mode for LEGO proof scripts.
-
-\\{lego-mode-map}"
- (lego-shell-mode-config))
-
-(define-derived-mode lego-mode proof-mode
- "lego" nil
- (lego-mode-config))
-
-(define-derived-mode lego-response-mode proof-response-mode
- "LEGOResp" nil
- (setq proof-response-font-lock-keywords lego-font-lock-terms)
- (lego-init-syntax-table)
- (proof-response-config-done))
-
-(define-derived-mode lego-goals-mode proof-goals-mode
- "LEGOGoals" "LEGO Proof State"
- (lego-goals-mode-config))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Code that's lego specific ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; needs to handle Normal as well
-;; it should ignore Normal TReg Normal VReg and (Normal ...)
-(defun lego-count-undos (span)
- "This is how to work out what the undo commands are.
-Given is the first SPAN which needs to be undone."
- (let ((ct 0) str i)
- (while span
- (setq str (span-property span 'cmd))
- (cond ((eq (span-property span 'type) 'vanilla)
- (if (or (proof-string-match lego-undoable-commands-regexp str)
- (and (proof-string-match "Equiv" str)
- (not (proof-string-match "Equiv\\s +[TV]Reg" str))))
- (setq ct (+ 1 ct))))
- ((eq (span-property span 'type) 'pbp)
- (setq i 0)
- (while (< i (length str))
- (if (= (aref str i) ?\;) (setq ct (+ 1 ct)))
- (setq i (+ 1 i)))))
- (setq span (next-span span 'type)))
- (list (concat "Undo " (int-to-string ct) ";"))))
-
-(defun lego-goal-command-p (span)
- "Decide whether argument is a goal or not"
- (proof-string-match lego-goal-command-regexp
- (or (span-property span 'cmd) "")))
-
-(defun lego-find-and-forget (span)
- (let (str ans)
- (while (and span (not ans))
- (setq str (span-property span 'cmd))
-
- (cond
-
- ((eq (span-property span 'type) 'comment))
-
- ((eq (span-property span 'type) 'proverproc))
-
- ((eq (span-property span 'type) 'goalsave)
- (unless (eq (span-property span 'name) proof-unnamed-theorem-name)
- (setq ans (format lego-forget-id-command (span-property span
'name)))))
- ;; alternative definitions
- ((proof-string-match lego-definiendum-alternative-regexp str)
- (setq ans (format lego-forget-id-command (match-string 1 str))))
- ;; declarations
- ((proof-string-match (concat "\\`\\$?" (lego-decl-defn-regexp "[:|=]"))
str)
- (let ((ids (match-string 1 str))) ; returns "a,b"
- (proof-string-match proof-id ids) ; matches "a"
- (setq ans (format lego-forget-id-command (match-string 1 ids)))))
-
- ((proof-string-match
"\\`\\(Inductive\\|\\Record\\)\\s-*\\[\\s-*\\w+\\s-*:[^;]+\\`Parameters\\s-*\\[\\s-*\\(\\w+\\)\\s-*:"
str)
- (setq ans (format lego-forget-id-command (match-string 2 str))))
-
- ((proof-string-match
- "\\`\\(Inductive\\|Record\\)\\s-*\\[\\s-*\\(\\w+\\)\\s-*:" str)
- (setq ans
- (format lego-forget-id-command (match-string 2 str))))
-
- ((proof-string-match "\\`\\s-*Module\\s-+\\(\\S-+\\)\\W" str)
- (setq ans (format "ForgetMark %s;" (match-string 1 str)))))
- ;; Carry on searching forward for something to forget
- ;; (The first thing to be forget will forget everything following)
- (setq span (next-span span 'type)))
- (when ans (list ans)))); was (or ans proof-no-command)
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Other stuff which is required to customise script management ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun lego-goal-hyp ()
- (cond
- ((looking-at lego-goal-regexp)
- (cons 'goal (match-string 1)))
- ((looking-at proof-shell-assumption-regexp)
- (cons 'hyp (match-string 1)))
- (t nil)))
-
-
-(defun lego-state-preserving-p (cmd)
- (not (proof-string-match lego-undoable-commands-regexp cmd)))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Commands specific to lego ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(proof-defshortcut lego-Intros "Intros " [(control I)])
-(proof-defshortcut lego-intros "intros " [(control i)])
-(proof-defshortcut lego-Refine "Refine " [(control r)])
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Lego shell startup and exit hooks ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defvar lego-shell-current-line-width nil
- "Current line width of the LEGO process's pretty printing module.
- Its value will be updated whenever the corresponding screen gets
- selected.")
-
-;; The line width needs to be adjusted if the LEGO process is
-;; running and is out of sync with the screen width
-
-(defun lego-shell-adjust-line-width ()
- "Use LEGO's pretty printing facilities to adjust output line width.
-Checks the width in the `proof-goals-buffer'"
- (and (proof-shell-live-buffer)
- (proof-with-current-buffer-if-exists proof-goals-buffer
- (let ((current-width
- ;; Actually, one might sometimes
- ;; want to get the width of the proof-response-buffer
- ;; instead. Never mind.
- (window-width (get-buffer-window proof-goals-buffer t))))
- (if (equal current-width lego-shell-current-line-width) ()
- ; else
- (setq lego-shell-current-line-width current-width)
- (set-buffer proof-shell-buffer)
- (insert (format lego-pretty-set-width (- current-width 1)))
- )))))
-
-(defun lego-mode-config ()
-
- (setq proof-terminal-string ";")
- (setq proof-script-comment-start "(*")
- (setq proof-script-comment-end "*)")
-
- (setq proof-assistant-home-page lego-www-home-page)
-
- (setq proof-showproof-command "Prf;"
- proof-goal-command "Goal %s;"
- proof-save-command "Save %s;"
- proof-context-command "Ctxt;"
- proof-info-command "Help;")
-
- (setq proof-prog-name lego-prog-name)
-
- (setq proof-goal-command-p 'lego-goal-command-p
- proof-completed-proof-behaviour 'closeany ; new in 3.0
- proof-count-undos-fn 'lego-count-undos
- proof-find-and-forget-fn 'lego-find-and-forget
- pg-topterm-goalhyplit-fn 'lego-goal-hyp
- proof-state-preserving-p 'lego-state-preserving-p)
-
- (setq proof-save-command-regexp lego-save-command-regexp
- proof-goal-command-regexp lego-goal-command-regexp
- proof-save-with-hole-regexp lego-save-with-hole-regexp
- proof-goal-with-hole-regexp lego-goal-with-hole-regexp
- proof-kill-goal-command lego-kill-goal-command
- proof-indent-any-regexp
- (proof-regexp-alt (proof-ids-to-regexp lego-commands) "\\s(" "\\s)"))
-
- (lego-init-syntax-table)
-
- ;; da: I've moved these out of proof-config-done in proof-script.el
- (setq pbp-goal-command "Pbp %s;")
- (setq pbp-hyp-command "PbpHyp %s;")
-
-;; font-lock
-
- (set proof-script-font-lock-keywords lego-font-lock-keywords-1)
-
- (proof-config-done)
-
-;; outline
-
- (make-local-variable 'outline-regexp)
- (setq outline-regexp lego-outline-regexp)
-
- (make-local-variable 'outline-heading-end-regexp)
- (setq outline-heading-end-regexp lego-outline-heading-end-regexp)
-
-;; tags
- (cond ((boundp 'tags-table-list) ;; GNU Emacs
- (make-local-variable 'tags-table-list)
- (setq tags-table-list (cons lego-tags tags-table-list))))
-
- (and (boundp 'tag-table-alist) ;; XEmacs
- (setq tag-table-alist
- (append '(("\\.l$" . lego-tags)
- ("lego" . lego-tags))
- tag-table-alist)))
-
- (set (make-local-variable 'blink-matching-paren-dont-ignore-comments) t)
-
-;; hooks and callbacks
-
- (add-hook 'proof-shell-insert-hook 'lego-shell-adjust-line-width))
-
-(defun lego-equal-module-filename (module filename)
- "Returns `t' if MODULE is equal to the FILENAME and `nil' otherwise.
-The directory and extension is stripped of FILENAME before the test."
- (equal module
- (file-name-sans-extension (file-name-nondirectory filename))))
-
-(defun lego-shell-compute-new-files-list ()
- "Function to update `proof-included-files-list'.
-Value for `proof-shell-compute-new-files-list', which see.
-
-For LEGO, we assume that module identifiers coincide with file names."
- (let ((module (match-string 1)))
- (cdr (cl-member-if
- (lambda (filename) (lego-equal-module-filename module filename))
- proof-included-files-list))))
-
-(defun lego-shell-mode-config ()
- (setq proof-shell-cd-cmd lego-shell-cd
- proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp
- proof-shell-error-regexp lego-error-regexp
- proof-shell-interrupt-regexp lego-interrupt-regexp
- proof-shell-assumption-regexp lego-id
- pg-subterm-first-special-char ?\360
- pg-subterm-start-char ?\372
- pg-subterm-sep-char ?\373
- pg-subterm-end-char ?\374
- pg-topterm-regexp "\375"
- proof-shell-eager-annotation-start "\376"
- proof-shell-eager-annotation-start-length 1
- proof-shell-eager-annotation-end "\377"
- proof-shell-annotated-prompt-regexp "Lego> \371"
- proof-shell-result-start "\372 Pbp result \373"
- proof-shell-result-end "\372 End Pbp result \373"
- proof-shell-start-goals-regexp "\372 Start of Goals \373"
- proof-shell-end-goals-regexp "\372 End of Goals \373"
- proof-shell-pre-sync-init-cmd "Configure AnnotateOn;"
- proof-shell-init-cmd lego-process-config
- proof-shell-restart-cmd lego-process-config
- pg-subterm-anns-use-stack nil
- proof-shell-handle-output-system-specific lego-shell-handle-output
- lego-shell-current-line-width nil
-
- ;; LEGO uses Unicode escape prefix: liable to create problems
- proof-shell-unicode nil
-
- proof-shell-process-file
- (cons "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]"
- (lambda () (let ((match (match-string 2)))
- (if (equal match "") match
- (concat (file-name-sans-extension match) ".l")))))
-
- proof-shell-retract-files-regexp
- "forgot back through Mark \"\\(.*\\)\""
-
- proof-shell-font-lock-keywords lego-font-lock-keywords-1
-
- proof-shell-compute-new-files-list
- 'lego-shell-compute-new-files-list)
-
- (lego-init-syntax-table)
-
- (proof-shell-config-done))
-
-(defun lego-goals-mode-config ()
- (setq pg-goals-change-goal "Next %s;"
- pg-goals-error-regexp lego-error-regexp)
- (setq font-lock-keywords lego-font-lock-terms)
- (lego-init-syntax-table)
- (proof-goals-config-done))
-
-
-(provide 'lego)
diff --git a/lego/legotags b/lego/legotags
deleted file mode 100755
index 8243287..0000000
--- a/lego/legotags
+++ /dev/null
@@ -1,91 +0,0 @@
-#!/usr/bin/perl
-#
-# Or perhaps: /usr/local/bin/perl
-#
-# $Id$
-#
-undef $/;
-
-if($#ARGV<$[) {die "No Files\n";}
-open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n";
-
-while(<>)
-{
- print "Tagging $ARGV\n";
- $a=$_;
- $cp=1;
- $lp=1;
- $tagstring="";
-
- while(1)
- {
-
-# ---- Get the next statement starting on a newline ----
-
- if($a=~/^[ \t\n]*\(\*/)
- { while($a=~/^\s*\(\*/)
- { $d=1; $a=$'; $cp+=length $&; $lp+=(($wombat=$&)=~tr/\n/\n/);
- while($d>0 && $a=~/\(\*|\*\)/)
- { $a=$'; $cp+=2+length $`; $lp+=(($wombat=$`)=~tr/\n/\n/);
- if($& eq "(*") {$d++} else {$d--};
- }
- if($d!=0) {die "Unbalanced Comment?";}
- }
- }
-
- if($cp>1 && $a=~/.*\n/) {$a=$'; $cp+=length $&; $lp++;}
- while($a=~/^\n/) {$cp++;$lp++;$a=$'}
-
- if($a=~/^[^;]*;/)
- { $stmt=$&;
- $newa=$';
- $newcp=$cp+length $&;
- $newlp=$lp+(($wombat=$&)=~tr/\n/\n/); }
- else { last;}
-
-# ---- The above embarrasses itself if there are semicolons inside comments
-# ---- inside commands. Could do better.
-
-# print "----- (",$lp,",",$cp,")\n", $stmt, "\n";
-
- if($stmt=~/^([ \t]*\$?Goal\s*([\w\']+))\s*:/)
- { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; }
-
- elsif($stmt=~/^([ \t]*\$?\[\s*[\w\']+)/)
- { do adddecs($stmt,$1) }
-
- elsif($stmt=~/^([ \t]*Inductive\s*\[\s*[\w\']+)/)
- { do adddecs($stmt,$1) }
-
-# ---- we don't need to tag saves: all goals should be named!
-
-# elsif($stmt=~/([ \t]*\$?Save\s+([\w\']+))/)
-# { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; }
-#
-# elsif($stmt=~/^([ \t]*\$?SaveUnfrozen\s+([\w\']+))/)
-# { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; }
-
-# ---- Maybe do something smart with discharge as well?
-
- $cp=$newcp; $lp=$newlp; $a=$newa;
- }
- print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring;
-}
-close tagfile;
-
-
-sub adddecs {
- $wk=$_[0];
- $tag=$_[1];
- while($wk=~/\[\s*([\w\']+)/)
- { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$';
- while($wk=~/^\s*,\s*([\w\']+)/)
- { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; }
- $d=1;
- while($d>0 && $wk=~/\[|\]/)
- { $wk=$'; if($& eq "[") {$d++} else {$d--};
- }
- }
- 0;
-}
-
diff --git a/lego/root2.l b/lego/root2.l
deleted file mode 100644
index 5712b12..0000000
--- a/lego/root2.l
+++ /dev/null
@@ -1,368 +0,0 @@
-(************************************************************************
- Conor McBride's proof that 2 has no rational root.
-
- This proof is accepted by LEGO version 1.3.1 with its standard library.
-*************************************************************************)
-
-Make lib_nat; (* loading basic logic, nat, plus, times etc *)
-
-(* note, plus and times are defined by recursion on their first arg *)
-
-
-(************************************************************************
- Alternative eliminators for nat
-
- LEGO's induction tactic figures out which induction principle to use
- by looking at the type of the variable on which we're doing induction.
- Consequently, we can persuade the tactic to use an alternative induction
- principle if we alias the type.
-
- Nat_elim is just the case analysis principle for natural numbers---the
- same as the induction principle except that there's no inductive hypothesis
- in the step case. It's intended to be used in combination with...
-
- ...NAT_elim, which performs no case analysis but says you can have an
- inductive hypothesis for any smaller value, where y is smaller than
- suc (plus x y). This is `well-founded induction' for the < relation,
- but expressed more concretely.
-
- The effect is very similar to that of `Case' and `Fix' in Coq.
-************************************************************************)
-
-[Nat = nat];
-[NAT = Nat];
-
-(* case analysis: just a weakening of induction *)
-
-Goal Nat_elim : {Phi:nat->Type}
- {phiz:Phi zero}
- {phis:{n:Nat}Phi (suc n)}
- {n:Nat}Phi n;
-intros ___;
- Expand Nat; Induction n;
- Immed;
- intros; Immed;
-Save;
-
-(* suc-plus guarded induction: the usual proof *)
-
-Goal NAT_elim :
- {Phi:nat->Type}
- {phi:{n:Nat}
- {ih:{x,y|Nat}(Eq n (suc (plus x y)))->Phi y}
- Phi n}
- {n:NAT}Phi n;
-intros Phi phi n';
-(* claim that we can build the hypothesis collector for each n *)
-Claim {n:nat}{x,y|Nat}(Eq n (suc (plus x y)))->Phi y;
-(* use phi on the claimed collector *)
-Refine phi n' (?+1 n');
-(* now build the collector by one-step induction *)
- Induction n;
- Qnify; (* nothing to collect for zero *)
- intros n nhyp;
- Induction x; (* case analysis on the slack *)
- Qnify;
- Refine phi; (* if the bound is tight, use phi to *)
- Immed; (* generate the new member of the collection *)
- Qnify;
- Refine nhyp; (* otherwise, we've already collected it *)
- Immed;
-Save;
-
-
-(***************************************************************************
- Equational laws governing plus and times:
- some of these are doubtless in the library, but it takes longer to
- remember their names than to prove them again.
-****************************************************************************)
-
-Goal plusZero : {x:nat}Eq (plus x zero) x;
-Induction x;
- Refine Eq_refl;
- intros;
- Refine Eq_resp suc;
- Immed;
-Save;
-
-Goal plusSuc : {x,y:nat}Eq (plus x (suc y)) (suc (plus x y));
-Induction x;
- intros; Refine Eq_refl;
- intros;
- Refine Eq_resp suc;
- Immed;
-Save;
-
-Goal plusAssoc : {x,y,z:nat}Eq (plus (plus x y) z) (plus x (plus y z));
-Induction x;
- intros; Refine Eq_refl;
- intros;
- Refine Eq_resp suc;
- Immed;
-Save;
-
-Goal plusComm : {x,y:nat}Eq (plus x y) (plus y x);
-Induction y;
- Refine plusZero;
- intros y yh x;
- Refine Eq_trans (plusSuc x y);
- Refine Eq_resp suc;
- Immed;
-Save;
-
-Goal plusCommA : {x,y,z:nat}Eq (plus x (plus y z)) (plus y (plus x z));
-intros;
- Refine Eq_trans ? (plusAssoc ???);
- Refine Eq_trans (Eq_sym (plusAssoc ???));
- Refine Eq_resp ([w:nat]plus w z);
- Refine plusComm;
-Save;
-
-Goal timesZero : {x:nat}Eq (times x zero) zero;
-Induction x;
- Refine Eq_refl;
- intros;
- Immed;
-Save;
-
-Goal timesSuc : {x,y:nat}Eq (times x (suc y)) (plus x (times x y));
-Induction x;
- intros; Refine Eq_refl;
- intros x xh y;
- Equiv Eq (suc (plus y (times x (suc y)))) ?;
- Equiv Eq ? (suc (plus x (plus y (times x y))));
- Refine Eq_resp;
- Qrepl xh y;
- Refine plusCommA;
-Save;
-
-Goal timesComm : {x,y:nat}Eq (times x y) (times y x);
-Induction y;
- Refine timesZero;
- intros y yh x;
- Refine Eq_trans (timesSuc ??);
- Refine Eq_resp (plus x);
- Immed;
-Save;
-
-Goal timesDistL : {x,y,z:nat}Eq (times (plus x y) z)
- (plus (times x z) (times y z));
-Induction x;
- intros; Refine Eq_refl;
- intros x xh y z;
- Refine Eq_trans (Eq_resp (plus z) (xh y z));
- Refine Eq_sym (plusAssoc ???);
-Save;
-
-Goal timesAssoc : {x,y,z:nat}Eq (times (times x y) z) (times x (times y z));
-Induction x;
- intros; Refine Eq_refl;
- intros x xh y z;
- Refine Eq_trans (timesDistL ???);
- Refine Eq_resp (plus (times y z));
- Immed;
-Save;
-
-(**********************************************************************
- Inversion principles for equations governing plus and times:
- these aren't in the library, at least not in this form.
-***********************************************************************)
-
-[Phi|Type]; (* Inversion principles are polymorphic in any goal *)
-
-Goal plusCancelL : {y,z|nat}{phi:{q':Eq y z}Phi}{x|nat}
- {q:Eq (plus x y) (plus x z)}Phi;
-intros ___;
-Induction x;
- intros;
- Refine phi q;
- intros x xh; Qnify;
- Refine xh;
- Immed;
-Save;
-
-Goal timesToZero : {a,b|Nat}
- {phiL:(Eq a zero)->Phi}
- {phiR:(Eq b zero)->Phi}
- {tz:Eq (times a b) zero}
- Phi;
-Induction a;
- intros; Refine phiL (Eq_refl ?);
- intros a;
- Induction b;
- intros; Refine phiR (Eq_refl ?);
- Qnify;
-Save;
-
-Goal timesToNonZero : {x,y|nat}
- {phi:{x',y'|nat}(Eq x (suc x'))->(Eq y (suc y'))->Phi}
- {z|nat}{q:Eq (times x y) (suc z)}Phi;
-Induction x;
- Qnify;
- intros x xh;
- Induction y;
- intros __; Qrepl timesZero (suc x); Qnify;
- intros;
- [EQR=Eq_refl]; Refine phi Then Immed;
-Save;
-
-(* I actually want plusDivisionL, but plusDivisionR is easier to prove,
- because here we do induction where times does computation. *)
-Goal plusDivisionR : {b|nat}{a,x,c|Nat}
- {phi:{c'|nat}(Eq (times c' (suc x)) c)->
- (Eq a (plus b c'))->Phi}
- {q:Eq (times a (suc x)) (plus (times b (suc x)) c)}
- Phi;
-Induction b;
- intros _____; Refine phi;
- Immed;
- Refine Eq_refl;
- intros b bh;
- Induction a;
- Qnify;
- intros a x c phi;
- Qrepl plusAssoc (suc x) (times b (suc x)) c;
- Refine plusCancelL;
- Refine bh;
- intros c q1 q2; Refine phi q1;
- Refine Eq_resp ? q2;
-Save;
-
-(* A bit of timesComm gives us the one we really need. *)
-Goal plusDivisionL : {b|nat}{a,x,c|Nat}
- {phi:{c'|nat}(Eq (times (suc x) c') c)->
- (Eq a (plus b c'))->Phi}
- {q:Eq (times (suc x) a) (plus (times (suc x) b) c)}
- Phi;
-intros _____;
- Qrepl timesComm (suc x) a; Qrepl timesComm (suc x) b;
- Refine plusDivisionR;
- intros c'; Qrepl timesComm c' (suc x);
- Immed;
-Save;
-
-Discharge Phi;
-
-
-(**************************************************************************
- Definition of primality:
-
- This choice of definition makes primality easy to exploit
- (especially as it's presented as an inversion principle), but hard to
- establish.
-***************************************************************************)
-
-[Prime = [p:nat]
- {a|NAT}{b,x|Nat}{Phi|Prop}
- {q:Eq (times p x) (times a b)}
- {phiL:{a':nat}
- (Eq a (times p a'))->(Eq x (times a' b))->Phi}
- {phiR:{b':nat}
- (Eq b (times p b'))->(Eq x (times a b'))->Phi}
- Phi
-];
-
-
-(**************************************************************************
- Proof that 2 is Prime. Nontrivial because of the above definition.
- Manageable because 1 is the only number between 0 and 2.
-***************************************************************************)
-
-Goal doublePlusGood : {x,y:nat}Eq (times (suc (suc x)) y)
- (plus (times two y) (times x y));
-intros __;
- Refine Eq_trans ? (Eq_sym (plusAssoc ???));
- Refine Eq_resp (plus y);
- Refine Eq_trans ? (Eq_sym (plusAssoc ???));
- Refine Eq_refl;
-Save;
-
-Goal twoPrime : Prime two;
-Expand Prime;
- Induction a;
- Induction n;
- intros useless b x _;
- Refine timesToZero Then Expand Nat Then Qnify;
- (* Qnify needs to know it's a nat *)
- intros; Refine phiL;
- Refine +1 (Eq_sym (timesZero ?));
- Refine Eq_refl;
- Induction n;
- intros useless b x _;
- Qrepl plusZero b;
- intros; Refine phiR;
- Refine +1 Eq_sym q;
- Refine Eq_sym (plusZero x);
- intros n nhyp b x _;
- Qrepl doublePlusGood n b;
- Refine plusDivisionL;
- intros c q1 q2; Qrepl q2; intros __;
- Refine nhyp|one (Eq_refl ?) q1;
- intros a' q3 q4; Refine phiL (suc a');
- Refine Eq_resp suc;
- Refine Eq_trans ? (Eq_sym (plusSuc ??));
- Refine Eq_resp ? q3;
- Refine Eq_resp (plus b) q4;
- intros b' q3 q4; Refine phiR b';
- Immed;
- Qrepl q3; Qrepl q4;
- Refine Eq_sym (doublePlusGood ??);
-Save;
-
-
-(**************************************************************************
- Now the proof that primes (>=2) have no rational root. It's the
- classic `minimal counterexample' proof unwound as an induction: we
- apply the inductive hypothesis to the smaller counterexample we
- construct.
-***************************************************************************)
-
-[pm2:nat]
-[p=suc (suc pm2)] (* p is at least 2 *)
-[Pp:Prime p];
-
-Goal noRatRoot : {b|NAT}{a|Nat}{q:Eq (times p (times a a)) (times b b)}
- and (Eq a zero) (Eq b zero);
-Induction b;
- Induction n; (* if b is zero, so is a, and the result holds *)
- intros useless;
- intros a;
- Refine timesToZero;
- Expand Nat; Qnify;
- Refine timesToZero; Refine ?+1;
- intros; Refine pair; Immed; Refine Eq_refl;
- intros b hyp a q; (* otherwise, build a smaller counterexample *)
- Refine Pp q; (* use primality once *)
- Refine cut ?+1; (* standard technique for exploiting symmetry *)
- intros H a' aq1 aq2; Refine H;
- Immed;
- Refine Eq_trans aq2;
- Refine timesComm;
- intros c bq; Qrepl bq; Qrepl timesAssoc p c c;
- Refine timesToNonZero ? (Eq_sym bq); (* need c to be nonzero *)
- intros p' c' dull cq; Qrepl cq; intros q2;
- Refine Pp (Eq_sym q2); (* use primality twice *)
- Refine cut ?+1; (* symmetry again *)
- intros H a' aq1 aq2; Refine H;
- Immed;
- Refine Eq_trans aq2;
- Refine timesComm;
- intros d aq; Qrepl aq; Qrepl timesAssoc p d d;
- intros q3;
- Refine hyp ? (Eq_sym q3); (* now use ind hyp *)
- Next +2; Expand NAT Nat; Qnify; (* trivial solution *)
- Next +1; (* show induction was properly guarded *)
- Refine Eq_trans bq; Expand p; Qrepl cq;
- Refine plusComm;
-Save;
-
-Discharge pm2;
-
-(**********************************************************************
- Putting it all together
-***********************************************************************)
-
-[noRatRootTwo = noRatRoot zero twoPrime
- : {b|nat}{a|nat}(Eq (times two (times a a)) (times b b))->
- (Eq a zero /\ Eq b zero)];
-
diff --git a/proof-general.el b/proof-general.el
index b72509b..4feed65 100644
--- a/proof-general.el
+++ b/proof-general.el
@@ -81,7 +81,7 @@
;; FIXME: These dirs used to not be listed, but I needed to add
;; them for the compilation to succeed for me. --Stef
;; These dirs are now obsolete and not published on MELPA. --Erik
- ;; "isar" "lego" "obsolete/plastic"
+ ;; "isar" "obsolete/plastic"
)))
(dolist (dir byte-compile-directories)
(add-to-list 'load-path (expand-file-name dir pg-init--pg-root)))))
- [nongnu] elpa/proof-general updated (20412f1 -> 1b1083e), ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 1931c8c 01/13: Remove Twelf support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 48bd86b 02/13: Remove HOL98 support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 73571a5 03/13: Remove CCC support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 8b16d1d 04/13: Remove LEGO support,
ELPA Syncer <=
- [nongnu] elpa/proof-general 23f7895 05/13: Remove Hol-Light support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 6c9c995 12/13: Change the license to GPLv3+ (Fix #198), ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 511226f 09/13: Remove Isabelle/Isar support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 497709f 10/13: AUTHORS: Add notes about copyright status, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 0a295cd 07/13: Remove Plastic support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general e27b1ef 08/13: Remove Lambda-Clam support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general f99cdf2 11/13: Misc cosmetic tweaks that occurred during GPLv3+ license work, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general da5f073 06/13: Remove ACL2 support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 1b1083e 13/13: Merge pull request #627 from ProofGeneral/scratch-GPLv3, ELPA Syncer, 2021/11/25