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}.