1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
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.
|
