Cette page en Franšais
GeoView is a tool that combines the Coq theorem prover with the
dynamic geometry drawing tool GeoplanJ developed at CNAM.
GeoView is an extension of the user-interface Pcoq and is dedicated to the visualization of formal statements of plane geometrical theorems.
The statements of geometrical theorems and their proofs are
constructed and verified with Coq theorem prover.
A dynamic figure is automatically associated to mathematical formulas to show the meaning of these statements.
The figures generated with GeoView can be integrated as interactive and dynamic figures in HTML files using the GeoplanJ applet.
Here is an example of a statement dealing with homothety and collinearity (you can see other examples here).
And here is the dynamic figure generated by GeoView :
You can grab the free points (in green) by
pointing with the mouse and move them by dragging.
By double-clicking on the figure, you obtain a menu to create new objects (points, lines ...)
The real number k is displayed as a point on a straight line. You can change the value of k by moving this point.
GeoView is written in Java and has been integrated in the graphical interface Pcoq developed and maintained in the Lemme team at INRIA Sophia-Antipolis.