搜索可判定谓词的反示例

Question

下面的Coq陈述应该是建设性的：

Require Import Decidable.

Lemma dec_search_nat_counterexample (P : nat -> Prop) (decH : forall i, decidable (P i))
  : (~ (forall i, P i)) -> exists i, ~ P i.

如果有一个上限，我希望能够显示某种形式的东西“假设不是每个i < N都满足P i，那么就有一个i < N ~ P i”。实际上，您可以编写一个函数，通过从零开始搜索来找到一个最小的示例。

当然，最初的声明没有上限，但我觉得应该有一个归纳性的论点，从上面有界的版本得到。但我不够聪明，不知道怎么做！我错过了一个聪明的诡计吗？或者说，尽管自然数的有序性很好，但这是否有根本的原因不能奏效呢？

Answer 1

在Meven -Bertrand的评论之后重新编写了答案

此语句等价于交换了马尔可夫原理和P和~P。由于P是可判定的，所以我们有P <-> (~ ~ P)，因此可以进行替换。

本文(http://pauillac.inria.fr/~herbelin/articles/lics-Her10-markov.pdf)认为马尔可夫原理在Coq中是不可证明的，因为作者(Coq的作者之一)提出了一种新的逻辑，它允许证明马尔可夫原理。

旧答案：

这在道德上是“全能的有限原则”-- LPO (见全科)。它需要经典公理来证明它的Coq -或者你断言自己是一个公理。

例如，见：

Require Import Coquelicot.Markov.

Check LPO.

Print Assumptions LPO.

因为它没有标准的库版本。