Completing c236b51348d2 by fixing EqdepFactsv actually committing the

new files (WeakFan.v and WKL.v).

3 files changed, 345 insertions, 5 deletions

diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 653f0b9b4e..4dfe99504c 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -438,14 +438,11 @@ Notation inj_pairT2 := inj_pair2.
 
 End EqdepTheory.
 
-Arguments eq_dep  U P p x q _ : clear implicits.
-Arguments eq_dep1 U P p x q y : clear implicits.
-
 (** Basic facts about eq_dep *)
 
 Lemma f_eq_dep :
   forall U (P:U->Type) R p q x y (f:forall p, P p -> R p),
-    eq_dep x y -> eq_dep (f p x) (f q y).
+    eq_dep p x q y -> eq_dep p (f p x) q (f q y).
 Proof.
 intros * []. reflexivity.
 Qed.
@@ -458,7 +455,10 @@ Qed.
 
 Lemma f_eq_dep_non_dep :
   forall U (P:U->Type) R p q x y (f:forall p, P p -> R),
-    eq_dep x y -> f p x = f q y.
+    eq_dep p x q y -> f p x = f q y.
 Proof.
 intros * []. reflexivity.
 Qed.
+
+Arguments eq_dep  U P p x q _ : clear implicits.
+Arguments eq_dep1 U P p x q y : clear implicits.
diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v
new file mode 100644
index 0000000000..24f1717a7c
--- /dev/null
+++ b/theories/Logic/WKL.v
@@ -0,0 +1,235 @@
+(************************************************************************)
+(*  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 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.
+
+(** [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.
+
+(** [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.
+Proof.
+intros * Hle H; induction H in n, Hle, H |- * ; intros.
+- apply le_n_0_eq in Hle as <-. apply here. assumption.
+- destruct n.
+  + apply here. assumption.
+  + apply next_left; auto using le_S_n.
+- destruct n.
+  + apply here. assumption.
+  + 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.
+Proof.
+intros * Hle Hbar.
+induction Hbar in n, l, Hle, Hbar |- *.
+- apply now_at; auto.
+- destruct n; [apply le_Sn_0 in Hle; contradiction|].
+  apply le_S_n in Hle.
+  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.
+Proof.
+intros P Hdemorgan; induction n; intros l H.
+- apply here.
+  intro. apply H.
+  apply now_at. auto.
+- assert (H0:~ (inductively_barred_at P n (true::l) /\ inductively_barred_at P n (false::l)))
+  by firstorder using inductively_barred_at.
+  assert (HnP:~ P l) by firstorder using inductively_barred_at.
+  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.
+Proof.
+intros P; induction n; intros l H1 H2.
+- inversion_clear H1. inversion_clear H2. auto.
+- inversion_clear H1.
+  + inversion_clear H2.
+    * auto.
+    * apply IHn with (true::l); auto.
+  + inversion_clear H2.
+    * auto.
+    * 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).
+Proof.
+inversion 1; subst; intros.
+- auto.
+- exfalso. 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.
+Proof.
+intros * DeMorgan. induction l1, l2.
+- trivial.
+- discriminate.
+- discriminate.
+- intros [= H] (HY1,H1) (HY2,H2).
+  pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1.
+  subst l1.
+  f_equal.
+  destruct a, b; try reflexivity.
+  + destruct H1 as (n,Hbar).
+    destruct (is_path_from_imp_inductively_barred_at _ _ _ (H2 n) Hbar).
+  + destruct H2 as (n,Hbar).
+    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.
+Proof.
+intros P DeMorgan. 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 DeMorgan l' l Hl'); auto.
+    * intro n. apply inductively_barred_at_imp_is_path_from. assumption.
+      firstorder.
+Qed.
+
+(** Main theorem *)
+
+Theorem PreWeakKonigsLemma : forall P,
+  demorgan_inductively_barred_at P -> infinite_from P [] -> has_infinite_path P.
+Proof.
+intros P DeMorgan Hinf.
+exists (X P). intros l Hl.
+assert (infinite_from P l).
+{ induction l.
+  - assumption.
+  - destruct Hl as (Hl,Ha).
+    intros n.
+    pose proof (IHl Hl) as IHl'. clear IHl.
+    apply Y_approx in Hl; [|assumption].
+    destruct a.
+    + destruct Ha as (l'&Hl'&HY'&n'&Hbar).
+      rewrite (Y_unique _ DeMorgan _ _ Hl' HY' Hl) in Hbar.
+      destruct (le_lt_dec n n') as [Hle|Hlt].
+      * specialize (IHl' (S n')).
+        apply is_path_from_restrict with n'; [assumption|].
+        apply find_left_path; trivial.
+      * specialize (IHl' (S n)).
+        apply inductively_barred_at_monotone with (n:=n) in Hbar; [|apply lt_le_weak, Hlt].
+        apply find_left_path; trivial.
+    + apply inductively_barred_at_imp_is_path_from; firstorder. }
+specialize (H 0). inversion H. 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.
+Proof.
+intros P HP. induction n; intros.
+- destruct (HP l).
+  + left. apply now_at, H.
+  + right. inversion 1. auto.
+- destruct (HP l).
+  + left. apply now_at, H.
+  + destruct (IHn (true::l)).
+    * destruct (IHn (false::l)).
+      { left. apply propagate_at; assumption. }
+      { right. inversion_clear 1; auto. }
+    * right. 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.
+Proof.
+intros P Hdec n l H.
+destruct (inductively_barred_at_decidable P Hdec n (true::l)).
+- destruct (inductively_barred_at_decidable P Hdec n (false::l)).
+  + auto.
+  + auto.
+- auto.
+Qed.
+
+(** Main corollary *)
+
+Corollary WeakKonigsLemma : forall P, (forall l, P l \/ ~ P l) ->
+  infinite_from P [] -> has_infinite_path P.
+Proof.
+intros P Hdec Hinf.
+apply inductively_barred_at_is_path_from_decidable in Hdec.
+apply PreWeakKonigsLemma; assumption.
+Qed.
diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v
new file mode 100644
index 0000000000..7de1175d2c
--- /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-2012     *)
+(*   \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.