Search code examples
coq

Equality on type which is not inductive type

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?

Solution

  • 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.