coq - 实数公理中的排除中间

Question

使用 Coq 的实数公理completeness和total_order_T，使用与标准库引理中相同的技术Un_cv_crit_lub，我设法证明

Lemma NatForallDec : forall (f : nat -> bool),
    { forall n:nat, f n = false } + { ~forall n:nat, f n = false }.

和

Lemma NatForallDecIncr : forall (f : nat -> bool),
    (forall n m:nat, f n = true -> n <= m -> f m = true)
    -> { forall n:nat, f n = false } + { exists n:nat, f n = true }.

这令人不安，因为它看起来像某种预言：如果f关于自然数的命题对于每个数都是可判定的，那么 的无限合取也f变得可判定。所以实数公理说我们可以提取一种算法，它可以在有限的时间内做出无限多的决定......

是否还有其他来自实数公理且与实数无关的排中示例？

关于实数，最小上界可以实现为收敛序列吗？

Definition Cv_lub (A : R -> Prop) (l : R) (n : nat) :
  is_lub A l
  -> { x : R | A x /\ (l - x <= 1 / INR n)%R }.

标签： coq