Back to the main documentation of CtCoq
In this page, we present a tool that uses the mouse to quicken some frequent operations on mathematical formulas. This tool uses a paradigm of object dragging to replace expressions by provably equivalent formulas, using the Coq command Rewrite. We give an overview of its use, with a short example, and we show how this mechanism can be adapted to the mathematical domain of your choice. This parametrisation uses behavior rules, we will show how these rules can be obtained from certain classes of theorems and how these rules can also be edited manually.
To perform rewriting in CtCoq, users must normally construct a Rewrite command where they must provide a theorem, the parameters for its instantiation, and the position where the rewriting occurs. In the tool we present here, these three kinds of parameters are determined simply when the user "drags" an expression with the mouse, by clicking on it, moving the mouse, and releasing the button (with the <Ctrl> key depressed and the left button of the mouse). The drag movement can convey some intuitive information, when the replacement has the effect of moving one piece of data from one place to the other.
In general, the drag movement is used to express one of several kinds of operations:
In this example, an arrow appears when the user is depressing the left button of the mouse while also depressing the <Ctrl> key of the keyboard. The pink and green colors appear in the normal behavior of the tool. They give some visual feedback to the user.
This animation shows four actions provoked by the user. The first one permutes two instances of x and y, the second one cancels the expression z - z, the third one cancels a neutral element, and the fourth one permutes two other expressions. Each of these actions would actually produce a command to insert in the Command window and, when the Auto do-it flag is on, this command would be directly executed, giving a result very close in speed to this animation.
We give here the list of all the theorems that can be triggered by the default behavior of our drag-and-drop mechanism.
We have devised a language of drag-and-drop behavior rules, where each possible reaction performed by the drag-and-drop tool is described by a separate behavior rule. To ensure the validity of each operation, each rule rests on a rewriting theorem whose proof should be done separately. Behavior rules can be edited manually, using an interactive editor. We also provide automatic tools that directly infer simple behavior patterns from the form of rewriting theorem statements, when these theorems belong to well known classes of theorems.