-
Notifications
You must be signed in to change notification settings - Fork 0
/
Classical_Wf.v
175 lines (154 loc) · 3.45 KB
/
Classical_Wf.v
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
Require Import Classical.
Require Export Ensembles.
Require Import EnsemblesImplicit.
Require Export Relation_Definitions.
Require Import Relation_Definitions_Implicit.
Require Import EnsemblesSpec.
Section MinimalElements.
Variable T:Type.
Variable R:relation T.
(* R is well-founded if and only if every nonempty subset of
T has a minimal element *)
Definition minimal_element_property : Prop :=
forall S:Ensemble T, Inhabited S -> exists x:T, In S x /\
forall y:T, In S y -> ~ R y x.
Lemma WF_implies_MEP: well_founded R -> minimal_element_property.
Proof.
unfold well_founded.
unfold minimal_element_property.
intros WF S Hinh.
destruct Hinh.
revert x H.
apply (@well_founded_ind T R WF
(fun x:T =>
In S x -> exists y:T, In S y /\ (forall z:T, In S z -> ~ R z y))).
intros.
case (classic (forall y:T, In S y -> ~ R y x)).
exists x.
split.
assumption.
assumption.
intro.
apply not_all_ex_not in H1.
destruct H1.
apply imply_to_and in H1.
destruct H1.
apply H with x0.
apply NNPP.
assumption.
assumption.
Qed.
Lemma MEP_implies_WF: minimal_element_property -> well_founded R.
Proof.
unfold well_founded.
unfold minimal_element_property.
intro MEP.
apply NNPP.
intuition.
apply not_all_ex_not in H.
destruct H.
assert (Inhabited [x:T | ~ Acc R x]).
exists x.
constructor; assumption.
apply MEP in H0.
destruct H0.
destruct H0.
destruct H0.
contradict H0.
constructor.
intros.
apply NNPP.
intuition.
apply H1 with y.
constructor; assumption.
assumption.
Qed.
End MinimalElements.
Section DecreasingSequences.
(* R is well-founded if and only if there is no infinite strictly
decreasing sequence of elements of T *)
Variable T:Type.
Variable R:relation T.
Definition decreasing_sequence_property :=
forall a:nat->T, exists n:nat, ~ R (a (S n)) (a n).
Lemma WF_implies_DSP: well_founded R -> decreasing_sequence_property.
Proof.
unfold decreasing_sequence_property.
intros WF a.
remember (a 0) as a0.
revert a0 a Heqa0.
apply (well_founded_ind WF (fun x:T =>
forall a:nat->T, x = a 0 -> exists n:nat, ~ R (a (S n)) (a n))).
intros.
case (classic (R (a 1) (a 0))).
intro.
pose (b := fun n:nat => a (S n)).
assert (exists n:nat, ~ R (b (S n)) (b n)).
apply H with (a 1).
rewrite H0.
assumption.
trivial.
destruct H2.
exists (S x0).
unfold b in H2.
assumption.
exists 0.
assumption.
Qed.
Require Import ClassicalChoice.
Lemma DSP_implies_WF: decreasing_sequence_property -> well_founded R.
Proof.
unfold decreasing_sequence_property.
intro DSP.
apply MEP_implies_WF.
unfold minimal_element_property.
intro S0.
intros.
apply NNPP.
intuition.
assert (forall x:T, In S0 x -> exists y:T, In S0 y /\ R y x).
intros.
apply NNPP.
intuition.
assert (forall y:T, ~(In S0 y /\ R y x)).
apply not_ex_all_not.
assumption.
apply H0.
exists x.
split.
assumption.
intros.
apply H3 with y.
tauto.
pose (S_type := {x:T | In S0 x}).
assert (exists f:S_type -> S_type, forall x:S_type,
R (proj1_sig (f x)) (proj1_sig x)).
apply choice with (R:=fun x y:S_type => R (proj1_sig y) (proj1_sig x)).
intro.
destruct x.
simpl.
pose proof (H1 x i).
destruct H2.
destruct H2.
exists (exist (fun x:T => In S0 x) x0 H2).
simpl.
assumption.
destruct H2 as [f Hf].
destruct H.
pose (b := nat_rect (fun n:nat => S_type)
(exist (fun x:T => In S0 x) x H)
(fun (n:nat) (x:S_type) => f x)).
simpl in b.
pose (a := fun n:nat => (proj1_sig (b n))).
assert (forall n:nat, R (a (S n)) (a n)).
unfold a.
intro.
simpl.
apply Hf.
contradict DSP.
apply ex_not_not_all.
exists a.
apply all_not_not_ex.
auto.
Qed.
End DecreasingSequences.