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
|
(************************************************************************)
(* 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.
|
