WKL.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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).P:list bool -> Prop
n:nat
l:list bool
is_path_from P n l <->
(exists l' : list bool,
   length l' = n /\
   (forall n' : nat,
    n' <= n -> ~ P (rev (firstn n' l') ++ l)))
Proof.P:list bool -> Prop
n:nat
l:list bool
is_path_from P n l <->
(exists l' : list bool,
   length l' = n /\
   (forall n' : nat,
    n' <= n -> ~ P (rev (firstn n' l') ++ l)))
intros.P:list bool -> Prop
n:nat
l:list bool
is_path_from P n l <->
(exists l' : list bool,
   length l' = n /\
   (forall n' : nat,
    n' <= n -> ~ P (rev (firstn n' l') ++ l))) split.P:list bool -> Prop
n:nat
l:list bool
is_path_from P n l ->
exists l' : list bool,
  length l' = n /\
  (forall n' : nat,
   n' <= n -> ~ P (rev (firstn n' l') ++ l))
P:list bool -> Prop
n:nat
l:list bool
(exists l' : list bool,
   length l' = n /\
   (forall n' : nat,
    n' <= n -> ~ P (rev (firstn n' l') ++ l))) ->
is_path_from P n l
-P:list bool -> Prop
n:nat
l:list bool
is_path_from P n l ->
exists l' : list bool,
  length l' = n /\
  (forall n' : nat,
   n' <= n -> ~ P (rev (firstn n' l') ++ l)) induction 1 as [|* HP _ (l'&Hl'&HPl')|* HP _ (l'&Hl'&HPl')].P:list bool -> Prop
l:list bool
H:~ P l
exists l' : list bool,
  length l' = 0 /\
  (forall n' : nat,
   n' <= 0 -> ~ P (rev (firstn n' l') ++ l))
P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
exists l'0 : list bool,
  length l'0 = S n /\
  (forall n' : nat,
   n' <= S n -> ~ P (rev (firstn n' l'0) ++ l))
P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
exists l'0 : list bool,
  length l'0 = S n /\
  (forall n' : nat,
   n' <= S n -> ~ P (rev (firstn n' l'0) ++ l))
  +P:list bool -> Prop
l:list bool
H:~ P l
exists l' : list bool,
  length l' = 0 /\
  (forall n' : nat,
   n' <= 0 -> ~ P (rev (firstn n' l') ++ l)) exists [].P:list bool -> Prop
l:list bool
H:~ P l
length [] = 0 /\
(forall n' : nat,
 n' <= 0 -> ~ P (rev (firstn n' []) ++ l)) split.P:list bool -> Prop
l:list bool
H:~ P l
length [] = 0
P:list bool -> Prop
l:list bool
H:~ P l
forall n' : nat,
n' <= 0 -> ~ P (rev (firstn n' []) ++ l) reflexivity.P:list bool -> Prop
l:list bool
H:~ P l
forall n' : nat,
n' <= 0 -> ~ P (rev (firstn n' []) ++ l) intros n <-%le_n_0_eq.P:list bool -> Prop
l:list bool
H:~ P l
~ P (rev (firstn 0 []) ++ l) assumption.
  +P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
exists l'0 : list bool,
  length l'0 = S n /\
  (forall n' : nat,
   n' <= S n -> ~ P (rev (firstn n' l'0) ++ l)) exists (true :: l').P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
length (true :: l') = S n /\
(forall n' : nat,
 n' <= S n -> ~ P (rev (firstn n' (true :: l')) ++ l)) split.P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
length (true :: l') = S n
P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
forall n' : nat,
n' <= S n -> ~ P (rev (firstn n' (true :: l')) ++ l) apply eq_S, Hl'.P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
forall n' : nat,
n' <= S n -> ~ P (rev (firstn n' (true :: l')) ++ l) intros [|] H.P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
H:0 <= S n
~ P (rev (firstn 0 (true :: l')) ++ l)
P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
n0:nat
H:S n0 <= S n
~ P (rev (firstn (S n0) (true :: l')) ++ l)
    *P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
H:0 <= S n
~ P (rev (firstn 0 (true :: l')) ++ l) assumption.
    *P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
n0:nat
H:S n0 <= S n
~ P (rev (firstn (S n0) (true :: l')) ++ l) simpl.P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
n0:nat
H:S n0 <= S n
~ P ((rev (firstn n0 l') ++ [true]) ++ l) rewrite <- app_assoc.P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ true :: l)
n0:nat
H:S n0 <= S n
~ P (rev (firstn n0 l') ++ [true] ++ l) apply HPl', le_S_n, H.
  +P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
exists l'0 : list bool,
  length l'0 = S n /\
  (forall n' : nat,
   n' <= S n -> ~ P (rev (firstn n' l'0) ++ l)) exists (false :: l').P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
length (false :: l') = S n /\
(forall n' : nat,
 n' <= S n -> ~ P (rev (firstn n' (false :: l')) ++ l)) split.P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
length (false :: l') = S n
P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
forall n' : nat,
n' <= S n -> ~ P (rev (firstn n' (false :: l')) ++ l) apply eq_S, Hl'.P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
forall n' : nat,
n' <= S n -> ~ P (rev (firstn n' (false :: l')) ++ l) intros [|] H.P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
H:0 <= S n
~ P (rev (firstn 0 (false :: l')) ++ l)
P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
n0:nat
H:S n0 <= S n
~ P (rev (firstn (S n0) (false :: l')) ++ l)
    *P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
H:0 <= S n
~ P (rev (firstn 0 (false :: l')) ++ l) assumption.
    *P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
n0:nat
H:S n0 <= S n
~ P (rev (firstn (S n0) (false :: l')) ++ l) simpl.P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
n0:nat
H:S n0 <= S n
~ P ((rev (firstn n0 l') ++ [false]) ++ l) rewrite <- app_assoc.P:list bool -> Prop
l:list bool
n:nat
HP:~ P l
l':list bool
Hl':length l' = n
HPl':forall n' : nat,
n' <= n ->
~ P (rev (firstn n' l') ++ false :: l)
n0:nat
H:S n0 <= S n
~ P (rev (firstn n0 l') ++ [false] ++ l) apply HPl', le_S_n, H.
-P:list bool -> Prop
n:nat
l:list bool
(exists l' : list bool,
   length l' = n /\
   (forall n' : nat,
    n' <= n -> ~ P (rev (firstn n' l') ++ l))) ->
is_path_from P n l intros (l'& <- &HPl').P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length l' ->
~ P (rev (firstn n' l') ++ l)
is_path_from P (length l') l induction l' as [|[|]] in l, HPl' |- *.P:list bool -> Prop
l:list bool
HPl':forall n' : nat,
n' <= length [] ->
~ P (rev (firstn n' []) ++ l)
is_path_from P (length []) l
P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (true :: l') ->
~ P (rev (firstn n' (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
is_path_from P (length (true :: l')) l
P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (false :: l') ->
~ P (rev (firstn n' (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
is_path_from P (length (false :: l')) l
  +P:list bool -> Prop
l:list bool
HPl':forall n' : nat,
n' <= length [] ->
~ P (rev (firstn n' []) ++ l)
is_path_from P (length []) l constructor.P:list bool -> Prop
l:list bool
HPl':forall n' : nat,
n' <= length [] ->
~ P (rev (firstn n' []) ++ l)
~ P l apply (HPl' 0).P:list bool -> Prop
l:list bool
HPl':forall n' : nat,
n' <= length [] ->
~ P (rev (firstn n' []) ++ l)
0 <= length [] apply le_0_n.
  +P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (true :: l') ->
~ P (rev (firstn n' (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
is_path_from P (length (true :: l')) l eapply next_left.P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (true :: l') ->
~ P (rev (firstn n' (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
~ P l
P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (true :: l') ->
~ P (rev (firstn n' (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
is_path_from P
  ((fix length (l0 : list bool) : nat :=
      match l0 with
      | [] => 0
      | _ :: l'0 => S (length l'0)
      end) l') (true :: l)
    *P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (true :: l') ->
~ P (rev (firstn n' (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
~ P l apply (HPl' 0), le_0_n.
    *P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (true :: l') ->
~ P (rev (firstn n' (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
is_path_from P
  ((fix length (l0 : list bool) : nat :=
      match l0 with
      | [] => 0
      | _ :: l'0 => S (length l'0)
      end) l') (true :: l) fold (length l').P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (true :: l') ->
~ P (rev (firstn n' (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
is_path_from P (length l') (true :: l) apply IHl'.P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (true :: l') ->
~ P (rev (firstn n' (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
forall n' : nat,
n' <= length l' ->
~ P (rev (firstn n' l') ++ true :: l) intros n' H%le_n_S.P:list bool -> Prop
l, l':list bool
HPl':forall n'0 : nat,
n'0 <= length (true :: l') ->
~ P (rev (firstn n'0 (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n'0 : nat,
 n'0 <= length l' ->
 ~ P (rev (firstn n'0 l') ++ l0)) ->
is_path_from P (length l') l0
n':nat
H:S n' <= S (length l')
~ P (rev (firstn n' l') ++ true :: l) apply HPl' in H.P:list bool -> Prop
l, l':list bool
HPl':forall n'0 : nat,
n'0 <= length (true :: l') ->
~ P (rev (firstn n'0 (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n'0 : nat,
 n'0 <= length l' ->
 ~ P (rev (firstn n'0 l') ++ l0)) ->
is_path_from P (length l') l0
n':nat
H:~ P (rev (firstn (S n') (true :: l')) ++ l)
~ P (rev (firstn n' l') ++ true :: l) simpl in H.P:list bool -> Prop
l, l':list bool
HPl':forall n'0 : nat,
n'0 <= length (true :: l') ->
~ P (rev (firstn n'0 (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n'0 : nat,
 n'0 <= length l' ->
 ~ P (rev (firstn n'0 l') ++ l0)) ->
is_path_from P (length l') l0
n':nat
H:~ P ((rev (firstn n' l') ++ [true]) ++ l)
~ P (rev (firstn n' l') ++ true :: l) rewrite <- app_assoc in H.P:list bool -> Prop
l, l':list bool
HPl':forall n'0 : nat,
n'0 <= length (true :: l') ->
~ P (rev (firstn n'0 (true :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n'0 : nat,
 n'0 <= length l' ->
 ~ P (rev (firstn n'0 l') ++ l0)) ->
is_path_from P (length l') l0
n':nat
H:~ P (rev (firstn n' l') ++ [true] ++ l)
~ P (rev (firstn n' l') ++ true :: l) assumption.
  +P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (false :: l') ->
~ P (rev (firstn n' (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
is_path_from P (length (false :: l')) l apply next_right.P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (false :: l') ->
~ P (rev (firstn n' (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
~ P l
P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (false :: l') ->
~ P (rev (firstn n' (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
is_path_from P
  ((fix length (l0 : list bool) : nat :=
      match l0 with
      | [] => 0
      | _ :: l'0 => S (length l'0)
      end) l') (false :: l)
    *P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (false :: l') ->
~ P (rev (firstn n' (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
~ P l apply (HPl' 0), le_0_n.
    *P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (false :: l') ->
~ P (rev (firstn n' (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
is_path_from P
  ((fix length (l0 : list bool) : nat :=
      match l0 with
      | [] => 0
      | _ :: l'0 => S (length l'0)
      end) l') (false :: l) fold (length l').P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (false :: l') ->
~ P (rev (firstn n' (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
is_path_from P (length l') (false :: l) apply IHl'.P:list bool -> Prop
l, l':list bool
HPl':forall n' : nat,
n' <= length (false :: l') ->
~ P (rev (firstn n' (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n' : nat,
 n' <= length l' ->
 ~ P (rev (firstn n' l') ++ l0)) ->
is_path_from P (length l') l0
forall n' : nat,
n' <= length l' ->
~ P (rev (firstn n' l') ++ false :: l) intros n' H%le_n_S.P:list bool -> Prop
l, l':list bool
HPl':forall n'0 : nat,
n'0 <= length (false :: l') ->
~ P (rev (firstn n'0 (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n'0 : nat,
 n'0 <= length l' ->
 ~ P (rev (firstn n'0 l') ++ l0)) ->
is_path_from P (length l') l0
n':nat
H:S n' <= S (length l')
~ P (rev (firstn n' l') ++ false :: l) apply HPl' in H.P:list bool -> Prop
l, l':list bool
HPl':forall n'0 : nat,
n'0 <= length (false :: l') ->
~ P (rev (firstn n'0 (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n'0 : nat,
 n'0 <= length l' ->
 ~ P (rev (firstn n'0 l') ++ l0)) ->
is_path_from P (length l') l0
n':nat
H:~ P (rev (firstn (S n') (false :: l')) ++ l)
~ P (rev (firstn n' l') ++ false :: l) simpl in H.P:list bool -> Prop
l, l':list bool
HPl':forall n'0 : nat,
n'0 <= length (false :: l') ->
~ P (rev (firstn n'0 (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n'0 : nat,
 n'0 <= length l' ->
 ~ P (rev (firstn n'0 l') ++ l0)) ->
is_path_from P (length l') l0
n':nat
H:~ P ((rev (firstn n' l') ++ [false]) ++ l)
~ P (rev (firstn n' l') ++ false :: l) rewrite <- app_assoc in H.P:list bool -> Prop
l, l':list bool
HPl':forall n'0 : nat,
n'0 <= length (false :: l') ->
~ P (rev (firstn n'0 (false :: l')) ++ l)
IHl':forall l0 : list bool,
(forall n'0 : nat,
 n'0 <= length l' ->
 ~ P (rev (firstn n'0 l') ++ l0)) ->
is_path_from P (length l') l0
n':nat
H:~ P (rev (firstn n' l') ++ [false] ++ l)
~ P (rev (firstn n' l') ++ false :: l) assumption.
Qed.

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

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 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.forall (P : list bool -> Prop) (n n' : nat)
  (l : list bool),
n <= n' -> is_path_from P n' l -> is_path_from P n l
Proof.forall (P : list bool -> Prop) (n n' : nat)
  (l : list bool),
n <= n' -> is_path_from P n' l -> is_path_from P n l
intros * Hle H; induction H in n, Hle, H |- * ; intros.P:list bool -> Prop
n:nat
Hle:n <= 0
l:list bool
H:~ P l
is_path_from P n l
P:list bool -> Prop
n, n0:nat
Hle:n <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (true :: l)
IHis_path_from:forall n1 : nat,
n1 <= n0 ->
is_path_from P n1 (true :: l)
is_path_from P n l
P:list bool -> Prop
n, n0:nat
Hle:n <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (false :: l)
IHis_path_from:forall n1 : nat,
n1 <= n0 ->
is_path_from P n1 (false :: l)
is_path_from P n l
-P:list bool -> Prop
n:nat
Hle:n <= 0
l:list bool
H:~ P l
is_path_from P n l apply le_n_0_eq in Hle as <-.P:list bool -> Prop
l:list bool
H:~ P l
is_path_from P 0 l apply here.P:list bool -> Prop
l:list bool
H:~ P l
~ P l assumption.
-P:list bool -> Prop
n, n0:nat
Hle:n <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (true :: l)
IHis_path_from:forall n1 : nat,
n1 <= n0 ->
is_path_from P n1 (true :: l)
is_path_from P n l destruct n.P:list bool -> Prop
n0:nat
Hle:0 <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (true :: l)
IHis_path_from:forall n : nat,
n <= n0 ->
is_path_from P n (true :: l)
is_path_from P 0 l
P:list bool -> Prop
n, n0:nat
Hle:S n <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (true :: l)
IHis_path_from:forall n1 : nat,
n1 <= n0 ->
is_path_from P n1 (true :: l)
is_path_from P (S n) l
  +P:list bool -> Prop
n0:nat
Hle:0 <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (true :: l)
IHis_path_from:forall n : nat,
n <= n0 ->
is_path_from P n (true :: l)
is_path_from P 0 l apply here.P:list bool -> Prop
n0:nat
Hle:0 <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (true :: l)
IHis_path_from:forall n : nat,
n <= n0 ->
is_path_from P n (true :: l)
~ P l assumption.
  +P:list bool -> Prop
n, n0:nat
Hle:S n <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (true :: l)
IHis_path_from:forall n1 : nat,
n1 <= n0 ->
is_path_from P n1 (true :: l)
is_path_from P (S n) l apply next_left; auto using le_S_n.
-P:list bool -> Prop
n, n0:nat
Hle:n <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (false :: l)
IHis_path_from:forall n1 : nat,
n1 <= n0 ->
is_path_from P n1 (false :: l)
is_path_from P n l destruct n.P:list bool -> Prop
n0:nat
Hle:0 <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (false :: l)
IHis_path_from:forall n : nat,
n <= n0 ->
is_path_from P n (false :: l)
is_path_from P 0 l
P:list bool -> Prop
n, n0:nat
Hle:S n <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (false :: l)
IHis_path_from:forall n1 : nat,
n1 <= n0 ->
is_path_from P n1 (false :: l)
is_path_from P (S n) l
  +P:list bool -> Prop
n0:nat
Hle:0 <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (false :: l)
IHis_path_from:forall n : nat,
n <= n0 ->
is_path_from P n (false :: l)
is_path_from P 0 l apply here.P:list bool -> Prop
n0:nat
Hle:0 <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (false :: l)
IHis_path_from:forall n : nat,
n <= n0 ->
is_path_from P n (false :: l)
~ P l assumption.
  +P:list bool -> Prop
n, n0:nat
Hle:S n <= S n0
l:list bool
H:~ P l
H0:is_path_from P n0 (false :: l)
IHis_path_from:forall n1 : nat,
n1 <= n0 ->
is_path_from P n1 (false :: l)
is_path_from P (S n) l apply next_right; auto using le_S_n.
Qed.

Lemma inductively_barred_at_monotone : forall P l n n', n' <= n ->
  inductively_barred_at P n' l -> inductively_barred_at P n l.forall (P : list bool -> Prop) (l : list bool)
  (n n' : nat),
n' <= n ->
inductively_barred_at P n' l ->
inductively_barred_at P n l
Proof.forall (P : list bool -> Prop) (l : list bool)
  (n n' : nat),
n' <= n ->
inductively_barred_at P n' l ->
inductively_barred_at P n l
intros * Hle Hbar.P:list bool -> Prop
l:list bool
n, n':nat
Hle:n' <= n
Hbar:inductively_barred_at P n' l
inductively_barred_at P n l
induction Hbar in n, l, Hle, Hbar |- *.P:list bool -> Prop
n, n0:nat
Hle:n0 <= n
l:list bool
H:P l
inductively_barred_at P n l
P:list bool -> Prop
n, n0:nat
Hle:S n0 <= n
l:list bool
Hbar1:inductively_barred_at P n0 (true :: l)
Hbar2:inductively_barred_at P n0 (false :: l)
IHHbar1:forall n1 : nat,
n0 <= n1 ->
inductively_barred_at P n1 (true :: l)
IHHbar2:forall n1 : nat,
n0 <= n1 ->
inductively_barred_at P n1 (false :: l)
inductively_barred_at P n l
-P:list bool -> Prop
n, n0:nat
Hle:n0 <= n
l:list bool
H:P l
inductively_barred_at P n l apply now_at; auto.
-P:list bool -> Prop
n, n0:nat
Hle:S n0 <= n
l:list bool
Hbar1:inductively_barred_at P n0 (true :: l)
Hbar2:inductively_barred_at P n0 (false :: l)
IHHbar1:forall n1 : nat,
n0 <= n1 ->
inductively_barred_at P n1 (true :: l)
IHHbar2:forall n1 : nat,
n0 <= n1 ->
inductively_barred_at P n1 (false :: l)
inductively_barred_at P n l destruct n; [apply le_Sn_0 in Hle; contradiction|].P:list bool -> Prop
n, n0:nat
Hle:S n0 <= S n
l:list bool
Hbar1:inductively_barred_at P n0 (true :: l)
Hbar2:inductively_barred_at P n0 (false :: l)
IHHbar1:forall n1 : nat,
n0 <= n1 ->
inductively_barred_at P n1 (true :: l)
IHHbar2:forall n1 : nat,
n0 <= n1 ->
inductively_barred_at P n1 (false :: l)
inductively_barred_at P (S n) l
  apply le_S_n in Hle.P:list bool -> Prop
n, n0:nat
Hle:n0 <= n
l:list bool
Hbar1:inductively_barred_at P n0 (true :: l)
Hbar2:inductively_barred_at P n0 (false :: l)
IHHbar1:forall n1 : nat,
n0 <= n1 ->
inductively_barred_at P n1 (true :: l)
IHHbar2:forall n1 : nat,
n0 <= n1 ->
inductively_barred_at P n1 (false :: l)
inductively_barred_at P (S n) l
  apply propagate_at; auto.
Qed.

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.forall P : list bool -> Prop,
demorgan_inductively_barred_at P ->
forall (n : nat) (l : list bool),
~ inductively_barred_at P n l -> is_path_from P n l
Proof.forall P : list bool -> Prop,
demorgan_inductively_barred_at P ->
forall (n : nat) (l : list bool),
~ inductively_barred_at P n l -> is_path_from P n l
intros P Hdemorgan; induction n; intros l H.P:list bool -> Prop
Hdemorgan:demorgan_inductively_barred_at P
l:list bool
H:~ inductively_barred_at P 0 l
is_path_from P 0 l
P:list bool -> Prop
Hdemorgan:demorgan_inductively_barred_at P
n:nat
IHn:forall l0 : list bool,
~ inductively_barred_at P n l0 ->
is_path_from P n l0
l:list bool
H:~ inductively_barred_at P (S n) l
is_path_from P (S n) l
-P:list bool -> Prop
Hdemorgan:demorgan_inductively_barred_at P
l:list bool
H:~ inductively_barred_at P 0 l
is_path_from P 0 l apply here.P:list bool -> Prop
Hdemorgan:demorgan_inductively_barred_at P
l:list bool
H:~ inductively_barred_at P 0 l
~ P l
  intro.P:list bool -> Prop
Hdemorgan:demorgan_inductively_barred_at P
l:list bool
H:~ inductively_barred_at P 0 l
H0:P l
False apply H.P:list bool -> Prop
Hdemorgan:demorgan_inductively_barred_at P
l:list bool
H:~ inductively_barred_at P 0 l
H0:P l
inductively_barred_at P 0 l
  apply now_at.P:list bool -> Prop
Hdemorgan:demorgan_inductively_barred_at P
l:list bool
H:~ inductively_barred_at P 0 l
H0:P l
P l auto.
-P:list bool -> Prop
Hdemorgan:demorgan_inductively_barred_at P
n:nat
IHn:forall l0 : list bool,
~ inductively_barred_at P n l0 ->
is_path_from P n l0
l:list bool
H:~ inductively_barred_at P (S n) l
is_path_from P (S n) l assert (H0:~ (inductively_barred_at P n (true::l) /\ inductively_barred_at P n (false::l)))
  by firstorder using inductively_barred_at.P:list bool -> Prop
Hdemorgan:demorgan_inductively_barred_at P
n:nat
IHn:forall l0 : list bool,
~ inductively_barred_at P n l0 ->
is_path_from P n l0
l:list bool
H:~ inductively_barred_at P (S n) l
H0:~
(inductively_barred_at P n (true :: l) /\
 inductively_barred_at P n (false :: l))
is_path_from P (S n) l
  assert (HnP:~ P l) by firstorder using inductively_barred_at.P:list bool -> Prop
Hdemorgan:demorgan_inductively_barred_at P
n:nat
IHn:forall l0 : list bool,
~ inductively_barred_at P n l0 ->
is_path_from P n l0
l:list bool
H:~ inductively_barred_at P (S n) l
H0:~
(inductively_barred_at P n (true :: l) /\
 inductively_barred_at P n (false :: l))
HnP:~ P l
is_path_from P (S n) l
  apply Hdemorgan in H0 as [H0|H0]; apply IHn in H0; auto using is_path_from.
Qed.

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.forall (P : list bool -> Prop) (n : nat)
  (l : list bool),
is_path_from P n l ->
inductively_barred_at P n l -> False
Proof.forall (P : list bool -> Prop) (n : nat)
  (l : list bool),
is_path_from P n l ->
inductively_barred_at P n l -> False
intros P; induction n; intros l H1 H2.P:list bool -> Prop
l:list bool
H1:is_path_from P 0 l
H2:inductively_barred_at P 0 l
False
P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H1:is_path_from P (S n) l
H2:inductively_barred_at P (S n) l
False
-P:list bool -> Prop
l:list bool
H1:is_path_from P 0 l
H2:inductively_barred_at P 0 l
False inversion_clear H1.P:list bool -> Prop
l:list bool
H2:inductively_barred_at P 0 l
H:~ P l
False inversion_clear H2.P:list bool -> Prop
l:list bool
H:~ P l
H0:P l
False auto.
-P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H1:is_path_from P (S n) l
H2:inductively_barred_at P (S n) l
False inversion_clear H1.P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H2:inductively_barred_at P (S n) l
H:~ P l
H0:is_path_from P n (true :: l)
False
P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H2:inductively_barred_at P (S n) l
H:~ P l
H0:is_path_from P n (false :: l)
False
  +P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H2:inductively_barred_at P (S n) l
H:~ P l
H0:is_path_from P n (true :: l)
False inversion_clear H2.P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H:~ P l
H0:is_path_from P n (true :: l)
H1:P l
False
P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H:~ P l
H0:is_path_from P n (true :: l)
H1:inductively_barred_at P n (true :: l)
H3:inductively_barred_at P n (false :: l)
False
    *P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H:~ P l
H0:is_path_from P n (true :: l)
H1:P l
False auto.
    *P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H:~ P l
H0:is_path_from P n (true :: l)
H1:inductively_barred_at P n (true :: l)
H3:inductively_barred_at P n (false :: l)
False apply IHn with (true::l); auto.
  +P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H2:inductively_barred_at P (S n) l
H:~ P l
H0:is_path_from P n (false :: l)
False inversion_clear H2.P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H:~ P l
H0:is_path_from P n (false :: l)
H1:P l
False
P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H:~ P l
H0:is_path_from P n (false :: l)
H1:inductively_barred_at P n (true :: l)
H3:inductively_barred_at P n (false :: l)
False
    *P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H:~ P l
H0:is_path_from P n (false :: l)
H1:P l
False auto.
    *P:list bool -> Prop
n:nat
IHn:forall l0 : list bool,
is_path_from P n l0 -> inductively_barred_at P n l0 -> False
l:list bool
H:~ P l
H0:is_path_from P n (false :: l)
H1:inductively_barred_at P n (true :: l)
H3:inductively_barred_at P n (false :: l)
False apply IHn with (false::l); auto.
Qed.

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).forall (P : list bool -> Prop) (l : list bool)
  (n : nat),
is_path_from P (S n) l ->
inductively_barred_at P n (false :: l) ->
is_path_from P n (true :: l)
Proof.forall (P : list bool -> Prop) (l : list bool)
  (n : nat),
is_path_from P (S n) l ->
inductively_barred_at P n (false :: l) ->
is_path_from P n (true :: l)
inversion 1; subst; intros.P:list bool -> Prop
l:list bool
n:nat
H:is_path_from P (S n) l
H1:~ P l
H2:is_path_from P n (true :: l)
H0:inductively_barred_at P n (false :: l)
is_path_from P n (true :: l)
P:list bool -> Prop
l:list bool
n:nat
H:is_path_from P (S n) l
H1:~ P l
H2:is_path_from P n (false :: l)
H0:inductively_barred_at P n (false :: l)
is_path_from P n (true :: l)
-P:list bool -> Prop
l:list bool
n:nat
H:is_path_from P (S n) l
H1:~ P l
H2:is_path_from P n (true :: l)
H0:inductively_barred_at P n (false :: l)
is_path_from P n (true :: l) auto.
-P:list bool -> Prop
l:list bool
n:nat
H:is_path_from P (S n) l
H1:~ P l
H2:is_path_from P n (false :: l)
H0:inductively_barred_at P n (false :: l)
is_path_from P n (true :: l) exfalso.P:list bool -> Prop
l:list bool
n:nat
H:is_path_from P (S n) l
H1:~ P l
H2:is_path_from P n (false :: l)
H0:inductively_barred_at P n (false :: l)
False eauto using is_path_from_imp_inductively_barred_at.
Qed.

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.forall P : list bool -> Prop,
demorgan_inductively_barred_at P ->
forall l1 l2 : list bool,
length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2
Proof.forall P : list bool -> Prop,
demorgan_inductively_barred_at P ->
forall l1 l2 : list bool,
length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2
intros * DeMorgan.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
forall l1 l2 : list bool,
length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2 induction l1, l2.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
length [] = length [] -> Y P [] -> Y P [] -> [] = []
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
b:bool
l2:list bool
length [] = length (b :: l2) ->
Y P [] -> Y P (b :: l2) -> [] = b :: l2
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l1:list bool
IHl1:forall l2 : list bool,
length l1 = length l2 ->
Y P l1 -> Y P l2 -> l1 = l2
length (a :: l1) = length [] ->
Y P (a :: l1) -> Y P [] -> a :: l1 = []
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l1:list bool
IHl1:forall l0 : list bool,
length l1 = length l0 ->
Y P l1 -> Y P l0 -> l1 = l0
b:bool
l2:list bool
length (a :: l1) = length (b :: l2) ->
Y P (a :: l1) -> Y P (b :: l2) -> a :: l1 = b :: l2
-P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
length [] = length [] -> Y P [] -> Y P [] -> [] = [] trivial.
-P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
b:bool
l2:list bool
length [] = length (b :: l2) ->
Y P [] -> Y P (b :: l2) -> [] = b :: l2 discriminate.
-P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l1:list bool
IHl1:forall l2 : list bool,
length l1 = length l2 ->
Y P l1 -> Y P l2 -> l1 = l2
length (a :: l1) = length [] ->
Y P (a :: l1) -> Y P [] -> a :: l1 = [] discriminate.
-P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l1:list bool
IHl1:forall l0 : list bool,
length l1 = length l0 ->
Y P l1 -> Y P l0 -> l1 = l0
b:bool
l2:list bool
length (a :: l1) = length (b :: l2) ->
Y P (a :: l1) -> Y P (b :: l2) -> a :: l1 = b :: l2 intros [= H] (HY1,H1) (HY2,H2).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l1:list bool
IHl1:forall l0 : list bool,
length l1 = length l0 ->
Y P l1 -> Y P l0 -> l1 = l0
b:bool
l2:list bool
H:length l1 = length l2
HY1:Y P l1
H1:if a
then
 exists n : nat,
   inductively_barred_at P n (false :: l1)
else infinite_from P (false :: l1)
HY2:Y P l2
H2:if b
then
 exists n : nat,
   inductively_barred_at P n (false :: l2)
else infinite_from P (false :: l2)
a :: l1 = b :: l2
  pose proof (IHl1 l2 H HY1 HY2).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l1:list bool
IHl1:forall l0 : list bool,
length l1 = length l0 ->
Y P l1 -> Y P l0 -> l1 = l0
b:bool
l2:list bool
H:length l1 = length l2
HY1:Y P l1
H1:if a
then
 exists n : nat,
   inductively_barred_at P n (false :: l1)
else infinite_from P (false :: l1)
HY2:Y P l2
H2:if b
then
 exists n : nat,
   inductively_barred_at P n (false :: l2)
else infinite_from P (false :: l2)
H0:l1 = l2
a :: l1 = b :: l2 clear HY1 HY2 H IHl1.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l1:list bool
b:bool
l2:list bool
H1:if a
then
 exists n : nat,
   inductively_barred_at P n (false :: l1)
else infinite_from P (false :: l1)
H2:if b
then
 exists n : nat,
   inductively_barred_at P n (false :: l2)
else infinite_from P (false :: l2)
H0:l1 = l2
a :: l1 = b :: l2
  subst l1.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a, b:bool
l2:list bool
H1:if a
then
 exists n : nat,
   inductively_barred_at P n (false :: l2)
else infinite_from P (false :: l2)
H2:if b
then
 exists n : nat,
   inductively_barred_at P n (false :: l2)
else infinite_from P (false :: l2)
a :: l2 = b :: l2
  f_equal.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a, b:bool
l2:list bool
H1:if a
then
 exists n : nat,
   inductively_barred_at P n (false :: l2)
else infinite_from P (false :: l2)
H2:if b
then
 exists n : nat,
   inductively_barred_at P n (false :: l2)
else infinite_from P (false :: l2)
a = b
  destruct a, b; try reflexivity.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l2:list bool
H1:exists n : nat,
  inductively_barred_at P n (false :: l2)
H2:infinite_from P (false :: l2)
true = false
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l2:list bool
H1:infinite_from P (false :: l2)
H2:exists n : nat,
  inductively_barred_at P n (false :: l2)
false = true
  +P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l2:list bool
H1:exists n : nat,
  inductively_barred_at P n (false :: l2)
H2:infinite_from P (false :: l2)
true = false destruct H1 as (n,Hbar).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l2:list bool
n:nat
Hbar:inductively_barred_at P n (false :: l2)
H2:infinite_from P (false :: l2)
true = false
    destruct (is_path_from_imp_inductively_barred_at _ _ _ (H2 n) Hbar).
  +P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l2:list bool
H1:infinite_from P (false :: l2)
H2:exists n : nat,
  inductively_barred_at P n (false :: l2)
false = true destruct H2 as (n,Hbar).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l2:list bool
H1:infinite_from P (false :: l2)
n:nat
Hbar:inductively_barred_at P n (false :: l2)
false = true
    destruct (is_path_from_imp_inductively_barred_at _ _ _ (H1 n) Hbar).
Qed.

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.forall P : list bool -> Prop,
demorgan_inductively_barred_at P ->
forall l : list bool, approx (X P) l -> Y P l
Proof.forall P : list bool -> Prop,
demorgan_inductively_barred_at P ->
forall l : list bool, approx (X P) l -> Y P l
intros P DeMorgan.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
forall l : list bool, approx (X P) l -> Y P l induction l.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
approx (X P) [] -> Y P []
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l:list bool
IHl:approx (X P) l -> Y P l
approx (X P) (a :: l) -> Y P (a :: l)
-P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
approx (X P) [] -> Y P [] trivial.
-P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l:list bool
IHl:approx (X P) l -> Y P l
approx (X P) (a :: l) -> Y P (a :: l) intros (H,Hb).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:if a then X P (length l) else ~ X P (length l)
Y P (a :: l) split.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:if a then X P (length l) else ~ X P (length l)
Y P l
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:if a then X P (length l) else ~ X P (length l)
if a
then
 exists n : nat,
   inductively_barred_at P n (false :: l)
else infinite_from P (false :: l)
  +P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:if a then X P (length l) else ~ X P (length l)
Y P l auto.
  +P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:if a then X P (length l) else ~ X P (length l)
if a
then
 exists n : nat,
   inductively_barred_at P n (false :: l)
else infinite_from P (false :: l) unfold X in Hb.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
a:bool
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:if a
then
 exists l0 : list bool,
   length l0 = length l /\ Y P (true :: l0)
else
 ~
 (exists l0 : list bool,
    length l0 = length l /\ Y P (true :: l0))
if a
then
 exists n : nat,
   inductively_barred_at P n (false :: l)
else infinite_from P (false :: l)
    destruct a.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:exists l0 : list bool,
  length l0 = length l /\ Y P (true :: l0)
exists n : nat, inductively_barred_at P n (false :: l)
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:~
(exists l0 : list bool,
   length l0 = length l /\ Y P (true :: l0))
infinite_from P (false :: l)
    *P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:exists l0 : list bool,
  length l0 = length l /\ Y P (true :: l0)
exists n : nat, inductively_barred_at P n (false :: l) destruct Hb as (l',(Hl',(HYl',HY))).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
l':list bool
Hl':length l' = length l
HYl':Y P l'
HY:exists n : nat,
  inductively_barred_at P n (false :: l')
exists n : nat, inductively_barred_at P n (false :: l)
      rewrite <- (Y_unique P DeMorgan l' l Hl'); auto.
    *P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:~
(exists l0 : list bool,
   length l0 = length l /\ Y P (true :: l0))
infinite_from P (false :: l) intro n.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:~
(exists l0 : list bool,
   length l0 = length l /\ Y P (true :: l0))
n:nat
is_path_from P n (false :: l) apply inductively_barred_at_imp_is_path_from.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:~
(exists l0 : list bool,
   length l0 = length l /\ Y P (true :: l0))
n:nat
demorgan_inductively_barred_at P
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:~
(exists l0 : list bool,
   length l0 = length l /\ Y P (true :: l0))
n:nat
~ inductively_barred_at P n (false :: l) assumption.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
l:list bool
IHl:approx (X P) l -> Y P l
H:approx (X P) l
Hb:~
(exists l0 : list bool,
   length l0 = length l /\ Y P (true :: l0))
n:nat
~ inductively_barred_at P n (false :: l)
      firstorder.
Qed.

Main theorem

Theorem PreWeakKonigsLemma : forall P,
  demorgan_inductively_barred_at P -> infinite_from P [] -> has_infinite_path P.forall P : list bool -> Prop,
demorgan_inductively_barred_at P ->
infinite_from P [] -> has_infinite_path P
Proof.forall P : list bool -> Prop,
demorgan_inductively_barred_at P ->
infinite_from P [] -> has_infinite_path P
intros P DeMorgan Hinf.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
has_infinite_path P
exists (X P).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
forall l : list bool, approx (X P) l -> ~ P l intros l Hl.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:approx (X P) l
~ P l
assert (infinite_from P l).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:approx (X P) l
infinite_from P l
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:approx (X P) l
H:infinite_from P l
~ P l
{P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:approx (X P) l
infinite_from P l induction l.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
Hl:approx (X P) []
infinite_from P []
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
a:bool
l:list bool
Hl:approx (X P) (a :: l)
IHl:approx (X P) l -> infinite_from P l
infinite_from P (a :: l)
  -P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
Hl:approx (X P) []
infinite_from P [] assumption.
  -P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
a:bool
l:list bool
Hl:approx (X P) (a :: l)
IHl:approx (X P) l -> infinite_from P l
infinite_from P (a :: l) destruct Hl as (Hl,Ha).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
a:bool
l:list bool
Hl:approx (X P) l
Ha:if a then X P (length l) else ~ X P (length l)
IHl:approx (X P) l -> infinite_from P l
infinite_from P (a :: l)
    intros n.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
a:bool
l:list bool
Hl:approx (X P) l
Ha:if a then X P (length l) else ~ X P (length l)
IHl:approx (X P) l -> infinite_from P l
n:nat
is_path_from P n (a :: l)
    pose proof (IHl Hl) as IHl'.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
a:bool
l:list bool
Hl:approx (X P) l
Ha:if a then X P (length l) else ~ X P (length l)
IHl:approx (X P) l -> infinite_from P l
n:nat
IHl':infinite_from P l
is_path_from P n (a :: l) clear IHl.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
a:bool
l:list bool
Hl:approx (X P) l
Ha:if a then X P (length l) else ~ X P (length l)
n:nat
IHl':infinite_from P l
is_path_from P n (a :: l)
    apply Y_approx in Hl; [|assumption].P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
a:bool
l:list bool
Hl:Y P l
Ha:if a then X P (length l) else ~ X P (length l)
n:nat
IHl':infinite_from P l
is_path_from P n (a :: l)
    destruct a.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
Ha:X P (length l)
n:nat
IHl':infinite_from P l
is_path_from P n (true :: l)
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
Ha:~ X P (length l)
n:nat
IHl':infinite_from P l
is_path_from P n (false :: l)
    +P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
Ha:X P (length l)
n:nat
IHl':infinite_from P l
is_path_from P n (true :: l) destruct Ha as (l'&Hl'&HY'&n'&Hbar).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
l':list bool
Hl':length l' = length l
HY':Y P l'
n':nat
Hbar:inductively_barred_at P n' (false :: l')
n:nat
IHl':infinite_from P l
is_path_from P n (true :: l)
      rewrite (Y_unique _ DeMorgan _ _ Hl' HY' Hl) in Hbar.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
l':list bool
Hl':length l' = length l
HY':Y P l'
n':nat
Hbar:inductively_barred_at P n' (false :: l)
n:nat
IHl':infinite_from P l
is_path_from P n (true :: l)
      destruct (le_lt_dec n n') as [Hle|Hlt].P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
l':list bool
Hl':length l' = length l
HY':Y P l'
n':nat
Hbar:inductively_barred_at P n' (false :: l)
n:nat
IHl':infinite_from P l
Hle:n <= n'
is_path_from P n (true :: l)
P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
l':list bool
Hl':length l' = length l
HY':Y P l'
n':nat
Hbar:inductively_barred_at P n' (false :: l)
n:nat
IHl':infinite_from P l
Hlt:n' < n
is_path_from P n (true :: l)
      *P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
l':list bool
Hl':length l' = length l
HY':Y P l'
n':nat
Hbar:inductively_barred_at P n' (false :: l)
n:nat
IHl':infinite_from P l
Hle:n <= n'
is_path_from P n (true :: l) specialize (IHl' (S n')).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
l':list bool
Hl':length l' = length l
HY':Y P l'
n':nat
Hbar:inductively_barred_at P n' (false :: l)
n:nat
IHl':is_path_from P (S n') l
Hle:n <= n'
is_path_from P n (true :: l)
        apply is_path_from_restrict with n'; [assumption|].P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
l':list bool
Hl':length l' = length l
HY':Y P l'
n':nat
Hbar:inductively_barred_at P n' (false :: l)
n:nat
IHl':is_path_from P (S n') l
Hle:n <= n'
is_path_from P n' (true :: l)
        apply find_left_path; trivial.
      *P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
l':list bool
Hl':length l' = length l
HY':Y P l'
n':nat
Hbar:inductively_barred_at P n' (false :: l)
n:nat
IHl':infinite_from P l
Hlt:n' < n
is_path_from P n (true :: l) specialize (IHl' (S n)).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
l':list bool
Hl':length l' = length l
HY':Y P l'
n':nat
Hbar:inductively_barred_at P n' (false :: l)
n:nat
IHl':is_path_from P (S n) l
Hlt:n' < n
is_path_from P n (true :: l)
        apply inductively_barred_at_monotone with (n:=n) in Hbar; [|apply lt_le_weak, Hlt].P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
l':list bool
Hl':length l' = length l
HY':Y P l'
n', n:nat
Hbar:inductively_barred_at P n (false :: l)
IHl':is_path_from P (S n) l
Hlt:n' < n
is_path_from P n (true :: l)
        apply find_left_path; trivial.
    +P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:Y P l
Ha:~ X P (length l)
n:nat
IHl':infinite_from P l
is_path_from P n (false :: l) apply inductively_barred_at_imp_is_path_from; firstorder. }P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:approx (X P) l
H:infinite_from P l
~ P l
specialize (H 0).P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:approx (X P) l
H:is_path_from P 0 l
~ P l inversion H.P:list bool -> Prop
DeMorgan:demorgan_inductively_barred_at P
Hinf:infinite_from P []
l:list bool
Hl:approx (X P) l
H:is_path_from P 0 l
l0:list bool
H0:~ P l
H2:l0 = l
~ P l assumption.
Qed.

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.forall P : list bool -> Prop,
(forall l : list bool, P l \/ ~ P l) ->
forall (n : nat) (l : list bool),
inductively_barred_at P n l \/
~ inductively_barred_at P n l
Proof.forall P : list bool -> Prop,
(forall l : list bool, P l \/ ~ P l) ->
forall (n : nat) (l : list bool),
inductively_barred_at P n l \/
~ inductively_barred_at P n l
intros P HP.P:list bool -> Prop
HP:forall l : list bool, P l \/ ~ P l
forall (n : nat) (l : list bool),
inductively_barred_at P n l \/
~ inductively_barred_at P n l induction n; intros.P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
l:list bool
inductively_barred_at P 0 l \/
~ inductively_barred_at P 0 l
P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l
-P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
l:list bool
inductively_barred_at P 0 l \/
~ inductively_barred_at P 0 l destruct (HP l).P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
l:list bool
H:P l
inductively_barred_at P 0 l \/
~ inductively_barred_at P 0 l
P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
l:list bool
H:~ P l
inductively_barred_at P 0 l \/
~ inductively_barred_at P 0 l
  +P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
l:list bool
H:P l
inductively_barred_at P 0 l \/
~ inductively_barred_at P 0 l left.P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
l:list bool
H:P l
inductively_barred_at P 0 l apply now_at, H.
  +P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
l:list bool
H:~ P l
inductively_barred_at P 0 l \/
~ inductively_barred_at P 0 l right.P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
l:list bool
H:~ P l
~ inductively_barred_at P 0 l inversion 1.P:list bool -> Prop
HP:forall l1 : list bool, P l1 \/ ~ P l1
l:list bool
H:~ P l
H0:inductively_barred_at P 0 l
l0:list bool
n:nat
H1:P l
H2:n = 0
H3:l0 = l
False auto.
-P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l destruct (HP l).P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:P l
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l
P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l
  +P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:P l
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l left.P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:P l
inductively_barred_at P (S n) l apply now_at, H.
  +P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l destruct (IHn (true::l)).P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:inductively_barred_at P n (true :: l)
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l
P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:~ inductively_barred_at P n (true :: l)
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l
    *P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:inductively_barred_at P n (true :: l)
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l destruct (IHn (false::l)).P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:inductively_barred_at P n (true :: l)
H1:inductively_barred_at P n (false :: l)
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l
P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:inductively_barred_at P n (true :: l)
H1:~ inductively_barred_at P n (false :: l)
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l
      {P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:inductively_barred_at P n (true :: l)
H1:inductively_barred_at P n (false :: l)
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l left.P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:inductively_barred_at P n (true :: l)
H1:inductively_barred_at P n (false :: l)
inductively_barred_at P (S n) l apply propagate_at; assumption. }P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:inductively_barred_at P n (true :: l)
H1:~ inductively_barred_at P n (false :: l)
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l
      {P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:inductively_barred_at P n (true :: l)
H1:~ inductively_barred_at P n (false :: l)
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l right.P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:inductively_barred_at P n (true :: l)
H1:~ inductively_barred_at P n (false :: l)
~ inductively_barred_at P (S n) l inversion_clear 1; auto. }
    *P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:~ inductively_barred_at P n (true :: l)
inductively_barred_at P (S n) l \/
~ inductively_barred_at P (S n) l right.P:list bool -> Prop
HP:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
IHn:forall l0 : list bool,
inductively_barred_at P n l0 \/ ~ inductively_barred_at P n l0
l:list bool
H:~ P l
H0:~ inductively_barred_at P n (true :: l)
~ inductively_barred_at P (S n) l inversion_clear 1; auto.
Qed.

Lemma inductively_barred_at_is_path_from_decidable :
  forall P, (forall l, P l \/ ~ P l) -> demorgan_inductively_barred_at P.forall P : list bool -> Prop,
(forall l : list bool, P l \/ ~ P l) ->
demorgan_inductively_barred_at P
Proof.forall P : list bool -> Prop,
(forall l : list bool, P l \/ ~ P l) ->
demorgan_inductively_barred_at P
intros P Hdec n l H.P:list bool -> Prop
Hdec:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
l:list bool
H:~
(inductively_barred_at P n (true :: l) /\
 inductively_barred_at P n (false :: l))
~ inductively_barred_at P n (true :: l) \/
~ inductively_barred_at P n (false :: l)
destruct (inductively_barred_at_decidable P Hdec n (true::l)).P:list bool -> Prop
Hdec:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
l:list bool
H:~
(inductively_barred_at P n (true :: l) /\
 inductively_barred_at P n (false :: l))
H0:inductively_barred_at P n (true :: l)
~ inductively_barred_at P n (true :: l) \/
~ inductively_barred_at P n (false :: l)
P:list bool -> Prop
Hdec:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
l:list bool
H:~
(inductively_barred_at P n (true :: l) /\
 inductively_barred_at P n (false :: l))
H0:~ inductively_barred_at P n (true :: l)
~ inductively_barred_at P n (true :: l) \/
~ inductively_barred_at P n (false :: l)
-P:list bool -> Prop
Hdec:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
l:list bool
H:~
(inductively_barred_at P n (true :: l) /\
 inductively_barred_at P n (false :: l))
H0:inductively_barred_at P n (true :: l)
~ inductively_barred_at P n (true :: l) \/
~ inductively_barred_at P n (false :: l) destruct (inductively_barred_at_decidable P Hdec n (false::l)).P:list bool -> Prop
Hdec:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
l:list bool
H:~
(inductively_barred_at P n (true :: l) /\
 inductively_barred_at P n (false :: l))
H0:inductively_barred_at P n (true :: l)
H1:inductively_barred_at P n (false :: l)
~ inductively_barred_at P n (true :: l) \/
~ inductively_barred_at P n (false :: l)
P:list bool -> Prop
Hdec:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
l:list bool
H:~
(inductively_barred_at P n (true :: l) /\
 inductively_barred_at P n (false :: l))
H0:inductively_barred_at P n (true :: l)
H1:~ inductively_barred_at P n (false :: l)
~ inductively_barred_at P n (true :: l) \/
~ inductively_barred_at P n (false :: l)
  +P:list bool -> Prop
Hdec:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
l:list bool
H:~
(inductively_barred_at P n (true :: l) /\
 inductively_barred_at P n (false :: l))
H0:inductively_barred_at P n (true :: l)
H1:inductively_barred_at P n (false :: l)
~ inductively_barred_at P n (true :: l) \/
~ inductively_barred_at P n (false :: l) auto.
  +P:list bool -> Prop
Hdec:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
l:list bool
H:~
(inductively_barred_at P n (true :: l) /\
 inductively_barred_at P n (false :: l))
H0:inductively_barred_at P n (true :: l)
H1:~ inductively_barred_at P n (false :: l)
~ inductively_barred_at P n (true :: l) \/
~ inductively_barred_at P n (false :: l) auto.
-P:list bool -> Prop
Hdec:forall l0 : list bool, P l0 \/ ~ P l0
n:nat
l:list bool
H:~
(inductively_barred_at P n (true :: l) /\
 inductively_barred_at P n (false :: l))
H0:~ inductively_barred_at P n (true :: l)
~ inductively_barred_at P n (true :: l) \/
~ inductively_barred_at P n (false :: l) auto.
Qed.

Main corollary

Corollary WeakKonigsLemma : forall P, (forall l, P l \/ ~ P l) ->
  infinite_from P [] -> has_infinite_path P.forall P : list bool -> Prop,
(forall l : list bool, P l \/ ~ P l) ->
infinite_from P [] -> has_infinite_path P
Proof.forall P : list bool -> Prop,
(forall l : list bool, P l \/ ~ P l) ->
infinite_from P [] -> has_infinite_path P
intros P Hdec Hinf.P:list bool -> Prop
Hdec:forall l : list bool, P l \/ ~ P l
Hinf:infinite_from P []
has_infinite_path P
apply inductively_barred_at_is_path_from_decidable in Hdec.P:list bool -> Prop
Hdec:demorgan_inductively_barred_at P
Hinf:infinite_from P []
has_infinite_path P
apply PreWeakKonigsLemma; assumption.
Qed.