diff options
Diffstat (limited to 'theories/Logic/WKL.v')
| -rw-r--r-- | theories/Logic/WKL.v | 261 |
1 files changed, 261 insertions, 0 deletions
diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v new file mode 100644 index 00000000..408eca4a --- /dev/null +++ b/theories/Logic/WKL.v @@ -0,0 +1,261 @@ +(************************************************************************) +(* 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 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. + +Require Import Omega. + +(** [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. + +(** We give the characterization of is_path_from in terms of a more common arithmetical formula *) + +Proposition is_path_from_characterization P n l : + is_path_from P n l <-> exists l', length l' = n /\ forall n', n'<=n -> ~ P (rev (firstn n' l') ++ l). +Proof. +intros. split. +- induction 1 as [|* HP _ (l'&Hl'&HPl')|* HP _ (l'&Hl'&HPl')]. + + exists []. split. reflexivity. intros n <-/le_n_0_eq. assumption. + + exists (true :: l'). split. apply eq_S, Hl'. intros [|] H. + * assumption. + * simpl. rewrite <- app_assoc. apply HPl', le_S_n, H. + + exists (false :: l'). split. apply eq_S, Hl'. intros [|] H. + * assumption. + * simpl. rewrite <- app_assoc. apply HPl', le_S_n, H. +- intros (l'& <- &HPl'). induction l' as [|[|]] in l, HPl' |- *. + + constructor. apply (HPl' 0). apply le_0_n. + + eapply next_left. + * apply (HPl' 0), le_0_n. + * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption. + + apply next_right. + * apply (HPl' 0), le_0_n. + * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption. +Qed. + +(** [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. |