?
"s indicating the location of
fields to be entered. As shown below,
all we need to enter in Step #2 is a formula; there are no hypotheses
involved.Ctrl
and "U
" keys simultaneously.qed
" step, the Metamath
RPN-format proof is also displayed:$= wph wps wph wi a1i.1 wph wps ax-1 ax-mp $.
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a1i.1 | . 2 ⊢ φ | |
2 | ax-1 3 | . 2 ⊢ (φ → (ψ → φ)) | |
3 | 1, 2 | ax-mp 6 | 1 ⊢ (ψ → φ) |
$(
" and ends with "$)
", must consist of valid Metamath
tokens, and must not contain
nested Metamath comments. (This is a
"feature" that allows the student/mathelogician to embed GUI proof
texts inside a Metamath
.mm file, if desired.)$(
" is treated as
an error. $)
" is ignored and will be
erased automatically.THEOREM
and LOC_AFTER
label values to
"clone" a proof.h
",
and that the final proof step "number" equal "qed
".
Given these bits of information, plus the Header's THEOREM=
label value and LOC_AFTER=
value, plus any
(optional) Distinct
Variable statements, the Proof Assistant can construct a
Metamath theorem in memory
and then validate/unify its proof. The only limitation is that the GUI
does not provide a way to enter new dummy variable definitions as part
of the proof text; any variables referenced in a new theorem proof must
be defined at the global scope level of the input Metamath .mm file.LOC_AFTER
field on
the proof text Header
statement is used only to specify the logical location of a new
theorem in the loaded set of Metamath statements; it is ignored when
present on a proof for an existing theorem. Location is significant in
Metamath because statements may refer only to previous statements in a
Metamath file. If LOC_AFTER
is
left blank (or = "?
"), then the
GUI treats the new theorem as if it were the last Metamath statement in
the database.File/New
specifying "a1i
". Then in the displayed proof text area,
change "THEOREM=a1i
" in the Header statement to "THEOREM=TESTa1i
", and set the Step:Hyp:
Ref data
on the qed
proof
step to "qed:1
", but.do not
change "LOC_AFTER=?
". Then
select menu item Unify/Unify (check
proof). If the Proof Assistant GUI program is working correctly,
the unification algorithm will complete the proof, assigning a1i
to the qed
proof step Ref.]$d x y z
"
may be entered in the proof text area. Each must begin in column 1 of a
new, separate line of the proof text (i.e. if two Distinct
Variable
statements are needed, then each must be entered on a separate proof
text area line.) This capability was added to the GUI specification as
an
afterthought because it was realized that figuring out the needed $d
's is an iterative process, with
some trial and error, even for highly expert Metamath users. A
Distinct Variable statement entered in a GUI proof text is treated as
an addition of distinct
variable restrictions to those already present
for the theorem in the loaded Metamath .mm file (except when
option "GenerateNew
" is selected on the Edit/Set Soft Dj
Vars Error Handling menu item.). * Comment begins with "*" in column 1
and
continues until the next line of the Proof
Text area which does not have a space in
column 1.
* Note how Formulas may be indented and spaced
freely by the user, continuing onto as many
lines as desired.
* Following are Distinct Variable
statements
(may occur anywhere inside the Proof Text
between the Header and Footer statements):
$d th ta
$d ch ta
* Note: Distinct Variable restrictions added
are applied in conjunction with any Distinct
Variable restrictions already contained in
the Metamath .mm file for the Theorem unless
"GenerateNew" is selected on the Edit/Set
Soft Dj Vars Error Handling menu item.
$)Request Message Window Handling |
Error and Informational messages
produced by the Proof Assistant GUI appear in a small text window
"pane" on the main Proof Assistant GUI window. A separate Request
Message window is created containing these messages and can be viewed
using Alt-Tab. |
Unification Search Sequence |
The program searches the loaded
Metamath assertions (from the .mm file(s)) in ascending database
sequence. That means that if two assertions satisfactorily unify with a
given proof step, the assertion that appears earliest in the input
files is used. If this is unacceptable the user can simply input the
correct assertion label. |
Unify Search Exclusions |
New RunParm to exclude loaded
assertions from the Unification search (example):ProofAsstUnifySearchExclude,biigb,xxxid |
Distinct Variable Errors and Alternative Unifications |
When the user manually inputs a
Ref for a proof step and that Ref either does not unify satisfactorily
or has Distinct Variable restriction errors, a message is produced
showing the assertions that do unify with the proof step. In the case
where the user leaves the Ref blank and allows the program to search
for a unifying assertion, the first Ref that unifies with the proof
step is taken and used, provisionally. If the Ref has a Distinct
Variable restriction error, the search continues, looking for a perfect
unification without the $d errors; if this secondary search is
unsuccessful, an informational message displaying altervative
assertions is produced. Note: The Edit menu (and input RunParm file) provide a choice about how "soft" Distinct Variable restriction errors are handled. '"Soft" Dj Vars Errors' refers to missing or incomplete $d statements on the theorem being proved. The default setting is not to report these errors but to "GenerateReplacements", which creates a complete set of $d statements for the theorem being proved once unification is completed for the 'qed' step of the proof. "Hard" errors, which occur when a pair of substitution variables violates the $d restrictions specified by a proof step Ref assertion are always reported and cannot be "fixed" by the mmj2 program. |
Annotated RunParms .txt |
Many options to customize
processing can be set by updating the "RunParms.txt" file which is
input in the mmj2.bat command file. All RunParm values and options are
documented in mmj2\mmj2jar\AnnotatedRunParms.txt.
For some features of mmj2, the AnnotatedRunParms.txt file is the only
source of documentation, so you may want to have a look; your
experience with the mmj2 Proof Assistant can be easily customized and
optimized to satisfy your personal requirements and preferences. |