1 files changed, 105 insertions, 0 deletions
diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v
new file mode 100644
index 00000000..49cc12b8
--- /dev/null
+++ b/theories/Logic/WeakFan.v
@@ -0,0 +1,105 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** 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.
+Proof.
+induction l1, l2.
+- trivial.
+- discriminate.
+- discriminate.
+- intros H (HY1,H1) (HY2,H2).
+  injection H as H.
+  pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1.
+  subst l1.
+  f_equal.
+  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.
+Proof.
+induction l.
+- trivial.
+- intros (H,Hb). split.
+  + auto.
+  + unfold X in Hb.
+    destruct a.
+    * destruct Hb as (l',(Hl',(HYl',HY))).
+      rewrite <- (Y_unique P l' l Hl'); auto.
+    * firstorder.
+Qed.
+
+Theorem WeakFanTheorem : forall P, barred P -> inductively_barred P [].
+Proof.
+intros P Hbar.
+destruct (Hbar (X P)) as (l,(Hd,HP)).
+assert (inductively_barred P l) by (apply (now P l), HP).
+clear Hbar HP.
+induction l.
+- assumption.
+- destruct Hd as (Hd,HX).
+  apply (IHl Hd). clear IHl.
+  destruct a; unfold X in HX; simpl in HX.
+  + apply propagate.
+    * apply H.
+    * destruct HX as (l',(Hl,(HY,Ht))); firstorder.
+      apply Y_approx in Hd. rewrite <- (Y_unique P l' l Hl); trivial.
+  + destruct HX. exists l. split; auto using Y_approx.
+Qed.