The 4.2.0 release of Interval departs a bit from the previous versions in that it is no longer just about proving properties of real-valued expressions. It can now be used to investigate such properties visually, that is, it can now plot function graphs from inside Coq. The main difference with traditional computer algebra systems is that a plot is not a list of points obtained by sampling, it is a formal proof that the function passes only through filled pixels. So, no longer do you have to wonder whether a plot is actually faithful.
To do so, the library now provides a
plot tactic to generate the proof term of a function graph, and a
Plot command to display it using Gnuplot. Here is a simple example, with the corresponding screenshot. While the screenshot was obtained using Coqide, the
Plot command does not depend on the actual user interface and can even be used from
From Coq Require Import Reals. From Interval Require Import Plot Tactic. Open Scope R_scope. Definition p1 := ltac:(plot (fun x => x^2 * sin (x^2)) (-4) 4). Plot p1.