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

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

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

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 Le Lt.

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
Main corollary

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