Hi everyone:
I am designing some functions about R type in the Coq standard library Coq.Reals.
I’m so sad that I can’t find/write a function to calculate equality of two Real numbers.
code detail (under Coq 8.13):
From Coq Require Import Reals RMicromega RingMicromega.
Open Scope R_scope.
(* find any boolearn function )
Search (R → R → bool). ( found this:
Reval_bop2: Op2 → R → R → bool
*)
Eval compute in Reval_bop2 OpEq R1 R1. (*
= if Req_EM_T R1 R1 then true else false
: bool *)
Eval compute in Reval_bop2 OpEq 1 2. (*
= if Req_EM_T R1 (R1 + R1) then true else false
: bool *)
so, I cannot get a boolean result. I only get an expression! but this is too long.
If anybody could help me, or could explain why Coq refused to calculate the boolean result?
Thank you very much!
Numbers come in a variety of types, with increasing complexity. the first layers are constructed in a finite way, and therefore there exist algorithms to compare them. Actually, Coq relies on the machinery of inductive types to describe them, and this where the algorithms get their ability to compute.
When it comes to the real numbers, the approach is different. It is explicitly stated that some numbers can be described by exhibiting a set and taking its upper bound. This includes an “infinite” point of view, which is beyond the capacity of algorithms. It has been shown that it is impossible to write an algorithm that takes as input two arbitrary real numbers, computes in a finite time, and returns a boolean value expressing when these two values are equal. The Coq system has to respect this impossibility.
Thank you very much. It really help me.