Interactive Command Reference¶
Administrative tactics¶
Administrative tactics are used to navigate the proof, obtain information about functions or constructors, or to prove a lemma in the middle of another proof.
undo
¶
Undoes the effect of a previous proof tactic. See Undo.
theorem list
¶
Lists all theorems in the current session.
theorem defer
¶
Moves the current theorem to the bottom of the theorem stack, selecting the next theorem.
See select for a more flexible way to select a theorem.
theorem show-ihs
¶
Display the induction hypotheses available in the current subgoal.
Note
This is a debugging command, and the output is not particularly human-readable.
theorem dump-proof PATH
¶
Records the current theorem’s partial proof to PATH
.
theorem show-proof
¶
Displays the current theorem’s partial proof.
session list
¶
Lists all active sessions together with all theorems within each session.
session defer
¶
Moves the current session to the bottom of the session stack and selects the next one.
See select for a more flexible way to select a theorem.
session create
¶
Creates a new session. This command will start the Session configuration wizard for setting up the theorems in the new session.
session serialize
¶
Saves the current session as partial proofs to the signature. In other words, any work done interactively will be reflected back into the loaded signature.
subgoal list
¶
Lists all remaining subgoals in the current theorem.
subgoal defer
¶
Moves the current subgoal to the bottom of the subgoal stack and selects the next one.
select
¶
select NAME
selects a theorem by name for proving.
See the session list command.
Note
When selecting a theorem from another session, be aware of the consequences this has on scoping. See Changing sessions.
rename
¶
Note
Renaming is poorly supported at the moment.
The resulting Harpoon proof script that is generated by interactive proving will not contain the renaming, and this could lead to accidental variable capture.
Renames a variable. Use rename meta SRC DST
to rename a metavariable and
rename comp SRC DST
to rename a program variable.
toggle-automation
¶
Use toggle-automation AUTO [STATE]
to change the state of proof automation
features. See Proof automation for available values for AUTO
.
Valid values for STATE
are on
, off
, and toggle
. If unspecified,
STATE
defaults to toggle
.
Proof tactics¶
intros
¶
Use intros [NAME...]
to introduce assumptions into the context.
Restrictions:
- The current goal type is either a simple or dependent function type.
For Pi-types, the name of the assumption matches the name used in the Pi. For arrow-types, names will be taken from the given list of names, in order. If no names are given explicitly, then names are automatically generated.
On success, this tactic will replace the current subgoal with a new subgoal in which the assumptions are in the context.
Note
It is uncommon to use this tactic directly due to automation.
split
¶
Use split EXP
to perform case analysis on the synthesizable expression EXP
.
Restrictions:
- The expression
EXP
and its synthesized type may not contain uninstantiated metavariables.
On success, this tactic removes the current subgoal and introduces a new subgoal
for every possible constructor for EXP
.
msplit
¶
Use msplit MVAR
to perform case analysis on the metavariable MVAR
.
This command is syntactic sugar for split [_ |- MVAR]
.
invert
¶
Use invert EXP
to perform inversion on the synthesizable expression
EXP
.
This is the same as using split EXP
, but invert
will check that a unique
case is produced.
impossible
¶
Use impossible EXP
to eliminate the uninhabited type of the synthesizable
expression EXP
.
This is the same as using split EXP
, but impossible
will check that zero
cases are produced.
by
¶
Use by EXP as VAR [MODIFIER]
to invoke a lemma or induction hypothesis
represented by the synthesizable expression EXP
and bind the result to the
name VAR
.
The optional parameter MODIFIER
specifies at what level the binding occurs.
Valid values for MODIFIER
are
boxed
(default): the binding is made as a computational variable.unboxed
: the binding is made as a metavariable.strengthened
: the binding is made as a metavariable, and its context is strengthened according to LF Subordination.
Restrictions:
- The defined variable
VAR
must not already be in scope. EXP
and its synthesized type may not contain uninstantiated metavariables.- (For
unboxed
andstrengthened
only.) The synthesized type must be a boxed contextual object.
On success, this tactic replaces the current subgoal with a subgoal having one additional entry in the appropriate context.
Tip
LF terms whose contexts contain blocks are not in principle eligible for
strengthening. But such a context is equivalent to a flat context, and
Beluga will automatically flatten any blocks when strengthening.
Therefore, strengthened
has a secondary use for flattening.
strengthen
¶
The command strengthen EXP as X
is syntactic sugar for by EXP as X
strengthened
.
See also by.
solve
¶
Use solve EXP
to complete the proof by providing an explicit checkable
expression EXP
.
Restrictions:
- The expression
EXP
must check against the current subgoal’s type.
On success, this tactic removes the current subgoal, introducing no new subgoals.
suffices
¶
Use suffices by EXP toshow TAU...
to reason backwards via the synthesizable
expression EXP
by constructing proofs for each type annotation TAU
.
This command captures the common situation when a lemma or computational constructor can be used to complete a proof, because its conclusion is (unifiable with) the subgoal’s type. In this case, it suffices to construct the arguments to the lemma or constructor.
The main restriction on suffices
is that the expression EXP
must
synthesize a type of the form
{X1 : U1} ... {Xn : Un} tau_1 -> ... -> tau_k -> tau
Thankfully, this is the most common form of type one sees when working with Beluga.
Restrictions:
- The expression
EXP
must synthesize a compatible type, as above. - Its target type
tau
must unify with the current goal type. - Each type
tau_i
must unify with thei
th type annotation given in the command. - After unification, there must remain no uninstantiated metavariables.
Tip
Sometimes, not all the type annotations are necesary to pin down the
instantiations for the Pi-bound metavariables.
Instead of a type, you can use _
to indicate that this type annotation
should be uniquely inferrable given the goal type and the other specified
annotations. It is not uncommon to use suffices by i toshow _
.
Tip
suffices
eliminates both explicit and implicit leading Pi-types via
unification. It can sometimes be simpler to manually eliminate leading
explicit Pi-types via partial application:
suffices by i [C] ... toshow ...
.
When explicit Pi-types are manually eliminated, the need for a full type
annotation is less common.
On success, one subgoal is generated for each tau_i
, and the current subgoal
is removed.
In principle, this command is redundant with solve
because one could just
write solve EXP
to invoke the lemma directly, but this can be quite
unwieldy if the arguments to the lemma are complicated. Furthermore, the
arguments would need to be written as Beluga terms rather than interactively
constructed.
Note
The user-provided type annotations TAU...
are allowed to refer to
metavariables marked (not in scope)
.
However, it is an error if an out-of-scope metavariable appears in the
instantiation for an explicitly Pi-bound metavariable.
actions capabilities.
- Current limitations:
- no paramater variables
- no substitution variables
- no case splits (>1 case produced)
- no pair type
- no splitting on contexts
auto-invert-solve
¶
This automation attempts to solve the subgoal if no variable splitting (other than inversions) is required to solve
the goal. It performs 2 iterations of depth-first proof-search, once on the computation level, and
once again on the LF level. Use auto-invert-solve INT
to specify the maximum depth
you want your search tree to reach. Depth is incremented when we attempt to
solve a subgoal.
For example, if we want to solve Ev [|- S (S (S (S z)))]
this would require
a depth bound of at least 2::
inductive Ev : [⊢ nat] → ctype =
| ZEv : Ev [⊢ z]
| SEv : Ev [⊢ N] → Ev [⊢ S (S N)]
depth = 0
solve for Ev [|- S (S (S (S z)))] -> focus on SEv --->
depth = 1
solve for Ev [|- S (S z)] -> focus on SEv --->
depth = 2
solve for Ev [|- z] -> focus on zEv
Note: If a goal has more than one subgoal, depth only increments by 1.
For example, if we want to solve ``Less_Than [|- S z] [|- S (S (S z))]`` this
would require depth bound of 3:
inductive Less_Than : [⊢ nat] → [⊢ nat] → ctype =
| ZLT : Less_Than [⊢ z] [⊢ S N]
| LT : Less_Than [⊢ N] [⊢ M] → Less_Than [⊢ S N] [⊢ S M]
| Trans_LT : Less_Than [⊢ N] [⊢ M]
→ Less_Than [⊢ M] [⊢ K] → Less_Than [⊢ N] [⊢ K]
depth = 0
solve for Less_Than [|- S z] [|- S (S (S z))] -> focus on Trans_LT --->
depth = 1
solve for Less_Than [|- M] [|- S (S (S z))] -> focus on LT --->
depth = 2
solve for Less_Than [|- M'] [|- S (S z)] -> focus on LT --->
depth = 3
solve for Less_Than [|- M''] [|- S z] -> focus on ZLT
---> found LT LT ZLT : Less_Than [|- S (S z)] [|- S (S (S z))]
depth = 1
solve for Less_Than [|- S z] [|- S (S z)] -> focus on LT --->
depth = 2
solve for Less_Than [|- z] [|- S z] -> focus on ZLT
---> found LT ZLT : Less_Than [|- S z] [|- S (S z)]
-> found Trans_LT (LT ZLT) (LT LT ZLT) : Less_Than [|- S z] [|- S (S (S z))]
inductive-auto-solve
¶
This automation will perform a case split on the user-specified variable then call auto-invert-solve on each sub case. Use inductive-auto-solve INT
to specify the maximum depth you want your search tree to reach. Depth is incremented as above.