Added a (constructive) proof of Weak Konig's lemma for decidable trees.

Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem
after all.

3 files changed, 4 insertions, 109 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index c3b2aad58..75b5e7fea 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -68,7 +68,8 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/IndefiniteDescription.v
     theories/Logic/FunctionalExtensionality.v
     theories/Logic/ExtensionalityFacts.v
-    theories/Logic/Fan.v
+    theories/Logic/WeakFan.v
+    theories/Logic/WKL.v
     theories/Logic/FinFun.v
   </dd>
     
diff --git a/theories/Logic/Fan.v b/theories/Logic/Fan.v
deleted file mode 100644
index 27b2d64fb..000000000
--- a/theories/Logic/Fan.v
+++ /dev/null
@@ -1,107 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** A constructive proof of 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 FanTheorem : 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.
diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget
index 488fd908e..6f7eba904 100644
--- a/theories/Logic/vo.itarget
+++ b/theories/Logic/vo.itarget
@@ -16,7 +16,8 @@ Epsilon.vo
 Eqdep_dec.vo
 EqdepFacts.vo
 Eqdep.vo
-Fan.vo
+WeakFan.vo
+WKL.vo
 FunctionalExtensionality.vo
 Hurkens.vo
 IndefiniteDescription.vo