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).

Basic Behavior

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 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 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 Point and shoot extension

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.