I heard that Coq is using "Dedekind cut", but how's that related to floatpoint errors?

Can we just use something like

data Q : Type where
  div : N -> N -> Bool -> Q

To replace all usages of floatpoint numbers?


1 Answer 1


It depends on whether you want to "simply" reason about the properties of real numbers, or if you want to perform actual calculations.

If you want to prove things about their general properties, then using Dedekind cuts is feasible.

If you want to compute actual numerical things, then you need a numerical representation of the cut, and then you're back to some computable representation of (some of) the reals (you can't get all of them). It doesn't strictly have to be floating point numbers - you could use arbitrary precision arithmetic for example - more accurate but slower in general.

Your type however seems to be aiming to represent the Rationals, for which floating point numbers are unnecessary, you could just have a type with one constructor: nat -> nat -> Q.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.