The aim of this page is to give the basic information to extend the drag-and-drop algorithm to address the mathematical domain of your choice. We describe the basic elements of behavior descriptions drag-and-drop rules. In other pages, we describes the tools provided to add new rules: an interactive editor and an automatic tool to construct the natural rules for some general classes of theorems.

When a drag-and-drop action is requested, the algorithm determines the
position where the action is requested from the two positions where
the mouse is depressed and released (with the standard settings, these
positions appear in pink and green). These positions gives a tree
structure which is successively matched against the rules given in a
collection. When this matching succeeds, a command is generated by
completing a command template coming from the rule with data coming
from the designated position. When necessary, a Coq `Pattern`
command is added in front of the command, to make sure that the
rewriting will occur only at the position designated by the user. To
understand how the matching happens, you need to know a little more
about the structure of formulas in CtCoq.

Each drag-and-drop behavior rule comes with the following kinds of data:

- A tree pattern (you can have more information on trees and patterns below).
- An initial path and a final path (you can have more information on paths below), paths are lists of integers.
- A depth degree (more on this below), this is a positive integer.

- find the least common ancestor,
- move up a number of steps given by the depth degree,
- match this position with the rule's pattern, and
- check the two paths against the initial and final path from the rule.

The formulas manipulated when performing rewriting are mostly restricted
to identifiers and functions applied to formulas. Thus, almost all
the structures we shall consider in this presentation we be composed
with only two basic patterns: identifiers (operator `ident`) and
applications of functions to non empty lists of arguments
(operators `appc` and `formula_ne_list`). For instance,
the expression "(x + y) * z" will be represented by the tree-like
structure given in figure 1:

**Figure 1.
*** The tree structure of a mathematical expression*

Trees with `appc` as head operator always have two children,
where the first one is the function and the second is the list of
arguments. Trees with `formula_ne_list` as head operator
can have an arbitrary number of children, but at least one. Trees
with `ident` as head operator do not have any children, they
simply carry a value which is a name.

The positions in tree structures are designated using paths, which are lists of integers. The first integer represent the rank of the branch you should follow to go from the root of the term towards the designated position. The rest of the list can be interpreted similarly, but taking the corresponding subterm as the new root. For instance, the identifier "x" is designated by the path "(2 1 2 1)", while the identifier "plus" is designated by the path "(2 1 1)".

Patterns are constructed like trees, except that they use an extra
kind of operators `meta` to represent variables that can be
instanciated with arbitrary tree structures (`meta` stands for
"meta-variables" to distinguish these from the variables occurring in
mathematical formulas, represented by the operator "ident"). For instance,
figure 2 gives a pattern that can match the expression "(x + y)" (the
sub-expression at path "(2 1)" in our example tree).

**Figure 2.*** A tree pattern*

The meta-variables in patterns have names and these names are significant. A meta-variable with the same name occurring at two different positions indicates that the corresponding subterms of the matched tree have to be equal. The names will also be significant to designate data from the matched tree, when transferring data to the constructed command.

For the drag-and-drop rule to be eligible, it is necessary that an ancestor of the positions given by the user "match" the patterns and positions given in the rule.

From the two positions given by the movement of the user, the
algorithm then determines the
*least common ancestor*, by looking
only at the paths, for instance if the two positions are "x" and "y",
with paths "(2 1 2 1)" "(2 1 2 2)" the least common ancestor is also
designated by the longest common prefix of the two paths : "(2 1 2)".
Very often, the expression that is matched against the pattern given
in the drag-and-drop behavior rule is not the least common ancestor,
but one of its ancestors, at a distance also recorded in the rule. This
is necessary to recognize movements that are not "wide" enough to
make sure that the least common ancestor is an ancestor for all the
relevant data. For instance, suppose we want to provoke a rewriting
with the commutativity of addition when dragging from "x" to "y" in
the expression "x + y". In this case, the least common ancestor to
"x" and "y" is the structure with "formula_ne_list" as head operator,
the structure designated by the path "(2 1 2)", but this structure does
not contain the "plus" operator.

Once the pattern matching between the designated position and the rule's pattern succeeds, it is necessary to check that the two positions given by the user's movement also match the initial and last position given in the rule. For positions, matching is represented by the prefix ordering on paths. If "p1" is the path that designates the position where the user pushed down the button of the mouse, and "p2" is the path that designates the position where the user released the mouse, if "Pi" and "Pf" are the paths recorded in the rule as initial path and final path, and if "p" is the path to the common ancestor that is matched against the rule pattern, then the algorithms checks that "p + Pi" is a prefix of "p1" and "p + Pf" is a prefix of "p2".

The command pattern is just another pattern like the one used to match the designated position. Here, meta-variable names are used to designate the expressions found in the designated position. For instance, if the user moved the mouse from "x" to "y" in figure 1 and the rule associates the pattern given in figure 2 and the pattern command given in figure 3, then the generated command will be "Rewrite (plus_commutative x y)".

**Figure 3.*** A command pattern.*

To complete the command pattern, the tool simply applies to this pattern a substitution obtained during the matching phase. In this respect, the name of variables as they appear in the formula pattern and in the command pattern is very significant.

We provide a procedure to add new theorems in the database. To use
this procedure, select a theorem in the **Theorems**
window or a **Library** window, type
`Escape-x`, then at the prompt type the string
"add-in-dad-patterns". This procedure recognizes only some
classes of theorems, and associates a specific behavior to each class.
Here is a description of the classes:

- Cancellation theorems
- Cancellation theorems have a conclusion of the form "x - x = m", where the operator "-" and the result "m" can vary. The drag-and-drop behavior associated to this kind of theorem is triggered when one selects one of the x's and drags to the other. The intuitive meaning is to combine the two instances of x.
- "zero" theorems
- Zero theorems have a conclusion of the form "x + 0 = m", "0 + x = m", where the operator "+" and the result "m" can vary (for instance the operator can be the multiplcation operator and m can be "0"). The drag-and-drop behavior associated to this kind of theorem is triggered when one selects the "0" and drags to the operator "+". The intuitive meaning is to combine the "0" with the operation for which it has a special meaning.
- Factorisation theorems
- Factorization theorems have a conclusion of the form ""(x * y) +
(z * y) = (x ^ z) @ y", where the opérators "^" and "@"
do not necessarily have to be the same as "*" and "+". Two
drag-and-drop behaviors are associated to these kinds of theorems, corresponding
to rewritings in both directions.
- If one finds an instance of "(x * y) + (z * y) " and the user selects one of the y's and drags to the "+" operator, this instance is replaced by the corresponding instance of "(x ^ z) @ y". The intuitive meaning is to drag the y's up the expression structure.
- If one finds an instance of "(x ^ z) @ y" and the user selects the y and drags it to the "x" or the "z", this instance is replaced by the corresponding instance of "(x * y) + (z * y) ". The intuitive meaning is to distribute the y to the arguments of the "^" operator.

- Commutativity theorems
- Commutativity theorems have a conclusion of the form "x + y = y ^ x" where the operator "^" does not necessarily have to be the same as "+", the drag-and-drop behavior associated to this kind of theorem is triggered when one selects x or y in an instance of the left-hand side or the right-hand side of the theorem and drags to the other argument.

Yves Bertot Last modified: Mon Feb 10 16:31:26 MET