This is a great use for AI! Calculating intersections is tedious and there are an surprising number of edge cases that are tedious to track down and fix.
I am eager for a lean equivalent of flocq in rocq. When I did some lean verification of numerical algorithms I did the same thing with rationals or the reals from mathlib. The big gap between that and the actual code is the lack of a solid theory library to pull in that would give me IEEE floats that is at the same level of quality as Flocq. I’m eager for that to come along (unless it has and I just haven’t found it yet).
This is a great use for AI! Calculating intersections is tedious and there are an surprising number of edge cases that are tedious to track down and fix.
Does this use integer coordinates or floating point coordinates?
It uses exact rational coordinates, not floating-point coordinates in the verified core. See: https://github.com/schildep/verified-polygon-intersection/bl...
I am eager for a lean equivalent of flocq in rocq. When I did some lean verification of numerical algorithms I did the same thing with rationals or the reals from mathlib. The big gap between that and the actual code is the lack of a solid theory library to pull in that would give me IEEE floats that is at the same level of quality as Flocq. I’m eager for that to come along (unless it has and I just haven’t found it yet).
Is the web demo compiled from the lean?