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 trad…

This is very cool. Russell did something similar, but at lower resolution, using the Coq notation system. With @gares we then made a quick hack to do a hi-res version. Russell O’Connor. A Computer Verified Theory of Compact Sets. SCSS 2008, RISC-Linz Report Series 08–08: 148–162, Jul 2008, Proceed…

This is definitely a big step forward towards having a general purpose CAS in Coq and will likely solve many plotting problems I had in the past! I will share some examples of what can go wrong with common math tools … It will be interesting to see what happens in the presence of rounded arithmetic…

[image] spitters: Russell O’Connor. A Computer Verified Theory of Compact Sets. SCSS 2008, RISC-Linz Report Series 08–08: 148–162, Jul 2008, Proceedings I did not know about this paper. Thanks a lot. There is a small difference in the notion of correctness. I guarantee that, if the function …

[image] MSoegtrop: It will be interesting to see what happens in the presence of rounded arithmetic e.g. with Zfloor. You will get some ugly staircases. (That is why I do not want to guarantee anything about completeness.) Plot ltac:(plot (fun x => IZR (Zfloor x)) (-4) 4). [floor]

This plotting function is very nice indeed. The specification of correctness of the graphs is slightly different between Coq interval and CoRN, but both are visually faithful. Both will show the singularities and problems of the plots. For instance, if you have very narrow spikes in the actual funct…

[image] VincentSe: if you have very narrow spikes in the actual function, those spikes will appear in the plots (instead of being lost because of the 64-bit precision). That is a misconception. More often than not, precision will have absolutely no impact on whether spikes will appear or not.…

I agree that Coq interval is easier to use when it understands the function to plot. But we need solutions for the other functions, those outside Coq interval’s syntax. I have been thinking to implement piecewise uniformly continuous functions in CoRN, to vary the density of sampling in different p…

[image] VincentSe: a gigantic modulus of continuity like in your exp(-x*x) example What do you mean “gigantic”? The modulus of continuity is 0.86. Even the cosine function has a larger modulus of continuity. exp (-x*x) is a very well behaved function. [image] VincentSe: to vary the densi…

Since I wrote about cosine, I might just as well put the pictures. Guess which one is correct, and which one was obtained with a computer algebra system. Time Plot ltac:(plot (fun x => cos x) (-1000) 1000 (-2) 2). (* Finished transaction in 0.218 secs (0.217u,0.s) (successful) *) [cos_bad] [cos_g…

Multiply the modulus of continuity 0.86 by the plot ratio 2000 / 1.6, it warns you that the plot has narrow spikes. It also warns you that the plot might not tell you much, as your next cosine example shows :slight_smile: By the way, many real-world functions have no closed-form. They are rather de…

Interval 4.2, now with plotting

Announcements

siraben July 28, 2021, 6:08am 17

Switching the Nix expression to use gnuplot_qt works!

Topic		Replies	Views
CoqInterval 4.0 released Announcements	0	901	June 17, 2020
Notes from the CoqPL 2024 Q/A session Miscellaneous meeting	9	641	January 29, 2024
[ANN] coq-lsp 0.1.9 Announcements serapi , coq-lsp , ui	0	222	May 31, 2024
Machine learning and hammers for Coq Using Rocq	45	7262	June 6, 2022
Alpha Announcement: Coq is a Lean Typechecker Announcements	7	12349	May 6, 2024

Interval 4.2, now with plotting

Related topics