# 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`

and`strengthened`

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 the`i`

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.