Library Stdlib.Logic.WKL
A constructive proof of a version of Weak König's Lemma over a
decidable predicate in the formulation of which infinite paths are
treated as predicates. The representation of paths as relations
avoid the need for classical logic and unique choice. The
decidability condition is sufficient to ensure that some required
instance of double negation for disjunction of finite paths holds.
The idea of the proof comes from the proof of the weak König's
lemma from separation in second-order arithmetic.
Notice that we do not start from a tree but just from an arbitrary
predicate. Original Weak Konig's Lemma is the instantiation of
the lemma to a tree
is_path_from P n l means that there exists a path of length n
from l on which P does not hold
Inductive is_path_from (P:list bool -> Prop) : nat -> list bool -> Prop :=
| here l : ~ P l -> is_path_from P 0 l
| next_left l n : ~ P l -> is_path_from P n (true::l) -> is_path_from P (S n) l
| next_right l n : ~ P l -> is_path_from P n (false::l) -> is_path_from P (S n) l.
We give the characterization of is_path_from in terms of a more common arithmetical formula
Proposition is_path_from_characterization P n l :
is_path_from P n l <-> exists l', length l' = n /\ forall n', n'<=n -> ~ P (rev (firstn n' l') ++ l).
infinite_from P l means that we can find arbitrary long paths
along which P does not hold above l
has_infinite_path P means that there is an infinite path
(represented as a predicate) along which P does not hold at all
Definition has_infinite_path (P:list bool -> Prop) :=
exists (X:nat -> Prop), forall l, approx X l -> ~ P l.
inductively_barred_at P n l means that P eventually holds above
l after at most n steps upwards
Inductive inductively_barred_at (P:list bool -> Prop) : nat -> list bool -> Prop :=
| now_at l n : P l -> inductively_barred_at P n l
| propagate_at l n :
inductively_barred_at P n (true::l) ->
inductively_barred_at P n (false::l) ->
inductively_barred_at P (S n) l.
The proof proceeds by building a set Y of finite paths
approximating either the smallest unbarred infinite path in P, if
there is one (taking true>false), or the path
true::true::... if P happens to be inductively_barred
Fixpoint Y P (l:list bool) :=
match l with
| [] => True
| b::l =>
Y P l /\
if b then exists n, inductively_barred_at P n (false::l) else infinite_from P (false::l)
end.
Require Import Compare_dec.
Lemma is_path_from_restrict : forall P n n' l, n <= n' ->
is_path_from P n' l -> is_path_from P n l.
Lemma inductively_barred_at_monotone : forall P l n n', n' <= n ->
inductively_barred_at P n' l -> inductively_barred_at P n l.
Definition demorgan_or (P:list bool -> Prop) l l' := ~ (P l /\ P l') -> ~ P l \/ ~ P l'.
Definition demorgan_inductively_barred_at P :=
forall n l, demorgan_or (inductively_barred_at P n) (true::l) (false::l).
Lemma inductively_barred_at_imp_is_path_from :
forall P, demorgan_inductively_barred_at P -> forall n l,
~ inductively_barred_at P n l -> is_path_from P n l.
Lemma is_path_from_imp_inductively_barred_at : forall P n l,
is_path_from P n l -> inductively_barred_at P n l -> False.
Lemma find_left_path : forall P l n,
is_path_from P (S n) l -> inductively_barred_at P n (false :: l) -> is_path_from P n (true :: l).
Lemma Y_unique : forall P, demorgan_inductively_barred_at P ->
forall l1 l2, length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2.
X is the translation of Y as a predicate
Definition X P n := exists l, length l = n /\ Y P (true::l).
Lemma Y_approx : forall P, demorgan_inductively_barred_at P ->
forall l, approx (X P) l -> Y P l.
Main theorem
Theorem PreWeakKonigsLemma : forall P,
demorgan_inductively_barred_at P -> infinite_from P [] -> has_infinite_path P.
Lemma inductively_barred_at_decidable :
forall P, (forall l, P l \/ ~ P l) -> forall n l, inductively_barred_at P n l \/ ~ inductively_barred_at P n l.
Lemma inductively_barred_at_is_path_from_decidable :
forall P, (forall l, P l \/ ~ P l) -> demorgan_inductively_barred_at P.
Main corollary