Library Coq.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

Require Import WeakFan List.
Import ListNotations.

Require Import Arith.

is_path_from P n l means that there exists a path of length n from l on which P does not hold
We give the characterization of is_path_from in terms of a more common arithmetical formula
infinite_from P l means that we can find arbitrary long paths along which P does not hold above l

Definition infinite_from (P:list bool -> Prop) l := forall n, is_path_from P n 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
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
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
Main corollary

Corollary WeakKonigsLemma : forall P, (forall l, P l \/ ~ P l) ->
  infinite_from P [] -> has_infinite_path P.