WeakFan.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 non-standard version of the weak Fan Theorem 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 idea of the proof comes from the proof of the weak König's lemma from separation in second-order arithmetic [Simpson99].

[Simpson99] Stephen G. Simpson. Subsystems of second order arithmetic, Cambridge University Press, 1999

Require Import List.
Import ListNotations.

inductively_barred P l means that P eventually holds above l

Inductive inductively_barred P : list bool -> Prop :=
| now l : P l -> inductively_barred P l
| propagate l :
    inductively_barred P (true::l) ->
    inductively_barred P (false::l) ->
    inductively_barred P l.

approx X l says that l is a boolean representation of a prefix of X

Fixpoint approx X (l:list bool) :=
  match l with
  | [] => True
  | b::l => approx X l /\ (if b then X (length l) else ~ X (length l))
  end.

barred P means that for any infinite path represented as a predicate, the property P holds for some prefix of the path

Definition barred P :=
  forall (X:nat -> Prop), exists l, approx X l /\ P 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 inductively_barred P (false::l) else ~ inductively_barred P (false::l)
  end.

Lemma Y_unique : forall P l1 l2, length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2.forall (P : list bool -> Type) (l1 l2 : list bool),
length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2
Proof.forall (P : list bool -> Type) (l1 l2 : list bool),
length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2
induction l1, l2.P:list bool -> Type
length [] = length [] -> Y P [] -> Y P [] -> [] = []
P:list bool -> Type
b:bool
l2:list bool
length [] = length (b :: l2) ->
Y P [] -> Y P (b :: l2) -> [] = b :: l2
P:list bool -> Type
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 -> Type
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 -> Type
length [] = length [] -> Y P [] -> Y P [] -> [] = [] trivial.
-P:list bool -> Type
b:bool
l2:list bool
length [] = length (b :: l2) ->
Y P [] -> Y P (b :: l2) -> [] = b :: l2 discriminate.
-P:list bool -> Type
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 -> Type
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 -> Type
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 (a :: l1) = length (b :: l2)
HY1:Y P l1
H1:if a
then inductively_barred P (false :: l1)
else ~ inductively_barred P (false :: l1)
HY2:Y P l2
H2:if b
then inductively_barred P (false :: l2)
else ~ inductively_barred P (false :: l2)
a :: l1 = b :: l2
  injection H as H.P:list bool -> Type
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 inductively_barred P (false :: l1)
else ~ inductively_barred P (false :: l1)
HY2:Y P l2
H2:if b
then inductively_barred P (false :: l2)
else ~ inductively_barred P (false :: l2)
a :: l1 = b :: l2
  pose proof (IHl1 l2 H HY1 HY2).P:list bool -> Type
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 inductively_barred P (false :: l1)
else ~ inductively_barred P (false :: l1)
HY2:Y P l2
H2:if b
then inductively_barred P (false :: l2)
else ~ inductively_barred P (false :: l2)
H0:l1 = l2
a :: l1 = b :: l2 clear HY1 HY2 H IHl1.P:list bool -> Type
a:bool
l1:list bool
b:bool
l2:list bool
H1:if a
then inductively_barred P (false :: l1)
else ~ inductively_barred P (false :: l1)
H2:if b
then inductively_barred P (false :: l2)
else ~ inductively_barred P (false :: l2)
H0:l1 = l2
a :: l1 = b :: l2
  subst l1.P:list bool -> Type
a, b:bool
l2:list bool
H1:if a
then inductively_barred P (false :: l2)
else ~ inductively_barred P (false :: l2)
H2:if b
then inductively_barred P (false :: l2)
else ~ inductively_barred P (false :: l2)
a :: l2 = b :: l2
  f_equal.P:list bool -> Type
a, b:bool
l2:list bool
H1:if a
then inductively_barred P (false :: l2)
else ~ inductively_barred P (false :: l2)
H2:if b
then inductively_barred P (false :: l2)
else ~ inductively_barred P (false :: l2)
a = b
  destruct a, b; firstorder.
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 l, approx (X P) l -> Y P l.forall (P : list bool -> Type) (l : list bool),
approx (X P) l -> Y P l
Proof.forall (P : list bool -> Type) (l : list bool),
approx (X P) l -> Y P l
induction l.P:list bool -> Type
approx (X P) [] -> Y P []
P:list bool -> Type
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 -> Type
approx (X P) [] -> Y P [] trivial.
-P:list bool -> Type
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 -> Type
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 -> Type
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 -> Type
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 inductively_barred P (false :: l)
else ~ inductively_barred P (false :: l)
  +P:list bool -> Type
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 -> Type
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 inductively_barred P (false :: l)
else ~ inductively_barred P (false :: l) unfold X in Hb.P:list bool -> Type
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 inductively_barred P (false :: l)
else ~ inductively_barred P (false :: l)
    destruct a.P:list bool -> Type
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)
inductively_barred P (false :: l)
P:list bool -> Type
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))
~ inductively_barred P (false :: l)
    *P:list bool -> Type
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)
inductively_barred P (false :: l) destruct Hb as (l',(Hl',(HYl',HY))).P:list bool -> Type
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:inductively_barred P (false :: l')
inductively_barred P (false :: l)
      rewrite <- (Y_unique P l' l Hl'); auto.
    *P:list bool -> Type
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))
~ inductively_barred P (false :: l) firstorder.
Qed.

Theorem WeakFanTheorem : forall P, barred P -> inductively_barred P [].forall P : list bool -> Prop,
barred P -> inductively_barred P []
Proof.forall P : list bool -> Prop,
barred P -> inductively_barred P []
intros P Hbar.P:list bool -> Prop
Hbar:barred P
inductively_barred P []
destruct Hbar with (X P) as (l,(Hd%Y_approx,HP)).P:list bool -> Prop
Hbar:barred P
l:list bool
Hd:Y P l
HP:P l
inductively_barred P []
assert (inductively_barred P l) by (apply (now P l), HP).P:list bool -> Prop
Hbar:barred P
l:list bool
Hd:Y P l
HP:P l
H:inductively_barred P l
inductively_barred P []
clear Hbar HP.P:list bool -> Prop
l:list bool
Hd:Y P l
H:inductively_barred P l
inductively_barred P []
induction l as [|a l].P:list bool -> Prop
Hd:Y P []
H:inductively_barred P []
inductively_barred P []
P:list bool -> Prop
a:bool
l:list bool
Hd:Y P (a :: l)
H:inductively_barred P (a :: l)
IHl:Y P l ->
inductively_barred P l ->
inductively_barred P []
inductively_barred P []
-P:list bool -> Prop
Hd:Y P []
H:inductively_barred P []
inductively_barred P [] assumption.
-P:list bool -> Prop
a:bool
l:list bool
Hd:Y P (a :: l)
H:inductively_barred P (a :: l)
IHl:Y P l ->
inductively_barred P l ->
inductively_barred P []
inductively_barred P [] destruct Hd as (Hd,HX).P:list bool -> Prop
a:bool
l:list bool
Hd:Y P l
HX:if a
then inductively_barred P (false :: l)
else ~ inductively_barred P (false :: l)
H:inductively_barred P (a :: l)
IHl:Y P l ->
inductively_barred P l ->
inductively_barred P []
inductively_barred P []
  apply (IHl Hd).P:list bool -> Prop
a:bool
l:list bool
Hd:Y P l
HX:if a
then inductively_barred P (false :: l)
else ~ inductively_barred P (false :: l)
H:inductively_barred P (a :: l)
IHl:Y P l ->
inductively_barred P l ->
inductively_barred P []
inductively_barred P l clear IHl.P:list bool -> Prop
a:bool
l:list bool
Hd:Y P l
HX:if a
then inductively_barred P (false :: l)
else ~ inductively_barred P (false :: l)
H:inductively_barred P (a :: l)
inductively_barred P l
  destruct a; unfold X in HX; simpl in HX.P:list bool -> Prop
l:list bool
Hd:Y P l
HX:inductively_barred P (false :: l)
H:inductively_barred P (true :: l)
inductively_barred P l
P:list bool -> Prop
l:list bool
Hd:Y P l
HX:~ inductively_barred P (false :: l)
H:inductively_barred P (false :: l)
inductively_barred P l
  +P:list bool -> Prop
l:list bool
Hd:Y P l
HX:inductively_barred P (false :: l)
H:inductively_barred P (true :: l)
inductively_barred P l apply propagate; assumption.
  +P:list bool -> Prop
l:list bool
Hd:Y P l
HX:~ inductively_barred P (false :: l)
H:inductively_barred P (false :: l)
inductively_barred P l exfalso; destruct (HX H).
Qed.