This document will give a basic introduction to the theorem prover and run through a reasoning example demonstrate how it can be used to reason about LF specifications.
The syntax for terms Canonical LF terms and types follows a similar style to that used by Twelf. Of note are the following structures.
[x] M
(term abstraction)
{x:A}B
(pi-types)
A -> B
(shorthand for pi-type without dependency)
Nominal constants are denoted by n1
, n2
, ... .
The names for variables and constants follow the same conventions as Twelf.
Context expressions G
are expressed using the following syntax.
<empty string>
(empty context)
Γ
(context variable)
G, n:A
(explicit context entry)
The syntax for formulas F
is the following.
forall x y z ..., F
(universal quantification)
exists x y z ..., F
(existential quantification)
ctx Γ1:C1 Γ2:C2 ..., F
(context quantification)
F1 => F2
(implication)
F1 /\ F2
(conjunction)
F1 \/ F2
(disjunction)
{G |- M : A}
(atomic formula)
pred M1 M2 ...
(defined predicate)
true
false
Quantified variables can optionally be given an arity type explicitly
which are constructed from o
using the constructor ->
.
search.
search <NUM>.
Search for a derivation of the current goal using matching with assumption formulas and decomposing judgments into subgoals using LF derivation rules. If a<NUM>
is provided, assumption judgements are decomposed<NUM>
times. If a<NUM>
is not provided, thesearch_depth
option is used. Thesearch_depth
can be changed with the Set command.intros.
Introduces variables and assumptions from a goal formula until it no longer has top-level universal quantification, context quantification, or implications.split.
If the current goal is a conjunction,F1 /\ F2
, creates subgoals for each sub formula,F1
andF2
.left.
If the current goal is a disjunction,F1 \/ F2
, changes the goal to be the left side formula,F1
.right.
If the current goal is a disjunction,F1 \/ F2
, changes the goal to be the right side formula,F2
.assert <FORMULA>.
assert <FORMULA> <NUM>.
Changes the proof state to one which has the given formula as a goal; once derivation of this goal is complete returns to the previous proof state with the given formula added as an assumption. Providing a<NUM>
will decompose assumption judgements<NUM>
times. If the asserted<FORMULA>
can be proven, it is added to the proof state immediately. This option defaults tosearch_depth
when not provided and may be changed with the Set command.apply <HYP NAME> to <HYP NAMES>.
apply <HYP NAME> to <HYP NAMES> with (Γ1 = G1), ..., (Γm = Gm), X1 = M1, ..., Xn = Mn.
Theapply
tactic applies a hypothesis of the formctx Γ1:C1 ... Γj:Cj, forall X1 ... Xi, H1 => ... => Hk => F
to argument hypotheses which matchH1
, ...,Hk
. The result is an instantiation ofF
. Either or both of i and j may be zero, that is there need not be universally quantified variables or context variables. Thewith
clause allows specific instantiations of any of the variablesX1
...Xi
andΓ1
...Γj
.
A previously proved theorem can be used instead of the first hypothesis, and then this acts like using a lemma.
It is recommended to provide the instantiations for quantifiers as the inference of these instantiations is only successful in simple cases.induction on <NUM>.
Given a goal of the formctx Γ1:C1 Γ2:C2 ..., forall X Y ..., H1 => H2 => ... => F
theinduction
tactic allows you to induct on one ofH1
,H2
,...
. The hypothesis to be inducted on must be an atomic formula. The choice of induction is based on the number<NUM>
. Applying theinduction
tactic results in an inductive hypothesis being added to the current set of hypotheses. Specifics on this inductive hypothesis and how it relates to the goal are given in the section Inductive Restrictions.
Adelfa supports nested induction through repeated calls to theinduction
tactic. See the Inductive Restrictions section for more details.exists M.
Instantiates an existential goal with the given term, if it is of the correct arity type.case <HYP NAME>.
case <HYP NAME>(keep).
Performs case analysis on the given assumption formula. By default, the assumption is removed, use `(keep)' to retain it.weaken <HYP NAME> with A.
weaken <HYP NAME> with A <NUM>.
When the given assumption formula is of the form{G |- M : A}
, and it can be verified that the LF typeA
must be well formed in the current context underG
, then a new assumption is added in which the typing judgment is weakened to include the given type.strengthen <HYP NAME>.
If the given assumption formula is of the form{G, n:A1 |- M : A2}
ifn
does not appear inM
orA2
then a new assumption is added in which the typing judgment is strengthened to{G |- M : A2}
.ctxpermute <HYP NAME> to G.
If the given assumption is of the form{G' |- M:A}
, and if the given context is a valid permutation of the contextG'
(i.e. does not violate dependencies), then a new assumption is added with the permuted context expressionG
.permute <HYP NAME> with <PERM>.
Where<PERM>
is a series of nominal constants being mapped to others such that it is a complete permutation. Mappings can be unidirectionaln1 -> n2, n2 -> n1
or bidirectionaln1 <-> n2
.
If the provided permutation is complete and limited to be within the relevant assumption's restricted set, a new assumption is added with the permutation applied to it.inst <HYP NAME> with n = M.
If the given assumption formula is of the form{G1,n:B,G2 |- M:A}
, and the termM
can be determined to be such that{G1 |- M : B}
is valid then this tactic replaces the given assumption with one in whichn:B
is removed from the context expression and all occurrences ofn
are replaced byM
.prune <HYP NAME>.
If the given assumption is of the form{G |- X n1 ... nm : A}
for some eigenvariableX
and distinct nominal constantsn1
,...
,nm
then this tactic will prune those nominal constants appearing as arguments toX
which (1) do not already appear inG
and (2) are not permitted in the instantiations for the context variable inG
.undo.
Undo the last step of reasoning.skip.
Skip to the next subgoal of the derivation.abort.
Abort the proof construction and return to top-level loop without adding formula to the available lemmas.unfold.
unfold <HYP NAME>.
If the given assumption formula is a defined predicate then it is unfolded using the relevant definition, using the first clause which matches. If no assumption formula is given, the goal formula is unfolded.applydfn <PROP>.
applydfn <PROP> to <HYP NAME>.
Applies a clause of the definition of<PROP>
to the given assumption formula. The first clause which matches is the one used. If no assumption formula is provided the definition is applied to the goal formula.
To use a lemma, prove it as a theorem and then refer to it by name in
another proof using the apply
tactic. For example,
Theorem my_lemma : ... ... Theorem my_theorem : ... ... apply my_lemma to H3 H5. ...
Adelfa's logic is simply-typed using simple arity typing based on a single base type
o
and constructor ->
.
All terms and formulas must be well-typed.
Inductive restrictions are represented by *
(smaller)
and @
(equal). They are used to track the size of
inductive arguments rather than using explicit numeric values. For
example, suppose we apply induction on 1.
when trying to
prove the following subject reduction theorem,
============================ forall E V T D1 D2, {|- D1 : eval E V} -> {|- D2: of E T} -> exists D3, {|- D3: of V T}
We will get the following proof state.
IH : forall E V T D1 D2, {|- D1 : eval E V}* -> {|- D2: of E T} -> exists D3, {|- D3: of V T} ============================ forall E V T D1 D2, {|- D1 : eval E V}@ -> {|- D2: of E T} -> exists D3, {|- D3: of V T}
Here we have an inductive hypothesis where the inductive argument is
flagged with *
. This means that we can only apply that
hypothesis to an argument which also has the *
.
Because *
means smaller, in order to get an argument with
a *
we must perform case analysis on an argument that is
"equal" which we denote by @
. Thus, the above proof
proceeds by first doing "intros." and then case analysis on
{|- D1 : eval E V}@
. This will give us two subgoals,
one which is trivial and the other which has hypotheses tagged
with *
and thus eligible for use with the inductive hypothesis.
The adelfa.tar provides a Proof General mode and syntax
highlighting for developing proofs in its PG/
directory. To
use it, install Proof General as instructed by its documentation. Then
copy the entirety of the adelfa
directory into the
installation location of Proof General. Add an entry for Adelfa in PG's
proof-assistant-table-default
resembling (adelfa
"Adelfa" "ath")
, located in PG/generic/proof-site.el
.
Afterwards, the proof-assistant-table-default
should resemble
something similar to:
(defconst proof-assistant-table-default '( ;; Main instances of PG. (isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (easycrypt "EasyCrypt" "ec" "\\.eca?\\'") (phox "PhoX" "phx" nil (".phi" ".pho")) (adelfa "Adelfa" "ath")
In your Emacs configuration, commonly located at ~/.emacs
or
~/.emacs.d/init.el
, add the following lines:
(defconst proof-site-file (expand-file-name "path-to-pg/PG/generic/proof-site.el")) (when (file-exists-p proof-site-file) (setq proof-splash-enable nil proof-output-tooltips nil proof-three-window-mode-policy 'horizontal) (load-file proof-site-file) (add-hook 'adelfa-mode-hook #'(lambda () (setq indent-line-function 'indent-relative))) (setq auto-mode-alist (append '(("\\.ath\\'" . adelfa-mode)) auto-mode-alist)))
Where path-to-pg
should be changed to the file path of your proof general installation.