CODEWITHSUNDEEP
coq
Daisuke Sugawara
Daisuke Sugawara

Reputation: 321

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?

Upvotes: 3

Views: 99

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

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.

Upvotes: 2

Related Questions