Plotting in a Formally Verified Way

TL;DR

This paper explores formal verification of function plots to ensure correctness, utilizing Coq proof assistant and polynomial approximations within the CoqInterval library to improve reliability.

Contribution

It introduces a method to formally verify the correctness of plots in computer algebra systems using Coq and polynomial approximations.

Findings

Verified plotting ensures accurate visual representations

Integration of formal methods into plotting libraries

Enhanced reliability of mathematical function visualizations

Abstract

An invaluable feature of computer algebra systems is their ability to plot the graph of functions. Unfortunately, when one is trying to design a library of mathematical functions, this feature often falls short, producing incorrect and potentially misleading plots, due to accuracy issues inherent to this use case. This paper investigates what it means for a plot to be correct and how to formally verify this property. The Coq proof assistant is then turned into a tool for plotting function graphs using reliable polynomial approximations. This feature is provided as part of the CoqInterval library.