.. _interactive-reference: Interactive Command Reference ============================= .. contents:: :local: :depth: 2 .. _administrative commands: 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 :ref:`proof tactic `. See :ref:`undo`. ``redo`` ^^^^^^^^ Undoes the effect of a previous ``undo``. See :ref:`undo`. ``history`` ^^^^^^^^^^^ Displays the ``undo`` history. See :ref:`undo`. .. _cmd-theorem: ``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 :ref:`cmd-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. .. _cmd-session-list: ``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 :ref:`cmd-select` for a more flexible way to select a theorem. ``session create`` ^^^^^^^^^^^^^^^^^^ Creates a new session. This command will start the :ref:`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. .. _note:: This will drop the current undo history. ``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. .. _cmd-select: ``select`` ^^^^^^^^^^ ``select NAME`` selects a theorem by name for proving. See the :ref:`session list ` command. .. note:: When selecting a theorem from another session, be aware of the consequences this has on scoping. See :ref:`changing sessions`. .. _cmd-rename: ``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. .. _cmd-toggle-automation: ``toggle-automation`` ^^^^^^^^^^^^^^^^^^^^^ Use ``toggle-automation AUTO [STATE]`` to change the state of proof automation features. See :ref:`Proof automation` for available values for ``AUTO``. Valid values for ``STATE`` are ``on``, ``off``, and ``toggle``. If unspecified, ``STATE`` defaults to ``toggle``. .. _cmd-type: ``type`` ^^^^^^^^ Use ``type EXP`` to display the computed type of the given synthesizable expression ``EXP``. .. _cmd-info: ``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: Proof tactics ------------- .. _cmd-intros: ``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 :ref:`automation `. .. _cmd-split: ``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``. .. _cmd-msplit: ``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. .. _cmd-by: ``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 :ref:`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. .. _cmd-unbox: ``unbox`` ^^^^^^^^^ The command ``unbox EXP as X`` is syntactic sugar for ``by EXP as X unboxed``. See also :ref:`by `. .. _cmd-strengthen: ``strengthen`` ^^^^^^^^^^^^^^ The command ``strengthen EXP as X`` is syntactic sugar for ``by EXP as X strengthened``. See also :ref:`by `. .. _cmd-solve: ``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. .. _cmd-suffices: ``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 .. code-block:: Beluga {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. -------------------------------------------------------------------------------- The following actions make use of the proof search loop ``cgSolve`` in ``src/core/logic.ml``. Therefore, as it's capabilites improve, so too should the documentation on these 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: ``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: ``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.