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.

redo

Undoes the effect of a previous undo. See Undo.

history

Displays the undo history. 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.

save

This command is a shortcut for session serialize.

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.

type

Use type EXP to display the computed type of the given synthesizable expression EXP.

info

Use info KIND OBJ to get information on the KIND named OBJ.

Valid values for KIND are

  • theorem: displays information about the Beluga program or Harpoon proof named OBJ.

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.

unbox

The command unbox EXP as X is syntactic sugar for by EXP as X unboxed. See also by.

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.