Yes, the core supports exact rationals. This is easier to deal with in formal verification than floating point.
I made the UI snap to a fixed precision, such that its easy to reproduce special cases with overlapping edges, coinciding vertices etc. that make up much of the complexity of the algorithm.
In a past life i tried to implement Delaunay triangulation in floating point for data that can come in a rotated square grid. Normal precision doesn't work in that case. I learned a lot about arbitrary precision numbers doing that. The question about floats here gave me flashbacks.
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).
I think to do efficient formally verified geometry with floating point we would also need something like Shewchuk robust predicates. (I worked with them in the past to write robust software that is not formally verified. Did not read up, if there is a formally verified library for them.) Shewchuk robust predicates give certain consistency guarantees that are nice to have when implementing computational geometry with floating points and I think can be formalized.
It uses exact rational coordinates, not floating-point coordinates in the verified core. See: https://github.com/schildep/verified-polygon-intersection/bl...
Yes, the core supports exact rationals. This is easier to deal with in formal verification than floating point.
I made the UI snap to a fixed precision, such that its easy to reproduce special cases with overlapping edges, coinciding vertices etc. that make up much of the complexity of the algorithm.
In a past life i tried to implement Delaunay triangulation in floating point for data that can come in a rotated square grid. Normal precision doesn't work in that case. I learned a lot about arbitrary precision numbers doing that. The question about floats here gave me flashbacks.
I can relate. Working in floating point hardware design gave me an irrational distaste for it. The horrors!
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).
Thanks for the pointer, I will look into it.
I think to do efficient formally verified geometry with floating point we would also need something like Shewchuk robust predicates. (I worked with them in the past to write robust software that is not formally verified. Did not read up, if there is a formally verified library for them.) Shewchuk robust predicates give certain consistency guarantees that are nice to have when implementing computational geometry with floating points and I think can be formalized.