I want to think about equality on real number in Coq.
But R in Coq.Reals.Reals. is not inductive type, so I can't define functions like Nat.eqb.
How do I define equality on real numbers in Coq?
Equality on type which is not inductive type
Viewed 77
1 Answers
The real numbers are axiomatized in Coq, and so is their equality operator:
Require Import Coq.Reals.Reals.
Check Req_EM_T.
(* forall r1 r2 : R, {r1 = r2} + {r1 <> r2} *)
The {r1 = r2} + {r1 <> r2} type is an informative boolean that gives you a proof of whether the two real numbers are equal.
Related