Library Coquelicot.Markov

This file is part of the Coquelicot formalization of real analysis in Coq:
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Require Import RIneq Rcomplements Omega.

This file proves the Limited Principle of Omniscience: given a decidable property P on nat, either P never holds or we can construct a witness for which P holds. Several variants are given.

Open Scope R_scope.

Limited Principle of Omniscience

Theorem LPO_min :
   P : natProp, ( n, P n ¬ P n) →
  {n : nat | P n i, (i < n)%nat¬ P i} + { n, ¬ P n}.

Theorem LPO :
   P : natProp, ( n, P n ¬ P n) →
  {n : nat | P n} + { n, ¬ P n}.

Lemma LPO_bool :
   f : natbool,
  {n | f n = true} + { n, f n = false}.


Lemma LPO_notforall : P : natProp, ( n, P n ¬P n) →
  (¬ n : nat, ¬ P n) → n : nat, P n.

Lemma LPO_notnotexists : P : natProp, ( n, P n ¬P n) →
  ~~ ( n : nat, P n) n : nat, P n.

Lemma LPO_ub_dec : (u : natR),
  {M : R | n, u n M} + { M : R, n, M < u n}.

Excluded-middle and decidability

Lemma EM_dec :
   P : Prop, {not (not P)} + {not P}.

Lemma EM_dec' :
   P : Prop, P not P{P} + {not P}.