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
|
(* Bounded and unbounded iterators *)
Require Recdef.
Require Import Coqlib.
Require Import Classical.
Require Import Max.
Module Type ITER.
Variable iterate
: forall A B : Set, (A -> B + A) -> A -> option B.
Hypothesis iterate_prop
: forall (A B : Set) (step : A -> B + A) (P : A -> Prop) (Q : B -> Prop),
(forall a : A, P a ->
match step a with inl b => Q b | inr a' => P a' end) ->
forall (a : A) (b : B), iterate A B step a = Some b -> P a -> Q b.
End ITER.
Axiom
dependent_description' :
forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
(forall x:A,
exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))).
(* A constructive implementation using bounded iteration. *)
Module PrimIter: ITER.
Section ITERATION.
Variables A B: Set.
Variable step: A -> B + A.
(** The [step] parameter represents one step of the iteration. From a
current iteration state [a: A], it either returns a value of type [B],
meaning that iteration is over and that this [B] value is the final
result of the iteration, or a value [a' : A] which is the next state
of the iteration.
The naive way to define the iteration is:
<<
Fixpoint iterate (a: A) : B :=
match step a with
| inl b => b
| inr a' => iterate a'
end.
>>
However, this is a general recursion, not guaranteed to terminate,
and therefore not expressible in Coq. The standard way to work around
this difficulty is to use Noetherian recursion (Coq module [Wf]).
This requires that we equip the type [A] with a well-founded ordering [<]
(no infinite ascending chains) and we demand that [step] satisfies
[step a = inr a' -> a < a']. For the types [A] that are of interest to us
in this development, it is however very painful to define adequate
well-founded orderings, even though we know our iterations always
terminate.
Instead, we choose to bound the number of iterations by an arbitrary
constant. [iterate] then becomes a function that can fail,
of type [A -> option B]. The [None] result denotes failure to reach
a result in the number of iterations prescribed, or, in other terms,
failure to find a solution to the dataflow problem. The compiler
passes that exploit dataflow analysis (the [Constprop], [CSE] and
[Allocation] passes) will, in this case, either fail ([Allocation])
or turn off the optimization pass ([Constprop] and [CSE]).
Since we know (informally) that our computations terminate, we can
take a very large constant as the maximal number of iterations.
Failure will therefore never happen in practice, but of
course our proofs also cover the failure case and show that
nothing bad happens in this hypothetical case either. *)
Definition num_iterations := 1000000000000%positive.
Function iter (niter: positive) (s: A) {wf Plt niter} : option B :=
if peq niter xH then None else
match step s with
| inl res => Some res
| inr s' => iter (Ppred niter) s'
end.
Proof.
intros. apply Ppred_Plt. auto.
apply Plt_wf.
Qed.
(** The [iterate] function is defined as [iter] up to
[num_iterations] through the loop. *)
Definition iterate := iter num_iterations.
(** We now prove the invariance property [iterate_prop]. *)
Variable P: A -> Prop.
Variable Q: B -> Prop.
Hypothesis step_prop:
forall a : A, P a ->
match step a with inl b => Q b | inr a' => P a' end.
Lemma iter_prop:
forall n a b, P a -> iter n a = Some b -> Q b.
Proof.
intros n a. functional induction (iter n a); intros.
discriminate.
inversion H0; subst b. generalize (step_prop s H). rewrite e0. auto.
apply IHo. generalize (step_prop s H). rewrite e0. auto. auto.
Qed.
Lemma iterate_prop:
forall a b, iterate a = Some b -> P a -> Q b.
Proof.
intros. apply iter_prop with num_iterations a; assumption.
Qed.
End ITERATION.
End PrimIter.
(* An implementation using classical logic and unbounded iteration,
in the style of Yves Bertot's paper, "Extending the Calculus
of Constructions with Tarski's fix-point theorem". *)
Module GenIter: ITER.
Section ITERATION.
Variables A B: Set.
Variable step: A -> B + A.
Definition B_le (x y: option B) : Prop := x = None \/ y = x.
Definition F_le (x y: A -> option B) : Prop := forall a, B_le (x a) (y a).
Definition F_iter (next: A -> option B) (a: A) : option B :=
match step a with
| inl b => Some b
| inr a' => next a'
end.
Lemma F_iter_monot:
forall f g, F_le f g -> F_le (F_iter f) (F_iter g).
Proof.
intros; red; intros. unfold F_iter.
destruct (step a) as [b | a']. red; auto. apply H.
Qed.
Fixpoint iter (n: nat) : A -> option B :=
match n with
| O => (fun a => None)
| S m => F_iter (iter m)
end.
Lemma iter_monot:
forall p q, (p <= q)%nat -> F_le (iter p) (iter q).
Proof.
induction p; intros.
simpl. red; intros; red; auto.
destruct q. elimtype False; omega.
simpl. apply F_iter_monot. apply IHp. omega.
Qed.
Lemma iter_either:
forall a,
(exists n, exists b, iter n a = Some b) \/
(forall n, iter n a = None).
Proof.
intro a. elim (classic (forall n, iter n a = None)); intro.
right; assumption.
left. generalize (not_all_ex_not nat (fun n => iter n a = None) H).
intros [n D]. exists n. generalize D.
case (iter n a); intros. exists b; auto. congruence.
Qed.
Definition converges_to (a: A) (b: option B) : Prop :=
exists n, forall m, (n <= m)%nat -> iter m a = b.
Lemma converges_to_Some:
forall a n b, iter n a = Some b -> converges_to a (Some b).
Proof.
intros. exists n. intros.
assert (B_le (iter n a) (iter m a)). apply iter_monot. auto.
elim H1; intro; congruence.
Qed.
Lemma converges_to_exists:
forall a, exists b, converges_to a b.
Proof.
intros. elim (iter_either a).
intros [n [b EQ]]. exists (Some b). apply converges_to_Some with n. assumption.
intro. exists (@None B). exists O. intros. auto.
Qed.
Lemma converges_to_unique:
forall a b, converges_to a b -> forall b', converges_to a b' -> b = b'.
Proof.
intros a b [n C] b' [n' C'].
rewrite <- (C (max n n')). rewrite <- (C' (max n n')). auto.
apply le_max_r. apply le_max_l.
Qed.
Lemma converges_to_exists_uniquely:
forall a, exists b, converges_to a b /\ forall b', converges_to a b' -> b = b'.
Proof.
intro. destruct (converges_to_exists a) as [b CT].
exists b. split. assumption. exact (converges_to_unique _ _ CT).
Qed.
Definition exists_iterate :=
dependent_description' A (fun _ => option B)
converges_to converges_to_exists_uniquely.
Definition iterate : A -> option B :=
match exists_iterate with existT f P => f end.
Lemma converges_to_iterate:
forall a b, converges_to a b -> iterate a = b.
Proof.
intros. unfold iterate. destruct exists_iterate as [f P].
apply converges_to_unique with a. apply P. auto.
Qed.
Lemma iterate_converges_to:
forall a, converges_to a (iterate a).
Proof.
intros. unfold iterate. destruct exists_iterate as [f P]. apply P.
Qed.
(** Invariance property. *)
Variable P: A -> Prop.
Variable Q: B -> Prop.
Hypothesis step_prop:
forall a : A, P a ->
match step a with inl b => Q b | inr a' => P a' end.
Lemma iter_prop:
forall n a b, P a -> iter n a = Some b -> Q b.
Proof.
induction n; intros until b; intro H; simpl.
congruence.
unfold F_iter. generalize (step_prop a H).
case (step a); intros. congruence.
apply IHn with a0; auto.
Qed.
Lemma iterate_prop:
forall a b, iterate a = Some b -> P a -> Q b.
Proof.
intros. destruct (iterate_converges_to a) as [n IT].
rewrite H in IT. apply iter_prop with n a. auto. apply IT. auto.
Qed.
End ITERATION.
End GenIter.
|
