coq - 非归纳类型的平等

Question

我想考虑 Coq 中实数的相等性。

但是RinCoq.Reals.Reals.不是归纳类型，所以我不能定义像Nat.eqb.

如何在 Coq 中定义实数的相等性？

标签： coq

Answer 1

实数在 Coq 中被公理化，它们的等式运算符也是如此：

Require Import Coq.Reals.Reals.

Check Req_EM_T.

(* forall r1 r2 : R, {r1 = r2} + {r1 <> r2} *)

该{r1 = r2} + {r1 <> r2}类型是一个信息丰富的布尔值，它可以证明两个实数是否相等。