Library Coq.Logic.WeakFan
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
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
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.
X is the translation of Y as a predicate