# Library Coquelicot.Markov

This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/
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.

Copyright (C) 2011-2015 Catherine Lelay

Copyright (C) 2011-2015 Guillaume Melquiond

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.

Theorem LPO_min :

∀ P : nat → Prop, (∀ n, P n ∨ ¬ P n) →

{n : nat | P n ∧ ∀ i, (i < n)%nat → ¬ P i} + {∀ n, ¬ P n}.

Theorem LPO :

∀ P : nat → Prop, (∀ n, P n ∨ ¬ P n) →

{n : nat | P n} + {∀ n, ¬ P n}.

Lemma LPO_bool :

∀ f : nat → bool,

{n | f n = true} + {∀ n, f n = false}.