In this page, you will find information on mechanisms for generating commands that we call proof-by-pointing and drag-and-drop. If you want more information on the general principle of these tools you can retrieve our paper on this topic (this paper was published at TACS'94, Springer Verlag LLNCS 789, it is a 177k postscript file).

*Proof-by-pointing* enables users to forget about the script and the
command language and to construct the proof by working only on the logical
formulas in the goals and theorem statements. The basic principle of
proof-by-pointing is to enable the user to guide the proof assistant by simply
bringing selected expressions to the foreground. This tool deals only with the
basic logical connectives, "for all", "there exists", "and",
"or", "implies", "not", and with equality. When
the user selects a subexpression of a goal, a command is generated that has the
following characteristics:

- the command will work on that specific goal,
- if the user selected a sub-expression of a hypothesis then:
- if the hypothesis is a universally quantified formula, the command will
use an instance of this formula (the Coq tactic
`Generalize`with an application of the hypothesis to a given argument then`Intros`), - if the hypothesis is an existentially quantified formula, the command
generates a witness for this formula (the Coq tactic
`Elim`then`Intros`), - if the hypothesis is a conjunct, the command breaks this conjunct into
pieces and continues recursively on the hypothesis corresponding to the selected
expression (the Coq tactic
`Elim`then`Intros`), - if the hypothesis is a disjunct, the command generates the two subgoals
corresponding to both cases of the disjunct and continues recursively on the
subgoal corresponding to the selected expression (the Coq tactic
`LApply`), - if the hypothesis is an implication, the command generates a subgoal for
the lefthand side and attempts to prove the same subgoal using the righthand
side of the implication as extra hypothesis; the command continues recursively
on the sub-goal corresponding to the chosen expression (the Coq tactic
`Elim`then`Intro`), - if the hypothesis is a negation, the command attempts to prove the negated
formula (the Coq tactic
`Elim`),

- if the hypothesis is a universally quantified formula, the command will
use an instance of this formula (the Coq tactic
- if the user selected a sub-expression of the conclusion then:
- if the conclusion is a universally quantified formula, the command
attempts to prove that formula for an arbitrary constant (the Coq tactic
`Intro`), - if the conclusion is an existentially quantified formula, the command
attempts to prove the formula for a given witness (the Coq tactic
`Exists`), - if the conclusion is a conjunct, the command generates the two subgoals
and continues on the subgoal corresponding to the selected expression (the Coq
tactic
`Split`), - if the conclusion is a disjunct, the command attempts to prove the chosen
case (the Coq tactic
`Left`or`Right`), - if the conclusion is an implication, the command generates a subgoal where
a new hypothesis corresponds to the lefthand side of the implication and the
conclusion is the righthand side of the implication; the command continues
recursively on the new hypothesis or on the conclusion depending on the selected
expression (the Coq tactic
`Intro`), - if the conclusion is a negation, the command attempts to prove a
contradiction, using the negated formula as an hypothesis (the Coq tactic
`Unfold not`then`Intro`),

- if the conclusion is a universally quantified formula, the command
attempts to prove that formula for an arbitrary constant (the Coq tactic
- if the user directly selected the complete conclusion or a complete
assumption, then the command tries to prove the goal by assumption (the Coq
tactic
`Assumption`or`Exact`).

When the user selects a sub-expression of a universally quantified formula in a hypothesis or a sub-expression of an existentially quantified formula in the conclusion, a value must be given to the proof assistant. For this purpose, the proof-by-pointing tool generates incomplete commands that contain place-holders that have to be filled in. The name of the place-holder is usually related to the name of the bound variable in the quantified formula. If the user-interface refuses to perform a ``Do it'' action for a command generated by proof-by-pointing, it usually means that a place-holder has been left unfilled in that command. Filling in a place-holder is easily done using the copy-paste shortcut provided by the middle button of the mouse.

The result of `Check` or `Search` commands, when displayed
in the **Theorems** or **Library** windows, can also
be used for proof-by-pointing. These expressions can simply be viewed as
extensions of the hypotheses of goals.

The basic behavior of proof-by-pointing is to bring the selected expression
to the forefront and simply try to solve the produced goal by assumption. A
natural extension to this behavior is to replace this last try by the
application of a specific command. For instance, the user can use
proof-by-pointing to create a new assumption and simply apply this assumption
using the `Apply` command. The interface provides this kind of
behavior for several commands. To use it, it suffices to choose the relevant
expression with the left mouse button. Then the *shooting* function is
chosen either in the popup menu that appears when one depresses at the same time
the `<Ctrl>` key and the right mouse button, or by a
keyboard accelerator.

As a mnemonic, consider that the user aims at the target with his left
finger and then chooses the device. This is the explanation for the name *point-and-shoot*.
This feature simply enables the user to combine proof-by-pointing and apply
specific commands as a shortcut. The various possibilities for point-and-shoot
and their keyboard accelerators are:

`a`.*point and*`Apply`.- When the selected expression can be transformed into an assumption, the
generated command is a combination of proof-by-pointing and
`Apply`on that assumption. The`Apply`pattern that is generated takes into account the form of that specific assumption. For example, it generates place holders to provide values for the universally quantified formulas that will not be instanciated by the`Apply`command. When the selected expression cannot be transformed into an assumption, it simply tries to solve the corresponding goal by assumption. `e`.*point and*.`Elim`- When the selected expression can be transformed into an assumption, the
generated command combines proof-by-pointing and
`Elim`on that assumption. Here, the`Elim`pattern that is generated is dumb, and executing the command may generate uninstanciated meta-variables. `f`.*point and*.`Auto`(no key binding)- The generated command combines proof-by-pointing and
`Auto`. `g`.*point and*.`Generalize`- When the selected expression can be transformed into an assumption, the
generated command combines proof-by-pointing and
`Generalize`on that assumption. `i`.*point and*.`Injection`- The generated command combines proof-by-pointing and
`Injection`. Note that Injection is itself a command that uses a notion of paths and the system tries to generate a clever path for this command, depending how deep in the expression the user selected. `l`.*point and*.`Simpl`- The generated command combines proof-by-pointing and
`Simpl`on the conclusion or an assumption. `m`.*point and*.`Assumption`- This is the basic proof-by-pointing behavior.
`r`.*point and*.`Red`- The generated command combines proof-by-pointing and
`Red`on the selected expression. `w`.*point and*.`Rewrite`- When the selected expression can be transformed into an assumption and it
is an equality, then a
`Rewrite`command is generated that uses this equality. The direction of the rewriting is decided by the member of the equality that has been chosen. If you choose the left hand side then the`Rewrite ->`command is generated, if you choose the right hand side, then the`Rewrite <-`command is generated.